Verify YM C297 weighted slice identification firewall

.github/workflows/ym-c297-weighted-slice-identification.yml

@@ -0,0 +1,78 @@
+name: YM C297 weighted slice identification
+
+on:
+  push:
+    branches:
+      - verification/ym-c297-weighted-slice-identification-20260820
+    paths:
+      - verification/ym-c297-weighted-slice-identification/*.lean
+      - .github/workflows/ym-c297-weighted-slice-identification.yml
+  pull_request:
+    paths:
+      - verification/ym-c297-weighted-slice-identification/*.lean
+      - .github/workflows/ym-c297-weighted-slice-identification.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-c297-weighted-slice-identification/FaizalShabirWeightedSliceIdentificationFirewall.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-c297-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-c297-weighted-slice-identification-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c297-axle-receipt.json

verification/ym-c297-weighted-slice-identification/FaizalShabirWeightedSliceIdentificationFirewall.lean

@@ -0,0 +1,45 @@
+import Mathlib
+
+/-!
+# C297 — weighted slice identification firewall
+
+Finite scalar algebra for one load-bearing point in the Faizal–Shabir OS-transfer audit.
+
+If an OS/slice form has scalar norm-square `t * x^2` with a strict weight `t < 1`,
+the bare identity map to ordinary Euclidean norm-square `x^2` need not be an isometry.
+A scalar multiplier whose square is `t` is exactly isometric for the weighted form.
+
+This file does not formalize Osterwalder–Schrader reconstruction, transfer operators,
+Yang–Mills theory, the mass gap, or the Clay theorem.
+-/
+
+namespace Millennium.YangMills.FaizalShabirWeightedSliceIdentificationFirewall
+
+/-- At the explicit contraction weight `t = 1/2`, the weighted OS norm of `1`
+is not the ordinary Euclidean norm of `1`. -/
+theorem bare_identity_not_isometry_at_half :
+    ((1 / 2 : ℝ) * (1 : ℝ)^2) ≠ (1 : ℝ)^2 := by
+  norm_num
+
+/-- Exact algebraic difference between the ordinary and weighted scalar
+norm-squares. -/
+theorem weighted_norm_difference
+    (t x : ℝ) :
+    x^2 - t * x^2 = (1 - t) * x^2 := by
+  ring
+
+/-- Any scalar multiplier `s` with `s^2 = t` gives the exact weighted
+isometry identity. The intended positive choice is `s = sqrt(t)`. -/
+theorem weighted_map_isometry_of_square
+    (s t x : ℝ)
+    (hs : s^2 = t) :
+    (s * x)^2 = t * x^2 := by
+  calc
+    (s * x)^2 = s^2 * x^2 := by ring
+    _ = t * x^2 := by rw [hs]
+
+#print axioms bare_identity_not_isometry_at_half
+#print axioms weighted_norm_difference
+#print axioms weighted_map_isometry_of_square
+
+end Millennium.YangMills.FaizalShabirWeightedSliceIdentificationFirewall