Verify YM C304 terminal-entry tail stability

.github/workflows/ym-c304-terminal-entry-tail-stability.yml

@@ -0,0 +1,78 @@
+name: YM C304 terminal-entry tail stability
+
+on:
+  push:
+    branches:
+      - verification/ym-c304-terminal-entry-tail-stability-20260820
+    paths:
+      - verification/ym-c304-terminal-entry-tail-stability/*.lean
+      - .github/workflows/ym-c304-terminal-entry-tail-stability.yml
+  pull_request:
+    paths:
+      - verification/ym-c304-terminal-entry-tail-stability/*.lean
+      - .github/workflows/ym-c304-terminal-entry-tail-stability.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-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.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-c304-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-c304-terminal-entry-tail-stability-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c304-axle-receipt.json

verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean

@@ -0,0 +1,73 @@
+import Mathlib
+
+/-!
+# Faizal–Shabir terminal-entry stability firewall
+
+Finite scalar logic for the ultraviolet-stability recurrence used upstream of
+the fixed-physical-scale clustering repair.
+
+This file deliberately does **not** formalize the Yang–Mills RG map, polymer
+norms, FRD, BKAR, continuum OS reconstruction, or a mass gap.  It checks only
+three load-bearing scalar facts:
+
+1. the printed condition `C * eps <= eps / 2` cannot be achieved merely by
+   making `eps` smaller; for positive `eps` it forces `C <= 1/2`;
+2. a finite additive forcing budget need not keep the first step inside an
+   arbitrarily small ball;
+3. after an independently proved entry into a radius-`r` ball, the quadratic
+   recurrence is forward invariant if the *tail* forcing is uniformly small.
+-/
+
+namespace Millennium.YangMills.FaizalShabirTerminalEntryFirewall
+
+theorem printed_epsilon_condition_forces_half_bound
+    (C eps : ℝ)
+    (heps : 0 < eps)
+    (h : C * eps <= eps / 2) :
+    C <= (1 : ℝ) / 2 := by
+  nlinarith
+
+theorem finite_forcing_can_break_small_ball
+    (C eps : ℝ)
+    (hsmall : 2 * eps < C) :
+    let x0 : ℝ := 0
+    let delta0 : ℝ := 1
+    let x1 : ℝ := C * x0 ^ 2 + C * delta0
+    2 * eps < x1 := by
+  dsimp
+  nlinarith
+
+theorem invariant_ball_under_small_tail
+    (C r : ℝ)
+    (x delta : ℕ → ℝ)
+    (hC : 0 <= C)
+    (hr : 0 <= r)
+    (hCr : C * r <= (1 : ℝ) / 2)
+    (hx_nonneg : ∀ n, 0 <= x n)
+    (hx0 : x 0 <= r)
+    (hdelta : ∀ n, C * delta n <= r / 2)
+    (hrec : ∀ n, x (n + 1) <= C * (x n) ^ 2 + C * delta n) :
+    ∀ n, x n <= r := by
+  intro n
+  induction n with
+  | zero =>
+      exact hx0
+  | succ n ih =>
+      have hxn0 : 0 <= x n := hx_nonneg n
+      have hsq : (x n) ^ 2 <= r ^ 2 := by
+        nlinarith
+      have hCsq : C * (x n) ^ 2 <= C * r ^ 2 :=
+        mul_le_mul_of_nonneg_left hsq hC
+      have hmul := mul_le_mul_of_nonneg_right hCr hr
+      have hCr2 : C * r ^ 2 <= r / 2 := by
+        nlinarith [hmul]
+      calc
+        x (n + 1) <= C * (x n) ^ 2 + C * delta n := hrec n
+        _ <= r / 2 + r / 2 := add_le_add (hCsq.trans hCr2) (hdelta n)
+        _ = r := by ring
+
+#print axioms printed_epsilon_condition_forces_half_bound
+#print axioms finite_forcing_can_break_small_ball
+#print axioms invariant_ball_under_small_tail
+
+end Millennium.YangMills.FaizalShabirTerminalEntryFirewall