From 740d436f044e57f7c1f011728f781e920bf4f4bc Mon Sep 17 00:00:00 2001
From: Steve Moraco <steve@lander.media>
Date: Wed, 19 Aug 2026 07:41:07 -0600
Subject: [PATCH 1/3] verify C286 triangular matching contraction source

---
 ...alShabirTriangularMatchingContraction.lean | 80 +++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean

diff --git a/verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean b/verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean
new file mode 100644
index 000000000..01b85d59e
--- /dev/null
+++ b/verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean
@@ -0,0 +1,80 @@
+import Mathlib
+
+namespace Millennium.YangMills.FaizalShabirTriangularMatchingContraction
+
+def geomEnvelope (q : ℝ) : ℕ → ℝ
+  | 0 => 0
+  | n + 1 => q * geomEnvelope q n + 1
+
+theorem homogeneous_contraction_iterate
+    (q D : ℝ)
+    (d : ℕ → ℝ)
+    (hq : 0 ≤ q)
+    (h0 : d 0 ≤ D)
+    (hstep : ∀ n, d (n + 1) ≤ q * d n) :
+    ∀ n, d n ≤ q ^ n * D := by
+  intro n
+  induction n with
+  | zero =>
+      simpa using h0
+  | succ n ih =>
+      calc
+        d (n + 1) ≤ q * d n := hstep n
+        _ ≤ q * (q ^ n * D) := mul_le_mul_of_nonneg_left ih hq
+        _ = q ^ (n + 1) * D := by
+          rw [pow_succ]
+          ring
+
+theorem homogeneous_contraction_hits_budget
+    (q D delta : ℝ)
+    (d : ℕ → ℝ)
+    (m : ℕ)
+    (hq : 0 ≤ q)
+    (h0 : d 0 ≤ D)
+    (hstep : ∀ n, d (n + 1) ≤ q * d n)
+    (hbudget : q ^ m * D ≤ delta) :
+    d m ≤ delta := by
+  exact (homogeneous_contraction_iterate q D d hq h0 hstep m).trans hbudget
+
+theorem affine_contraction_iterate
+    (q D eps : ℝ)
+    (d : ℕ → ℝ)
+    (hq : 0 ≤ q)
+    (h0 : d 0 ≤ D)
+    (hstep : ∀ n, d (n + 1) ≤ q * d n + eps) :
+    ∀ n, d n ≤ q ^ n * D + eps * geomEnvelope q n := by
+  intro n
+  induction n with
+  | zero =>
+      simpa [geomEnvelope] using h0
+  | succ n ih =>
+      calc
+        d (n + 1) ≤ q * d n + eps := hstep n
+        _ ≤ q * (q ^ n * D + eps * geomEnvelope q n) + eps := by
+          exact add_le_add_right (mul_le_mul_of_nonneg_left ih hq) eps
+        _ = q ^ (n + 1) * D + eps * geomEnvelope q (n + 1) := by
+          rw [geomEnvelope, pow_succ]
+          ring
+
+theorem affine_contraction_hits_budget
+    (q D eps G delta : ℝ)
+    (d : ℕ → ℝ)
+    (m : ℕ)
+    (hq : 0 ≤ q)
+    (heps : 0 ≤ eps)
+    (h0 : d 0 ≤ D)
+    (hstep : ∀ n, d (n + 1) ≤ q * d n + eps)
+    (hgeom : geomEnvelope q m ≤ G)
+    (hbudget : q ^ m * D + eps * G ≤ delta) :
+    d m ≤ delta := by
+  have hiter := affine_contraction_iterate q D eps d hq h0 hstep m
+  have hforce : eps * geomEnvelope q m ≤ eps * G :=
+    mul_le_mul_of_nonneg_left hgeom heps
+  exact hiter.trans ((add_le_add_left hforce (q ^ m * D)).trans hbudget)
+
+#print axioms homogeneous_contraction_iterate
+#print axioms homogeneous_contraction_hits_budget
+#print axioms affine_contraction_iterate
+#print axioms affine_contraction_hits_budget
+
+end Millennium.YangMills.FaizalShabirTriangularMatchingContraction

From 3ed1c9218571be273e8ea2eb68a1165a773d4120 Mon Sep 17 00:00:00 2001
From: Steve Moraco <steve@lander.media>
Date: Wed, 19 Aug 2026 07:41:23 -0600
Subject: [PATCH 2/3] add guarded C286 Lean verifier workflow

---
 ...m-c286-triangular-matching-contraction.yml | 78 +++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100644 .github/workflows/ym-c286-triangular-matching-contraction.yml

diff --git a/.github/workflows/ym-c286-triangular-matching-contraction.yml b/.github/workflows/ym-c286-triangular-matching-contraction.yml
new file mode 100644
index 000000000..86b45489c
--- /dev/null
+++ b/.github/workflows/ym-c286-triangular-matching-contraction.yml
@@ -0,0 +1,78 @@
+name: YM C286 triangular matching contraction
+
+on:
+  push:
+    branches:
+      - verification/ym-c286-triangular-matching-contraction-20260819
+    paths:
+      - verification/ym-c286-triangular-matching-contraction/*.lean
+      - .github/workflows/ym-c286-triangular-matching-contraction.yml
+  pull_request:
+    paths:
+      - verification/ym-c286-triangular-matching-contraction/*.lean
+      - .github/workflows/ym-c286-triangular-matching-contraction.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-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.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-c286-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-c286-triangular-matching-contraction-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c286-axle-receipt.json

From 2272e41d9c3489d8515899d25b0c91b5def00ac0 Mon Sep 17 00:00:00 2001
From: Steve Moraco <steve@lander.media>
Date: Wed, 19 Aug 2026 07:42:42 -0600
Subject: [PATCH 3/3] repair C286 verifier after failed-first Lean proof
 mismatch

---
 .../FaizalShabirTriangularMatchingContraction.lean         | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean b/verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean
index 01b85d59e..e4e25be28 100644
--- a/verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean
+++ b/verification/ym-c286-triangular-matching-contraction/FaizalShabirTriangularMatchingContraction.lean
@@ -51,7 +51,8 @@ theorem affine_contraction_iterate
       calc
         d (n + 1) ≤ q * d n + eps := hstep n
         _ ≤ q * (q ^ n * D + eps * geomEnvelope q n) + eps := by
-          exact add_le_add_right (mul_le_mul_of_nonneg_left ih hq) eps
+          have hmul := mul_le_mul_of_nonneg_left ih hq
+          nlinarith
         _ = q ^ (n + 1) * D + eps * geomEnvelope q (n + 1) := by
           rw [geomEnvelope, pow_succ]
           ring
@@ -70,7 +71,9 @@ theorem affine_contraction_hits_budget
   have hiter := affine_contraction_iterate q D eps d hq h0 hstep m
   have hforce : eps * geomEnvelope q m ≤ eps * G :=
     mul_le_mul_of_nonneg_left hgeom heps
-  exact hiter.trans ((add_le_add_left hforce (q ^ m * D)).trans hbudget)
+  have hmid : q ^ m * D + eps * geomEnvelope q m ≤ q ^ m * D + eps * G := by
+    nlinarith
+  exact hiter.trans (hmid.trans hbudget)
 
 #print axioms homogeneous_contraction_iterate
 #print axioms homogeneous_contraction_hits_budget