Verify YM C328 parabolic-cone harmonic bootstrap

.github/workflows/ym-c328-parabolic-cone-harmonic-bootstrap.yml

@@ -0,0 +1,52 @@
+name: YM C328 parabolic-cone harmonic bootstrap
+
+on:
+  push:
+    branches:
+      - verification/ym-c328-parabolic-cone-harmonic-bootstrap-20260820
+    paths:
+      - verification/ym-c328-parabolic-cone-harmonic-bootstrap/*.lean
+      - .github/workflows/ym-c328-parabolic-cone-harmonic-bootstrap.yml
+  pull_request:
+    paths:
+      - verification/ym-c328-parabolic-cone-harmonic-bootstrap/*.lean
+      - .github/workflows/ym-c328-parabolic-cone-harmonic-bootstrap.yml
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    runs-on: ubuntu-22.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v4
+      - name: Verify flattened Lean theorem source
+        shell: bash
+        run: |
+          set -euo pipefail
+          SRC=verification/ym-c328-parabolic-cone-harmonic-bootstrap/FaizalShabirParabolicConeHarmonicBootstrap.lean
+          if grep -nE '\b(sorry|admit|sorryAx|axiom|opaque|unsafe|native_decide|Lean\.ofReduceBool)\b' "$SRC"; then exit 1; fi
+          SRC="$SRC" python3 - <<'PY'
+          import hashlib, json, os, pathlib, urllib.request
+          path = pathlib.Path(os.environ['SRC'])
+          source = path.read_text()
+          payload = json.dumps({'content': source,'environment':'lean-4.30.0','ignore_imports':True,'mathlib_options':False,'timeout_seconds':900}).encode()
+          req = urllib.request.Request('https://axle.axiommath.ai/api/v1/check', data=payload, headers={'Content-Type':'application/json'}, method='POST')
+          with urllib.request.urlopen(req, timeout=960) as response:
+            result = json.load(response)
+          receipt={'source_path':str(path),'source_sha256':hashlib.sha256(source.encode()).hexdigest(),'axle_environment':'lean-4.30.0','axle_result':result}
+          pathlib.Path('/tmp/ym-c328-axle-receipt.json').write_text(json.dumps(receipt,indent=2))
+          print(json.dumps(receipt,indent=2))
+          lean=result.get('lean_messages',{}); tool=result.get('tool_messages',{})
+          bad=(not result.get('okay') or bool(result.get('failed_declarations',[])) or bool(lean.get('errors',[])) or bool(lean.get('warnings',[])) or bool(tool.get('errors',[])) or bool(tool.get('warnings',[])) or 'sorryAx' in json.dumps(result))
+          if bad: raise SystemExit(1)
+          PY
+      - uses: actions/upload-artifact@v4
+        if: always()
+        with:
+          name: ym-c328-parabolic-cone-harmonic-bootstrap-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c328-axle-receipt.json

verification/ym-c328-parabolic-cone-harmonic-bootstrap/FaizalShabirParabolicConeHarmonicBootstrap.lean

@@ -0,0 +1,66 @@
+import Mathlib
+
+/-!
+# C328: parabolic center/stable cone finite firewall
+
+Finite real-algebra consumers for the repaired Faizal--Shabir weak-RG architecture.
+
+The file proves only:
+* a cubic center step with remainder `|R| <= rho * g^3` lies between two
+  cubic comparison steps;
+* `rho < beta` leaves a positive effective cubic decrement;
+* on the parabolic boundary `K = A g^2`, the mixed `g K` channel is exactly
+  cubic order and therefore can shift the one-loop coefficient unless a
+  stronger cancellation/subquadratic theorem is supplied.
+
+It does not formalize the Yang--Mills Banach RG, an invariant cone, asymptotic
+freedom, AF/IR identification, continuum OS reconstruction, a mass gap, or the
+Clay theorem.
+-/
+
+namespace Millennium.YangMills.FaizalShabirParabolicConeHarmonicBootstrap
+
+/-- A center step with an absolute cubic remainder lies between the two
+comparison cubic steps. -/
+theorem center_step_two_sided
+    (g g' beta rho R : ℝ)
+    (hstep : g' = g - beta * g ^ 3 + R)
+    (hR : |R| ≤ rho * g ^ 3)
+    (hg : 0 ≤ g) :
+    g - (beta + rho) * g ^ 3 ≤ g' ∧
+      g' ≤ g - (beta - rho) * g ^ 3 := by
+  have hpow : 0 ≤ g ^ 3 := by positivity
+  have hRlo : -(rho * g ^ 3) ≤ R := (abs_le.mp hR).1
+  have hRhi : R ≤ rho * g ^ 3 := (abs_le.mp hR).2
+  constructor
+  · rw [hstep]
+    nlinarith
+  · rw [hstep]
+    nlinarith
+
+/-- A strict cubic remainder margin leaves a positive effective decrement. -/
+theorem effective_cubic_margin_pos
+    (beta rho : ℝ)
+    (hmargin : rho < beta) :
+    0 < beta - rho := by
+  linarith
+
+/-- On the parabolic boundary `K = A g^2`, the allowed mixed center channel
+`g*K` is exactly cubic order. -/
+theorem mixed_channel_is_cubic_on_parabolic_boundary
+    (g A : ℝ) :
+    g * (A * g ^ 2) = A * g ^ 3 := by
+  ring
+
+/-- The quadratic stable channel on the same boundary is fourth order. -/
+theorem stable_square_is_quartic_on_parabolic_boundary
+    (g A : ℝ) :
+    (A * g ^ 2) ^ 2 = A ^ 2 * g ^ 4 := by
+  ring
+
+#print axioms center_step_two_sided
+#print axioms effective_cubic_margin_pos
+#print axioms mixed_channel_is_cubic_on_parabolic_boundary
+#print axioms stable_square_is_quartic_on_parabolic_boundary
+
+end Millennium.YangMills.FaizalShabirParabolicConeHarmonicBootstrap