Verify YM C271 polar-conditioning firewall

.github/workflows/ym-c271-polar-conditioning.yml

@@ -0,0 +1,80 @@
+name: YM C271 polar conditioning firewall
+
+on:
+  push:
+    branches:
+      - verification/ym-c271-polar-conditioning-20260819
+    paths:
+      - verification/ym-c271-polar-conditioning/*.lean
+      - .github/workflows/ym-c271-polar-conditioning.yml
+  pull_request:
+    paths:
+      - verification/ym-c271-polar-conditioning/*.lean
+      - .github/workflows/ym-c271-polar-conditioning.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-c271-polar-conditioning/FaizalShabirPolarConditioningFirewall.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-c271-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-c271-polar-conditioning-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c271-axle-receipt.json

verification/ym-c271-polar-conditioning/FaizalShabirPolarConditioningFirewall.lean

@@ -0,0 +1,83 @@
+import Mathlib
+
+/-!
+# Faizal–Shabir polar-conditioning firewall
+
+Finite scalar shadow of the load-bearing conditioning problem in the
+Faizal–Shabir block map. The unitary polar factor of a matrix behaves, on the
+one-dimensional real slice, like `x ↦ x / |x|`. Near the singular point zero
+there is no uniform Lipschitz constant.
+
+This file deliberately does **not** formalize SU(N), path holonomies, the
+matrix polar decomposition, the Yang–Mills block map, Gaussian chart
+factorization, RG, Osterwalder–Schrader reconstruction, or a mass gap.
+-/
+
+namespace Millennium.YangMills.FaizalShabirPolarConditioningFirewall
+
+/-- Scalar polar factor, with an arbitrary convention at the singular point. -/
+noncomputable def scalarPolar (x : ℝ) : ℝ := if 0 ≤ x then 1 else -1
+
+/-- The scalar polar factor is `+1` on the positive half-line. -/
+theorem scalarPolar_pos {x : ℝ} (hx : 0 < x) : scalarPolar x = 1 := by
+  simp [scalarPolar, le_of_lt hx]
+
+/-- The scalar polar factor is `-1` on the negative half-line. -/
+theorem scalarPolar_neg {x : ℝ} (hx : x < 0) : scalarPolar x = -1 := by
+  simp [scalarPolar, not_le.mpr hx]
+
+/-- No finite Lipschitz constant controls the scalar polar factor uniformly
+across arbitrarily near-singular inputs of opposite sign. -/
+theorem scalarPolar_no_uniform_lipschitz
+    (L : ℝ) (hL : 0 ≤ L) :
+    ∃ x y : ℝ,
+      0 < x ∧ y < 0 ∧
+      |scalarPolar x - scalarPolar y| > L * |x - y| := by
+  let t : ℝ := 1 / (L + 1)
+  have hden : 0 < L + 1 := by linarith
+  have ht : 0 < t := by
+    dsimp [t]
+    exact one_div_pos.mpr hden
+  refine ⟨t, -t, ht, by linarith, ?_⟩
+  have hpx : scalarPolar t = 1 := scalarPolar_pos ht
+  have hpy : scalarPolar (-t) = -1 := scalarPolar_neg (by linarith)
+  have hpolarDist : |scalarPolar t - scalarPolar (-t)| = 2 := by
+    rw [hpx, hpy]
+    norm_num
+  have hdist : |t - (-t)| = 2 * t := by
+    rw [abs_of_nonneg]
+    · ring
+    · linarith
+  have hratio : L / (L + 1) < 1 := by
+    exact (div_lt_one hden).2 (by linarith)
+  have hLt : L * t < 1 := by
+    simpa [t, div_eq_mul_inv] using hratio
+  rw [hpolarDist, hdist]
+  nlinarith
+
+/-- If a scalar lies within `ε` of `1`, it lies above the explicit lower
+conditioning margin `1 - ε`. -/
+theorem near_one_has_lower_margin
+    (x ε : ℝ)
+    (hx : |x - 1| ≤ ε) :
+    1 - ε ≤ x := by
+  have h := (abs_le.mp hx).1
+  linarith
+
+/-- If the radius is strictly below one, the preceding lower margin is
+strictly positive. -/
+theorem near_one_is_positive
+    (x ε : ℝ)
+    (hε : ε < 1)
+    (hx : |x - 1| ≤ ε) :
+    0 < x := by
+  have hmargin := near_one_has_lower_margin x ε hx
+  linarith
+
+#print axioms scalarPolar_pos
+#print axioms scalarPolar_neg
+#print axioms scalarPolar_no_uniform_lipschitz
+#print axioms near_one_has_lower_margin
+#print axioms near_one_is_positive
+
+end Millennium.YangMills.FaizalShabirPolarConditioningFirewall