Verify YM C292 coarse-frame dual operatorization

.github/workflows/ym-c292-coarse-frame-dual-operatorization.yml

@@ -0,0 +1,78 @@
+name: YM C292 coarse-frame dual operatorization
+
+on:
+  push:
+    branches:
+      - verification/ym-c292-coarse-frame-dual-operatorization-20260819
+    paths:
+      - verification/ym-c292-coarse-frame-dual-operatorization/*.lean
+      - .github/workflows/ym-c292-coarse-frame-dual-operatorization.yml
+  pull_request:
+    paths:
+      - verification/ym-c292-coarse-frame-dual-operatorization/*.lean
+      - .github/workflows/ym-c292-coarse-frame-dual-operatorization.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-c292-coarse-frame-dual-operatorization/FaizalShabirCoarseFrameDualFirewall.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-c292-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-c292-coarse-frame-dual-operatorization-axle-receipt
+          if-no-files-found: warn
+          retention-days: 30
+          path: /tmp/ym-c292-axle-receipt.json

verification/ym-c292-coarse-frame-dual-operatorization/FaizalShabirCoarseFrameDualFirewall.lean

@@ -0,0 +1,68 @@
+import Mathlib
+
+/-!
+# Faizal–Shabir coarse-frame / dual-basis operatorization firewall
+
+Finite real-algebra shadow of a load-bearing source issue in the Section-5
+mixed-block construction.
+
+The manuscript first chooses arbitrary vacuum-centered coarse test observables
+and forms the matrix of transfer/cumulant matrix elements in those vectors. It
+then reconstructs an operator using the same vectors as ket/bra coefficients.
+For a non-orthonormal basis this is not coordinate invariant: matrix elements
+must be paired with the dual basis (equivalently inverse Gram factors).
+
+In one dimension this is already visible. If the physical operator is scalar
+`op` and the chosen basis vector is represented by nonzero scalar `v`, then the
+matrix element is `op * v^2`. Reconstructing with the same vector once more
+produces `op * v^4`, which changes quartically under basis rescaling. Dividing
+by the basis Gram factor `v^2` (the one-dimensional dual-basis correction)
+recovers `op` exactly and is invariant under nonzero rescaling.
+
+This file proves only that finite algebraic firewall. It does not formalize
+OS Hilbert spaces, localized frames, dual-frame decay, the Faizal–Shabir mixed
+operator, Yang–Mills fields, regulator/volume uniformity, or a Clay theorem.
+-/
+
+namespace Millennium.YangMills.FaizalShabirCoarseFrameDualFirewall
+
+def matrixElement (op v : ℝ) : ℝ := op * v * v
+
+def naiveReconstruction (op v : ℝ) : ℝ := matrixElement op v * v * v
+
+theorem naive_reconstruction_eq_quartic (op v : ℝ) :
+    naiveReconstruction op v = op * v ^ 4 := by
+  simp [naiveReconstruction, matrixElement, pow_succ]
+  ring
+
+theorem naive_reconstruction_rescales_quartically (op v t : ℝ) :
+    naiveReconstruction op (t * v) = t ^ 4 * naiveReconstruction op v := by
+  simp [naiveReconstruction, matrixElement]
+  ring
+
+theorem naive_reconstruction_two_witness :
+    naiveReconstruction 1 2 = 16 := by
+  norm_num [naiveReconstruction, matrixElement]
+
+noncomputable def dualReconstruction (op v : ℝ) : ℝ :=
+  matrixElement op v / (v * v)
+
+theorem dual_reconstruction_exact (op v : ℝ) (hv : v ≠ 0) :
+    dualReconstruction op v = op := by
+  unfold dualReconstruction matrixElement
+  field_simp [hv]
+
+theorem dual_reconstruction_rescaling_invariant
+    (op v t : ℝ) (hv : v ≠ 0) (ht : t ≠ 0) :
+    dualReconstruction op (t * v) = dualReconstruction op v := by
+  have htv : t * v ≠ 0 := mul_ne_zero ht hv
+  rw [dual_reconstruction_exact op (t * v) htv]
+  rw [dual_reconstruction_exact op v hv]
+
+#print axioms naive_reconstruction_eq_quartic
+#print axioms naive_reconstruction_rescales_quartically
+#print axioms naive_reconstruction_two_witness
+#print axioms dual_reconstruction_exact
+#print axioms dual_reconstruction_rescaling_invariant
+
+end Millennium.YangMills.FaizalShabirCoarseFrameDualFirewall