Verify YM C327 Theorem 10.7 geometric-center firewall

.github/workflows/ym-c327-theorem107-geometric-center.yml

@@ -0,0 +1,52 @@
+name: YM C327 Theorem 10.7 geometric-center firewall
+
+on:
+  push:
+    branches:
+      - verification/ym-c327-theorem107-geometric-center-20260820
+    paths:
+      - verification/ym-c327-theorem107-geometric-center/*.lean
+      - .github/workflows/ym-c327-theorem107-geometric-center.yml
+  pull_request:
+    paths:
+      - verification/ym-c327-theorem107-geometric-center/*.lean
+      - .github/workflows/ym-c327-theorem107-geometric-center.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-c327-theorem107-geometric-center/FaizalShabirTheorem107GeometricCenterFirewall.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-c327-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-c327-theorem107-geometric-center-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c327-axle-receipt.json

verification/ym-c327-theorem107-geometric-center/FaizalShabirTheorem107GeometricCenterFirewall.lean

@@ -0,0 +1,85 @@
+import Mathlib
+
+/-!
+# Theorem 10.7 geometric-center firewall
+
+Finite scalar firewall for the displayed Faizal--Shabir weak-RG recurrences.
+
+The source's Theorem 10.7 uses a center recurrence
+
+`g' = g - a*g^3 + R_g`
+
+with a remainder bounded by terms including `K^2`, and a homogeneous stable
+recurrence with strict linear contraction. These bounds alone do not force the
+center to have the claimed `k^(-1/2)` asymptotic: the `K^2` channel can support
+a geometrically decaying positive center trajectory.
+
+This file formalizes only the finite one-step algebra behind that countermodel.
+It does not formalize an RG trajectory, admissibility, Yang--Mills, asymptotic
+freedom, AF/IR identification, a mass gap, continuum OS reconstruction, or the
+Clay theorem.
+-/
+
+namespace Millennium.YangMills.FaizalShabirTheorem107GeometricCenterFirewall
+
+/-- Exact factorization of the remainder needed to turn the cubic center step
+into the geometric step `g' = g/4`. -/
+theorem center_remainder_factorization (a g : ℝ) :
+    g / 4 - g + a * g ^ 3 = g * (a * g ^ 2 - (3 : ℝ) / 4) := by
+  ring
+
+/-- The geometric center step is exactly a cubic center step plus its required
+remainder. -/
+theorem quarter_step_is_cubic_step_plus_remainder (a g : ℝ) :
+    g / 4 = g - a * g ^ 3 + (g / 4 - g + a * g ^ 3) := by
+  ring
+
+/-- If the stable coordinate satisfies `K^2 = g`, then for sufficiently small
+`g` the remainder required by `g' = g/4` is already bounded by the source-shaped
+majorant `g^5 + g*K + K^2`.
+
+Thus a `K^2` term in an absolute remainder bound can permit a geometric center
+step unless an additional relative center/stable condition or cancellation is
+proved. -/
+theorem source_shaped_bound_allows_quarter_center_step
+    (a g K : ℝ)
+    (ha : 0 ≤ a)
+    (hg : 0 ≤ g)
+    (hK : 0 ≤ K)
+    (hKsq : K ^ 2 = g)
+    (hsmall : a * g ^ 2 ≤ (3 : ℝ) / 4) :
+    |g / 4 - g + a * g ^ 3| ≤ g ^ 5 + g * K + K ^ 2 := by
+  have hfactor_nonpos : a * g ^ 2 - (3 : ℝ) / 4 ≤ 0 := by
+    linarith
+  have hfactor_le_one : (3 : ℝ) / 4 - a * g ^ 2 ≤ 1 := by
+    have hag2 : 0 ≤ a * g ^ 2 := mul_nonneg ha (sq_nonneg g)
+    linarith
+  have hleft : |g / 4 - g + a * g ^ 3| ≤ g := by
+    rw [center_remainder_factorization, abs_mul, abs_of_nonneg hg,
+      abs_of_nonpos hfactor_nonpos]
+    have heq : -(a * g ^ 2 - (3 : ℝ) / 4) = (3 : ℝ) / 4 - a * g ^ 2 := by
+      ring
+    rw [heq]
+    simpa using mul_le_mul_of_nonneg_left hfactor_le_one hg
+  have hpow : 0 ≤ g ^ 5 := pow_nonneg hg 5
+  have hmul : 0 ≤ g * K := mul_nonneg hg hK
+  have hrhs : g ≤ g ^ 5 + g * K + K ^ 2 := by
+    rw [hKsq]
+    linarith
+  exact hleft.trans hrhs
+
+/-- The parabolic relation `K^2 = g` is preserved by the geometric pair of
+steps `K' = K/2`, `g' = g/4`. -/
+theorem half_quarter_preserves_square_relation
+    (g K : ℝ)
+    (hKsq : K ^ 2 = g) :
+    (K / 2) ^ 2 = g / 4 := by
+  rw [div_pow, hKsq]
+  norm_num
+
+#print axioms center_remainder_factorization
+#print axioms quarter_step_is_cubic_step_plus_remainder
+#print axioms source_shaped_bound_allows_quarter_center_step
+#print axioms half_quarter_preserves_square_relation
+
+end Millennium.YangMills.FaizalShabirTheorem107GeometricCenterFirewall