From 49eddceda3639ad461085f6b42a21e21bc9ced22 Mon Sep 17 00:00:00 2001 From: Steve Moraco Date: Wed, 19 Aug 2026 15:29:24 -0600 Subject: [PATCH 1/3] verify(ym): mirror C304 terminal-entry recurrence --- .../FaizalShabirTerminalEntryFirewall.lean | 90 +++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100644 verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean diff --git a/verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean b/verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean new file mode 100644 index 000000000..8a2294555 --- /dev/null +++ b/verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean @@ -0,0 +1,90 @@ +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. + +The third fact is the finite consumer behind the repaired terminal-scale gate: +reindex a regulator row at its entry index `K` and apply the theorem to the +shifted sequences. +-/ + +namespace Millennium.YangMills.FaizalShabirTerminalEntryFirewall + +/-- The condition printed in the source, `C * eps <= eps / 2`, is a condition +on `C`, not something that can be forced by shrinking a positive `eps`. -/ +theorem printed_epsilon_condition_forces_half_bound + (C eps : ℝ) + (heps : 0 < eps) + (h : C * eps <= eps / 2) : + C <= (1 : ℝ) / 2 := by + nlinarith + +/-- A one-step forcing sequence can have finite total mass and still eject the +quadratic recurrence from an arbitrarily small target ball. This is the +finite first-step shadow of why mere summability of nonnegative defects is not +a smallness theorem. -/ +theorem finite_forcing_can_break_small_ball + (C eps : ℝ) + (hC : 0 < C) + (heps : 0 < eps) + (hsmall : 2 * eps < C) : + let x0 : ℝ := 0 + let delta0 : ℝ := 1 + let x1 : ℝ := C * x0 ^ 2 + C * delta0 + 2 * eps < x1 := by + dsimp + nlinarith + +/-- Once a trajectory has independently entered a radius-`r` ball, a uniform +small tail forcing keeps the quadratic recurrence inside that ball. + +In the RG application one shifts the index so that `x 0` is the activity norm +at the entry scale `K`; `delta n` is the corresponding tail defect. -/ +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 + simpa [pow_two, mul_assoc] using 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 From 82fae0393b2d8a1289754e217f6b7e3ddeff6fca Mon Sep 17 00:00:00 2001 From: Steve Moraco Date: Wed, 19 Aug 2026 15:29:37 -0600 Subject: [PATCH 2/3] ci(ym): guard C304 terminal-entry Lean source --- .../ym-c304-terminal-entry-tail-stability.yml | 78 +++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 .github/workflows/ym-c304-terminal-entry-tail-stability.yml diff --git a/.github/workflows/ym-c304-terminal-entry-tail-stability.yml b/.github/workflows/ym-c304-terminal-entry-tail-stability.yml new file mode 100644 index 000000000..468f805c9 --- /dev/null +++ b/.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 From 9743bd62ae3c8f2cef1582924f6bb24d62aba3b5 Mon Sep 17 00:00:00 2001 From: Steve Moraco Date: Wed, 19 Aug 2026 15:39:18 -0600 Subject: [PATCH 3/3] fix(ym): clean C304 finite replay --- .../FaizalShabirTerminalEntryFirewall.lean | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean b/verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean index 8a2294555..1fe1c1e0c 100644 --- a/verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean +++ b/verification/ym-c304-terminal-entry-tail-stability/FaizalShabirTerminalEntryFirewall.lean @@ -16,16 +16,10 @@ three load-bearing scalar facts: 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. - -The third fact is the finite consumer behind the repaired terminal-scale gate: -reindex a regulator row at its entry index `K` and apply the theorem to the -shifted sequences. -/ namespace Millennium.YangMills.FaizalShabirTerminalEntryFirewall -/-- The condition printed in the source, `C * eps <= eps / 2`, is a condition -on `C`, not something that can be forced by shrinking a positive `eps`. -/ theorem printed_epsilon_condition_forces_half_bound (C eps : ℝ) (heps : 0 < eps) @@ -33,14 +27,8 @@ theorem printed_epsilon_condition_forces_half_bound C <= (1 : ℝ) / 2 := by nlinarith -/-- A one-step forcing sequence can have finite total mass and still eject the -quadratic recurrence from an arbitrarily small target ball. This is the -finite first-step shadow of why mere summability of nonnegative defects is not -a smallness theorem. -/ theorem finite_forcing_can_break_small_ball (C eps : ℝ) - (hC : 0 < C) - (heps : 0 < eps) (hsmall : 2 * eps < C) : let x0 : ℝ := 0 let delta0 : ℝ := 1 @@ -49,11 +37,6 @@ theorem finite_forcing_can_break_small_ball dsimp nlinarith -/-- Once a trajectory has independently entered a radius-`r` ball, a uniform -small tail forcing keeps the quadratic recurrence inside that ball. - -In the RG application one shifts the index so that `x 0` is the activity norm -at the entry scale `K`; `delta n` is the corresponding tail defect. -/ theorem invariant_ball_under_small_tail (C r : ℝ) (x delta : ℕ → ℝ) @@ -77,7 +60,7 @@ theorem invariant_ball_under_small_tail 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 - simpa [pow_two, mul_assoc] using hmul + 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)