diff --git a/.github/workflows/ym-c327-theorem107-geometric-center.yml b/.github/workflows/ym-c327-theorem107-geometric-center.yml new file mode 100644 index 000000000..92800928a --- /dev/null +++ b/.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 diff --git a/verification/ym-c327-theorem107-geometric-center/FaizalShabirTheorem107GeometricCenterFirewall.lean b/verification/ym-c327-theorem107-geometric-center/FaizalShabirTheorem107GeometricCenterFirewall.lean new file mode 100644 index 000000000..5706d209b --- /dev/null +++ b/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