Verify YM C325 Proj_G field/activity typing firewall

.github/workflows/ym-c325-projg-field-activity-typing.yml

@@ -0,0 +1,52 @@
+name: YM C325 Proj_G field/activity typing
+
+on:
+  push:
+    branches:
+      - verification/ym-c325-projg-field-activity-typing-20260820
+    paths:
+      - verification/ym-c325-projg-field-activity-typing/*.lean
+      - .github/workflows/ym-c325-projg-field-activity-typing.yml
+  pull_request:
+    paths:
+      - verification/ym-c325-projg-field-activity-typing/*.lean
+      - .github/workflows/ym-c325-projg-field-activity-typing.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-c325-projg-field-activity-typing/FaizalShabirProjGFieldActivityTypingFirewall.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-c325-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-c325-projg-field-activity-typing-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c325-axle-receipt.json

verification/ym-c325-projg-field-activity-typing/FaizalShabirProjGFieldActivityTypingFirewall.lean

@@ -0,0 +1,49 @@
+import Mathlib
+
+/-!
+# Proj_G field-size versus activity-size firewall
+
+Finite scalar bookkeeping for C325.
+
+The source-level issue is a type distinction: a nearest-group projection correction
+can be second order in an independent local field/chart size without being quadratic
+in an unrelated polymer activity norm. The repaired fixed-terminal-scale route may
+instead pay such a correction as a fixed additive local budget.
+
+This file does not formalize SU(N), the polar map, BKAR, polymer activities,
+reflection positivity, a Yang--Mills RG step, a mass gap, or the Clay theorem.
+-/
+
+namespace Millennium.YangMills.FaizalShabirProjGFieldActivityTypingFirewall
+
+/-- A strictly positive correction present at zero activity cannot satisfy a
+uniform bound by `C * activity^2`. -/
+theorem positive_field_correction_not_activity_quadratic
+    (C projection : ℝ)
+    (hprojection : 0 < projection) :
+    ¬ projection ≤ C * (0 : ℝ) ^ 2 := by
+  simpa using (not_le.mpr hprojection)
+
+/-- Four independent nonnegative one-step budgets, each no larger than a
+quarter of the invariant radius, fit inside that radius. -/
+theorem four_way_invariant_budget
+    (quadratic largeField projection genuineResidual radius : ℝ)
+    (hquadratic : quadratic ≤ radius / 4)
+    (hlarge : largeField ≤ radius / 4)
+    (hprojection : projection ≤ radius / 4)
+    (hgenuine : genuineResidual ≤ radius / 4) :
+    quadratic + largeField + projection + genuineResidual ≤ radius := by
+  linarith
+
+/-- A field-quadratic projection estimate can be consumed as one fixed quarter
+of an invariant-ball budget without identifying field size with activity size. -/
+theorem field_quadratic_projection_fits_quarter_budget
+    (C δ radius : ℝ)
+    (hbudget : C * δ ^ 2 ≤ radius / 4) :
+    C * δ ^ 2 ≤ radius / 4 := hbudget
+
+#print axioms positive_field_correction_not_activity_quadratic
+#print axioms four_way_invariant_budget
+#print axioms field_quadratic_projection_fits_quarter_budget
+
+end Millennium.YangMills.FaizalShabirProjGFieldActivityTypingFirewall