diff --git a/.github/workflows/unitary-prefix-norm.yml b/.github/workflows/unitary-prefix-norm.yml
new file mode 100644
index 0000000000..fbb59cb1ec
--- /dev/null
+++ b/.github/workflows/unitary-prefix-norm.yml
@@ -0,0 +1,43 @@
+name: Verify unitary prefix norm lemmas
+
+on:
+  pull_request:
+    paths:
+      - 'research/lean-unitary-prefix-norm/**'
+      - 'research/e8-lemma-g-lean/LemmaG/Stream.lean'
+      - 'research/e8-lemma-g-lean/PROOF.md'
+      - 'research/e8-lemma-g-lean/lake-manifest.json'
+      - 'research/e8-lemma-g-lean/lean-toolchain'
+      - 'research/hyperplane-end-lean/PROOF.md'
+      - '.github/workflows/unitary-prefix-norm.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  lean-prefix-norm:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7
+        with:
+          fetch-depth: 0
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7
+        with:
+          python-version: '3.12'
+      - name: Check source bindings and guard tests
+        run: |
+          python3 -I -B research/lean-unitary-prefix-norm/verify.py --source-only
+          python3 -I -B research/lean-unitary-prefix-norm/test_verifier.py
+      - name: Install pinned elan bootstrap
+        run: |
+          curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/leanprover/elan/0e36a07b9bbcc5381fa6250df109f9a4f94d7bac/elan-init.sh -o /tmp/elan-init.sh
+          sh /tmp/elan-init.sh -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+      - name: Build fresh proofs and audit all theorem axioms
+        run: |
+          python3 -I -B research/lean-unitary-prefix-norm/verify.py --work "$RUNNER_TEMP/unitary-prefix-norm"
+          cat "$RUNNER_TEMP/unitary-prefix-norm/AXIOMS.log"
+          git diff --exit-code
diff --git a/research/lean-unitary-prefix-norm/AXIOMS.json b/research/lean-unitary-prefix-norm/AXIOMS.json
new file mode 100644
index 0000000000..053618cb98
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/AXIOMS.json
@@ -0,0 +1,166 @@
+{
+  "PrefixNorm.Examples.asymmetric_preserves_norm": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.backward_bits_if": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.bad_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.bad_endpoint": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.bad_not_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.eight_not_norm_preserving": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.forward_bits_if": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.good_cancellation_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.good_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.good_prefix_bound": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.half_store_overshoot": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_endpoint": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_exact": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.loop_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.phases_norm": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.recipe_exact": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.wrong_recipe_cut": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.wrong_recipe_labelled": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.Examples.wrong_recipe_not_exact": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.components_bits": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.components_sq": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.components_uniform": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.inverse_norm": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.recipesExact_take": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.splice_bits": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.splice_sq": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.splice_uniform": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.supported_certificate": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.supported_prefix": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.weighted_prefix": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.weighted_row": [
+    "Classical.choice",
+    "Quot.sound",
+    "propext"
+  ],
+  "PrefixNorm.wellLabelled_take": [
+    "Quot.sound",
+    "propext"
+  ]
+}
diff --git a/research/lean-unitary-prefix-norm/OVERLAP.json b/research/lean-unitary-prefix-norm/OVERLAP.json
new file mode 100644
index 0000000000..e51d3450b4
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/OVERLAP.json
@@ -0,0 +1,112 @@
+{
+  "schema_version": 1,
+  "status": "bounded overlap evidence, not a novelty certificate",
+  "base_commit": "bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c",
+  "refreshed_main": "bce54fb3f895cbe5cd4c0eb477c3afeed100190f",
+  "refresh_delta": "Only historical reconciliation92 evidence/ledger changes; selected record, guidance, catalogue and all five live proof inputs unchanged.",
+  "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1291",
+  "entry": {
+    "searched_at": "2026-10-13T21:46:15.108970+00:00",
+    "terms": [
+      "prefix norm",
+      "signed prefix",
+      "unitary",
+      "formal interface"
+    ],
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-13T21:46:07.137936+00:00",
+        "complete_pagination": true,
+        "records": 860
+      },
+      "discussions": {
+        "fetched_at": "2026-10-13T21:46:15.079923+00:00",
+        "complete_pagination": true,
+        "records": 32
+      }
+    },
+    "local_records": 325,
+    "warnings": []
+  },
+  "pre_submission": {
+    "searched_at": "2026-10-13T22:18:53.601924+00:00",
+    "terms": [
+      "prefix norm",
+      "signed prefix",
+      "unitary",
+      "formal interface"
+    ],
+    "coverage": {
+      "open_prs": {
+        "fetched_at": "2026-10-13T22:18:44.696720+00:00",
+        "complete_pagination": true,
+        "records": 800
+      },
+      "discussions": {
+        "fetched_at": "2026-10-13T22:18:53.568634+00:00",
+        "complete_pagination": true,
+        "records": 51
+      }
+    },
+    "local_records": 327,
+    "warnings": []
+  },
+  "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.",
+  "nearest_work": [
+    {
+      "number": 1282,
+      "title": "Research audit: signed prefixes give 18/21-bit local bounds for selected PR1094",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1282",
+      "head": "851e5232f7c9e105fb6e8f3a7be7a070e7524012",
+      "updated_at": "2026-10-13T21:44:02Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Explicit predecessor and formalization handoff: written unitary norm argument plus selected finite row/Horner replay. This package formalizes the quantified implication on the existing Lean semantics and deliberately leaves the concrete row certificate external."
+    },
+    {
+      "number": 821,
+      "title": "Research audit: 286-to-160-bit prefix estimate for pinned #626 (no new kappa)",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/821",
+      "head": "6b832a6ba4dce8dd6e2fb0897dd4543364b932f8",
+      "updated_at": "2026-10-13T06:25:21Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Written replica-level norm estimate for historical PR626; different precision layer and no Lean prefix-norm theorem. Its retained local envelope is not recomputed here."
+    },
+    {
+      "number": 1086,
+      "title": "Formalize source-bound CK cleanup-prefix scalar reordering in Lean",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1086",
+      "head": "89a2dac3e8f84703110e00a231079c96fa4a9dd3",
+      "updated_at": "2026-10-13T17:51:15Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Lean scalar cleanup reordering with source-bound historical finite instance; no norm-preservation or component-store theorem."
+    },
+    {
+      "number": 1295,
+      "title": "Conditional precision audit: commuting intervals lower PR1054's rounded-word budget",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1295",
+      "head": "3a6773708f0d73f7dbee164f4c6e7658b0b41509",
+      "updated_at": "2026-10-13T21:55:39Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Concurrent conditional rounded dirty-word precision substitution using commuting intervals; different recursion and no proof-assistant formalization."
+    },
+    {
+      "number": 1294,
+      "title": "Independent verification: universal dirty phase identities with four explicit invariants",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1294",
+      "head": "03025ca1d51091a9525203000e77dacccfa6a70d",
+      "updated_at": "2026-10-13T21:52:52Z",
+      "draft": false,
+      "state": "open",
+      "distinction": "Concurrent universal noncommutative phase identities for the dirty-word interval argument; different algebraic obligations and explicitly not a proof-assistant formalization."
+    }
+  ],
+  "existing_formal_source": {
+    "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean",
+    "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8",
+    "distinction": "Imports the original conjugation theorem and event semantics unchanged; adds normed-space and partial-store corollaries. HPE PROOF.md supplies orientation, not an additional imported Lean axiom."
+  }
+}
diff --git a/research/lean-unitary-prefix-norm/PrefixNorm.lean b/research/lean-unitary-prefix-norm/PrefixNorm.lean
new file mode 100644
index 0000000000..4b4e9251bb
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/PrefixNorm.lean
@@ -0,0 +1,180 @@
+/-
+Prefix norm corollaries for the existing Lemma G stream semantics.
+Gareth Davidson, with substantial OpenAI Codex assistance. Apache-2.0.
+The conjugation theorem and Event/Stream definitions are credited imports.
+-/
+import LemmaG.Stream
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.NormNum
+
+open scoped BigOperators
+
+namespace PrefixNorm
+
+open LemmaG LemmaG.Stream
+
+section Labelled
+
+variable {ι Λ K M : Type*} [Fintype ι] [DecidableEq ι]
+variable [NormedField K] [NormedAddCommGroup M] [NormedSpace K M]
+
+omit [Fintype ι] [NormedField K] in
+/-- A prefix inherits the actual source's well-labelled condition. -/
+theorem wellLabelled_take (es : List (Event ι Λ K)) (l : ι → Λ)
+    (hw : WellLabelled es l) (k : ℕ) : WellLabelled (es.take k) l := by
+  have h := (wellLabelled_append (es.take k) (es.drop k) l).mp (by simpa using hw)
+  exact h.1
+
+omit [Fintype ι] [DecidableEq ι] in
+/-- Exact recipes are inherited by prefixes; no new event model is introduced. -/
+theorem recipesExact_take (T : Λ → M ≃ₗ[K] M) (rec : Λ → Λ → M → M)
+    (es : List (Event ι Λ K)) (hr : RecipesExact T rec es) (k : ℕ) :
+    RecipesExact T rec (es.take k) := by
+  intro r A B hm v
+  exact hr r A B (List.mem_of_mem_take hm) v
+
+/-- Norm preservation of a linear equivalence also controls its inverse. -/
+theorem inverse_norm (T : Λ → M ≃ₗ[K] M)
+    (hT : ∀ a x, ‖T a x‖ = ‖x‖) (a : Λ) (x : M) : ‖(T a).symm x‖ = ‖x‖ := by
+  simpa using (hT a ((T a).symm x)).symm
+
+/-- Weighted row estimate, on the imported physical semantics and scalar matrix. -/
+theorem weighted_row (T : Λ → M ≃ₗ[K] M) (rec : Λ → Λ → M → M)
+    (es : List (Event ι Λ K)) (l : ι → Λ) (x : ι → M) (budget : ι → ℝ)
+    (hT : ∀ a v, ‖T a v‖ = ‖v‖) (hr : RecipesExact T rec es)
+    (hw : WellLabelled es l) (hx : ∀ j, ‖x j‖ ≤ budget j) (r : ι) :
+    ‖physRun rec es x r‖ ≤ ∑ j, ‖S es r j‖ * budget j := by
+  rw [conj_matrix T rec es l x hr hw r, hT]
+  calc
+    ‖∑ j, S es r j • (T (l j)).symm (x j)‖
+        ≤ ∑ j, ‖S es r j • (T (l j)).symm (x j)‖ := norm_sum_le _ _
+    _ = ∑ j, ‖S es r j‖ * ‖x j‖ := by
+      apply Finset.sum_congr rfl
+      intro j _
+      rw [norm_smul, inverse_norm T hT]
+    _ ≤ ∑ j, ‖S es r j‖ * budget j := by
+      exact Finset.sum_le_sum fun j _ => mul_le_mul_of_nonneg_left (hx j) (norm_nonneg _)
+
+/-- All finite words and all prefix lengths, including k beyond the word length. -/
+theorem weighted_prefix (T : Λ → M ≃ₗ[K] M) (rec : Λ → Λ → M → M)
+    (es : List (Event ι Λ K)) (l : ι → Λ) (x : ι → M) (budget : ι → ℝ)
+    (hT : ∀ a v, ‖T a v‖ = ‖v‖) (hr : RecipesExact T rec es)
+    (hw : WellLabelled es l) (hx : ∀ j, ‖x j‖ ≤ budget j) (k : ℕ) (r : ι) :
+    ‖physRun rec (es.take k) x r‖ ≤ ∑ j, ‖S (es.take k) r j‖ * budget j := by
+  exact weighted_row T rec (es.take k) l x budget hT (recipesExact_take T rec es hr k)
+    (wellLabelled_take es l hw k) hx r
+
+/-- Empty private inputs cost zero. The signed row is restricted to actual inputs. -/
+theorem supported_prefix (T : Λ → M ≃ₗ[K] M) (rec : Λ → Λ → M → M)
+    (es : List (Event ι Λ K)) (l : ι → Λ) (x : ι → M) (active : Finset ι) (B : ℝ)
+    (hT : ∀ a v, ‖T a v‖ = ‖v‖) (hr : RecipesExact T rec es) (hw : WellLabelled es l)
+    (hx : ∀ j ∈ active, ‖x j‖ ≤ B) (hz : ∀ j ∉ active, x j = 0) (k : ℕ) (r : ι) :
+    ‖physRun rec (es.take k) x r‖ ≤ (∑ j ∈ active, ‖S (es.take k) r j‖) * B := by
+  have hi : ∀ j, ‖x j‖ ≤ if j ∈ active then B else 0 := by
+    intro j
+    by_cases h : j ∈ active
+    · simpa [h] using hx j h
+    · simp [h, hz j h]
+  have bound := weighted_prefix T rec es l x (fun j => if j ∈ active then B else 0)
+    hT hr hw hi k r
+  simpa [mul_ite, Finset.sum_mul] using bound
+
+/-- A persistent-column prefix certificate supplies one uniform physical bound. -/
+theorem supported_certificate (T : Λ → M ≃ₗ[K] M) (rec : Λ → Λ → M → M)
+    (es : List (Event ι Λ K)) (l : ι → Λ) (x : ι → M) (active : Finset ι) (B L : ℝ)
+    (hT : ∀ a v, ‖T a v‖ = ‖v‖) (hr : RecipesExact T rec es) (hw : WellLabelled es l)
+    (hB : 0 ≤ B) (hx : ∀ j ∈ active, ‖x j‖ ≤ B) (hz : ∀ j ∉ active, x j = 0)
+    (hrows : ∀ k r, (∑ j ∈ active, ‖S (es.take k) r j‖) ≤ L) (k : ℕ) (r : ι) :
+    ‖physRun rec (es.take k) x r‖ ≤ L * B := by
+  exact (supported_prefix T rec es l x active B hT hr hw hx hz k r).trans
+    (mul_le_mul_of_nonneg_right (hrows k r) hB)
+
+end Labelled
+
+section PartialStore
+
+variable {ν 𝕜 : Type*} [Fintype ν] [DecidableEq ν] [RCLike 𝕜]
+
+/-- A subset of coordinates has been written; the complement still holds the old value. -/
+def splice (written : Finset ν) (old new : EuclideanSpace 𝕜 ν) : EuclideanSpace 𝕜 ν :=
+  WithLp.toLp 2 (fun i => if i ∈ written then new i else old i)
+
+/-- Actual Euclidean norm, not the max norm of an unwrapped Pi type. -/
+theorem splice_sq (written : Finset ν) (old new : EuclideanSpace 𝕜 ν) :
+    ‖splice written old new‖ ^ 2 ≤ ‖old‖ ^ 2 + ‖new‖ ^ 2 := by
+  rw [PiLp.norm_sq_eq_of_L2, PiLp.norm_sq_eq_of_L2, PiLp.norm_sq_eq_of_L2,
+      ← Finset.sum_add_distrib]
+  apply Finset.sum_le_sum
+  intro i _
+  change ‖if i ∈ written then new i else old i‖ ^ 2 ≤ ‖old i‖ ^ 2 + ‖new i‖ ^ 2
+  by_cases h : i ∈ written
+  · simp only [if_pos h]
+    exact le_add_of_nonneg_left (sq_nonneg _)
+  · simp only [if_neg h]
+    exact le_add_of_nonneg_right (sq_nonneg _)
+
+/-- Explicit factor-two squared allowance for partially stored values. -/
+theorem splice_uniform (written : Finset ν) (old new : EuclideanSpace 𝕜 ν) (L : ℝ)
+    (hL : 0 ≤ L) (ho : ‖old‖ ≤ L) (hn : ‖new‖ ≤ L) :
+    ‖splice written old new‖ ^ 2 ≤ 2 * L ^ 2 := by
+  have ho2 : ‖old‖ ^ 2 ≤ L ^ 2 := (sq_le_sq₀ (norm_nonneg _) hL).mpr ho
+  have hn2 : ‖new‖ ^ 2 ≤ L ^ 2 := (sq_le_sq₀ (norm_nonneg _) hL).mpr hn
+  nlinarith [splice_sq written old new]
+
+/-- A rational/integer squared guard yields a strict binary precision envelope. -/
+theorem splice_bits (written : Finset ν) (old new : EuclideanSpace 𝕜 ν) (L : ℝ) (b : ℕ)
+    (hL : 0 ≤ L) (ho : ‖old‖ ≤ L) (hn : ‖new‖ ≤ L)
+    (hbits : 2 * L ^ 2 < (2 : ℝ) ^ (2 * b)) :
+    ‖splice written old new‖ < (2 : ℝ) ^ b := by
+  have hp : 0 ≤ (2 : ℝ) ^ b := by positivity
+  apply (sq_lt_sq₀ (norm_nonneg _) hp).mp
+  have he : ((2 : ℝ) ^ b) ^ 2 = (2 : ℝ) ^ (2 * b) := by rw [← pow_mul, Nat.mul_comm]
+  rw [he]
+  exact (splice_uniform written old new L hL ho hn).trans_lt hbits
+
+end PartialStore
+
+section ComplexComponents
+
+variable {ν : Type*} [Fintype ν] [DecidableEq ν]
+
+/-- Real and imaginary components can have independent completed-write masks. -/
+def components (realDone imagDone : Finset ν) (old new : EuclideanSpace ℂ ν) :
+    EuclideanSpace ℂ ν := WithLp.toLp 2 (fun i =>
+      ⟨if i ∈ realDone then (new i).re else (old i).re,
+       if i ∈ imagDone then (new i).im else (old i).im⟩)
+
+/-- Direct complex half-store bound, without assuming a realification isometry. -/
+theorem components_sq (realDone imagDone : Finset ν) (old new : EuclideanSpace ℂ ν) :
+    ‖components realDone imagDone old new‖ ^ 2 ≤ ‖old‖ ^ 2 + ‖new‖ ^ 2 := by
+  rw [PiLp.norm_sq_eq_of_L2, PiLp.norm_sq_eq_of_L2, PiLp.norm_sq_eq_of_L2,
+      ← Finset.sum_add_distrib]
+  apply Finset.sum_le_sum
+  intro i _
+  simp only [Complex.sq_norm, Complex.normSq_apply, components, PiLp.toLp_apply]
+  split_ifs <;> nlinarith [sq_nonneg (old i).re, sq_nonneg (old i).im,
+                          sq_nonneg (new i).re, sq_nonneg (new i).im]
+
+/-- A uniform bound on either complex endpoint controls any component write order. -/
+theorem components_uniform (realDone imagDone : Finset ν) (old new : EuclideanSpace ℂ ν)
+    (L : ℝ) (hL : 0 ≤ L) (ho : ‖old‖ ≤ L) (hn : ‖new‖ ≤ L) :
+    ‖components realDone imagDone old new‖ ^ 2 ≤ 2 * L ^ 2 := by
+  have ho2 : ‖old‖ ^ 2 ≤ L ^ 2 := (sq_le_sq₀ (norm_nonneg _) hL).mpr ho
+  have hn2 : ‖new‖ ^ 2 ≤ L ^ 2 := (sq_le_sq₀ (norm_nonneg _) hL).mpr hn
+  nlinarith [components_sq realDone imagDone old new]
+
+/-- Strict bit envelope for independently written real/imaginary coordinates. -/
+theorem components_bits (realDone imagDone : Finset ν) (old new : EuclideanSpace ℂ ν)
+    (L : ℝ) (b : ℕ) (hL : 0 ≤ L) (ho : ‖old‖ ≤ L) (hn : ‖new‖ ≤ L)
+    (hbits : 2 * L ^ 2 < (2 : ℝ) ^ (2 * b)) :
+    ‖components realDone imagDone old new‖ < (2 : ℝ) ^ b := by
+  have hp : 0 ≤ (2 : ℝ) ^ b := by positivity
+  apply (sq_lt_sq₀ (norm_nonneg _) hp).mp
+  have he : ((2 : ℝ) ^ b) ^ 2 = (2 : ℝ) ^ (2 * b) := by rw [← pow_mul, Nat.mul_comm]
+  rw [he]
+  exact (components_uniform realDone imagDone old new L hL ho hn).trans_lt hbits
+
+end ComplexComponents
+
+end PrefixNorm
diff --git a/research/lean-unitary-prefix-norm/PrefixNorm/Examples.lean b/research/lean-unitary-prefix-norm/PrefixNorm/Examples.lean
new file mode 100644
index 0000000000..bea1ce4085
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/PrefixNorm/Examples.lean
@@ -0,0 +1,159 @@
+/-
+Nonvacuous instances and hypothesis-boundary witnesses for PrefixNorm.
+Gareth Davidson, with substantial OpenAI Codex assistance. Apache-2.0.
+-/
+import PrefixNorm
+import Mathlib.Tactic.FinCases
+
+open scoped BigOperators
+open LemmaG LemmaG.Stream
+
+noncomputable section
+
+namespace PrefixNorm.Examples
+
+abbrev Reg := Fin 2
+
+def labels (_ : Reg) : Bool := false
+
+def input (r : Reg) : ℝ := if r = 0 then 1 else 0
+
+def phases : Bool → ℝ ≃ₗ[ℝ] ℝ
+  | false => LinearEquiv.refl ℝ ℝ
+  | true => LinearEquiv.neg ℝ
+
+def recipe (a b : Bool) (x : ℝ) : ℝ := phases b ((phases a).symm x)
+
+theorem phases_norm (a : Bool) (x : ℝ) : ‖phases a x‖ = ‖x‖ := by
+  cases a <;> simp [phases]
+
+theorem recipe_exact (es : List (Event Reg Bool ℝ)) : RecipesExact phases recipe es := by
+  intro r A B hm x
+  rfl
+
+def goodWord : List (Event Reg Bool ℝ) :=
+  [.copy 1 0 false, .relabel 0 false true, .relabel 1 false true,
+   .add 0 1 (-1), .add 0 1 1, .relabel 0 true false, .clear 1 false]
+
+theorem good_labelled : WellLabelled goodWord labels := by
+  norm_num [goodWord, WellLabelled, Event.Admissible, Event.lab, labels, Function.update_apply]
+
+/-- The new all-prefix theorem actually applies to a word with nonidentity labels. -/
+theorem good_prefix_bound (k : ℕ) (r : Reg) :
+    ‖physRun recipe (goodWord.take k) input r‖ ≤ ‖S (goodWord.take k) r 0‖ := by
+  have hx : ∀ j ∈ ({0} : Finset Reg), ‖input j‖ ≤ (1 : ℝ) := by
+    intro j hj
+    have h : j = 0 := by simpa using hj
+    subst j
+    norm_num [input]
+  have hz : ∀ j ∉ ({0} : Finset Reg), input j = 0 := by
+    intro j hj
+    simp_all [input]
+  simpa using supported_prefix phases recipe goodWord labels input {0} 1 phases_norm
+    (recipe_exact goodWord) good_labelled hx hz k r
+
+theorem good_cancellation_cut : physRun recipe (goodWord.take 4) input 0 = 0 := by
+  norm_num [goodWord, physRun, Event.phys, input, recipe, phases, Function.update_apply]
+
+def badWord : List (Event Reg Bool ℝ) :=
+  [.copy 1 0 false, .relabel 1 false true, .add 0 1 (-1),
+   .add 0 1 1, .relabel 1 true false, .clear 1 false]
+
+theorem bad_not_labelled : ¬ WellLabelled badWord labels := by
+  norm_num [badWord, WellLabelled, Event.Admissible, Event.lab, labels, Function.update_apply]
+
+/-- Unitary exact recipes and a restored endpoint do not replace label admissibility. -/
+theorem bad_cut : physRun recipe (badWord.take 3) input 0 = 2 ∧
+    S (badWord.take 3) (0 : Reg) 0 = 0 := by
+  norm_num [badWord, S, scalRun, physRun, Event.scal, Event.phys, input, recipe, phases,
+            Function.update_apply, Pi.single_apply]
+
+theorem bad_endpoint : physRun recipe badWord input = input := by
+  funext r
+  fin_cases r <;>
+    norm_num [badWord, physRun, Event.phys, input, recipe, phases, Function.update_apply]
+
+/-- Each actual recipe preserves norms, but one reverse edge is not the labelled inverse. -/
+def asymmetricRecipe (a b : Bool) (x : ℝ) : ℝ :=
+  if a = false ∧ b = true then -x else x
+
+def wrongRecipeWord : List (Event Reg Bool ℝ) :=
+  [.copy 1 0 false, .relabel 1 false true, .relabel 1 true false, .add 0 1 (-1)]
+
+theorem asymmetric_preserves_norm (a b : Bool) (x : ℝ) :
+    ‖asymmetricRecipe a b x‖ = ‖x‖ := by
+  cases a <;> cases b <;> simp [asymmetricRecipe]
+
+theorem wrong_recipe_labelled : WellLabelled wrongRecipeWord labels := by
+  norm_num [wrongRecipeWord, WellLabelled, Event.Admissible, Event.lab, labels, Function.update_apply]
+
+theorem wrong_recipe_not_exact : ¬ RecipesExact phases asymmetricRecipe wrongRecipeWord := by
+  intro h
+  have bad := h 1 true false (by simp [wrongRecipeWord]) (1 : ℝ)
+  norm_num [asymmetricRecipe, phases] at bad
+
+theorem wrong_recipe_cut : physRun asymmetricRecipe wrongRecipeWord input 0 = 2 ∧
+    S wrongRecipeWord (0 : Reg) 0 = 0 := by
+  norm_num [wrongRecipeWord, physRun, Event.phys, S, scalRun, Event.scal, input,
+            asymmetricRecipe, Function.update_apply, Pi.single_apply]
+
+/-- An exact invertible label can nevertheless amplify norms. -/
+def eight : ℝ ≃ₗ[ℝ] ℝ where
+  toFun x := 8 * x
+  invFun x := x / 8
+  left_inv x := by dsimp; ring
+  right_inv x := by dsimp; ring
+  map_add' x y := by ring
+  map_smul' x y := by simp only [RingHom.id_apply, smul_eq_mul]; ring
+
+def largeLabels : Bool → ℝ ≃ₗ[ℝ] ℝ
+  | false => LinearEquiv.refl ℝ ℝ
+  | true => eight
+
+def largeRecipe (a b : Bool) (x : ℝ) : ℝ := largeLabels b ((largeLabels a).symm x)
+
+def loop : List (Event Reg Bool ℝ) := [.relabel 0 false true, .relabel 0 true false]
+
+theorem loop_labelled : WellLabelled loop labels := by
+  norm_num [loop, WellLabelled, Event.Admissible, Event.lab, labels, Function.update_apply]
+
+theorem loop_exact : RecipesExact largeLabels largeRecipe loop := by
+  intro r A B hm x
+  rfl
+
+theorem eight_not_norm_preserving : ‖largeLabels true (1 : ℝ)‖ ≠ ‖(1 : ℝ)‖ := by
+  norm_num [largeLabels, eight]
+
+theorem loop_cut : physRun largeRecipe (loop.take 1) input 0 = 8 ∧
+    S (loop.take 1) (0 : Reg) 0 = 1 := by
+  norm_num [loop, physRun, Event.phys, S, scalRun, Event.scal, input,
+            largeRecipe, largeLabels, eight, Function.update_apply, Pi.single_apply]
+
+theorem loop_endpoint : physRun largeRecipe loop input = input := by
+  funext r
+  fin_cases r <;>
+    norm_num [loop, physRun, Event.phys, input, largeRecipe, largeLabels, eight, Function.update_apply]
+
+def oldVector : EuclideanSpace ℂ Unit := WithLp.toLp 2 (fun _ => ⟨3/5, 4/5⟩)
+def newVector : EuclideanSpace ℂ Unit := WithLp.toLp 2 (fun _ => 1)
+
+/-- Both endpoints have unit norm; a real-first store has squared norm 41/25. -/
+theorem half_store_overshoot : ‖oldVector‖ ^ 2 = 1 ∧ ‖newVector‖ ^ 2 = 1 ∧
+    ‖components Finset.univ ∅ oldVector newVector‖ ^ 2 = 41/25 := by
+  norm_num [PiLp.norm_sq_eq_of_L2, oldVector, newVector, components,
+            Complex.sq_norm, Complex.normSq_apply, PiLp.toLp_apply]
+
+/-- Only a conditional numerical corollary: source row bounds are not assumed proved by Lean. -/
+theorem forward_bits_if {ν : Type*} [Fintype ν] [DecidableEq ν]
+    (reDone imDone : Finset ν) (old new : EuclideanSpace ℂ ν)
+    (ho : ‖old‖ ≤ 131088) (hn : ‖new‖ ≤ 131088) :
+    ‖components reDone imDone old new‖ < (2 : ℝ) ^ 18 := by
+  exact components_bits reDone imDone old new 131088 18 (by norm_num) ho hn (by norm_num)
+
+theorem backward_bits_if {ν : Type*} [Fintype ν] [DecidableEq ν]
+    (reDone imDone : Finset ν) (old new : EuclideanSpace ℂ ν)
+    (ho : ‖old‖ ≤ 1154896) (hn : ‖new‖ ≤ 1154896) :
+    ‖components reDone imDone old new‖ < (2 : ℝ) ^ 21 := by
+  exact components_bits reDone imDone old new 1154896 21 (by norm_num) ho hn (by norm_num)
+
+end PrefixNorm.Examples
diff --git a/research/lean-unitary-prefix-norm/PrintAxioms.lean b/research/lean-unitary-prefix-norm/PrintAxioms.lean
new file mode 100644
index 0000000000..92d551ff84
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/PrintAxioms.lean
@@ -0,0 +1,35 @@
+import PrefixNorm.Examples
+
+#print axioms PrefixNorm.wellLabelled_take
+#print axioms PrefixNorm.recipesExact_take
+#print axioms PrefixNorm.inverse_norm
+#print axioms PrefixNorm.weighted_row
+#print axioms PrefixNorm.weighted_prefix
+#print axioms PrefixNorm.supported_prefix
+#print axioms PrefixNorm.supported_certificate
+#print axioms PrefixNorm.splice_sq
+#print axioms PrefixNorm.splice_uniform
+#print axioms PrefixNorm.splice_bits
+#print axioms PrefixNorm.components_sq
+#print axioms PrefixNorm.components_uniform
+#print axioms PrefixNorm.components_bits
+#print axioms PrefixNorm.Examples.phases_norm
+#print axioms PrefixNorm.Examples.recipe_exact
+#print axioms PrefixNorm.Examples.good_labelled
+#print axioms PrefixNorm.Examples.good_prefix_bound
+#print axioms PrefixNorm.Examples.good_cancellation_cut
+#print axioms PrefixNorm.Examples.bad_not_labelled
+#print axioms PrefixNorm.Examples.bad_cut
+#print axioms PrefixNorm.Examples.bad_endpoint
+#print axioms PrefixNorm.Examples.asymmetric_preserves_norm
+#print axioms PrefixNorm.Examples.wrong_recipe_labelled
+#print axioms PrefixNorm.Examples.wrong_recipe_not_exact
+#print axioms PrefixNorm.Examples.wrong_recipe_cut
+#print axioms PrefixNorm.Examples.loop_labelled
+#print axioms PrefixNorm.Examples.loop_exact
+#print axioms PrefixNorm.Examples.eight_not_norm_preserving
+#print axioms PrefixNorm.Examples.loop_cut
+#print axioms PrefixNorm.Examples.loop_endpoint
+#print axioms PrefixNorm.Examples.half_store_overshoot
+#print axioms PrefixNorm.Examples.forward_bits_if
+#print axioms PrefixNorm.Examples.backward_bits_if
diff --git a/research/lean-unitary-prefix-norm/README.md b/research/lean-unitary-prefix-norm/README.md
new file mode 100644
index 0000000000..3877b961de
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/README.md
@@ -0,0 +1,174 @@
+# Formal unitary prefix bounds on the existing Lemma G semantics
+
+This package proves the quantified norm implication requested by
+[PR1282](https://github.com/CrocSwap/integer-mult-bounds/pull/1282), directly on
+the existing `LemmaG.Stream.Event`, `physRun`, `S`, `RecipesExact` and
+`WellLabelled`. It adds **13 core Lean theorems and 20 example theorems**,
+including partial real/imaginary stores and exact witnesses showing why the
+hypotheses matter. It imports the credited conjugation theorem without
+introducing a replacement event model.
+
+This is a scoped formal proof. Instantiating its hypotheses for the selected
+PR1094 compiler and finite row certificate remains open. The selected bound
+and production precision charge are unchanged.
+
+## Exact statements and boundary
+
+For any finite register type, normed field `K`, normed `K`-space `M`, finite
+event word `es`, initial labels `l`, and initial values `x`, assume:
+
+1. Every label map `T a : M ≃ₗ[K] M` preserves the norm.
+2. Every relabel executes exactly `T b ∘ (T a)⁻¹` (`RecipesExact`).
+3. The word satisfies the imported `WellLabelled` predicate, including matching
+   source/destination frames for ADD (`Event.Admissible`).
+4. `‖x j‖ ≤ budget j` for every initial register.
+
+Then `PrefixNorm.weighted_prefix` proves, for **every natural prefix length**
+`k` and register `r`,
+
+\[
+ \|\operatorname{physRun}(\mathrm{rec},\mathrm{es.take}\ k,x)_r\|
+ \leq \sum_j \|S(\mathrm{es.take}\ k)_{rj}\|\,\mathrm{budget}_j.
+\]
+
+The entries of `S` are the exact scalar shadow after cancellation. Admissibility
+and recipe exactness are proved to pass to prefixes. The proof uses the original
+`Stream.conj_matrix`, norm preservation of inverse label maps, and the triangle
+inequality. Prefix lengths beyond the word length are also covered.
+
+`supported_prefix` restricts the sum to active initial inputs of norm at most
+`B`, with every other initial register zero. Arbitrary bounded dirty inputs
+belong in the active set. `supported_certificate` takes the all-prefix row
+bound `L` as an **explicit hypothesis** and gives the uniform bound `L * B`
+for nonnegative `B`.
+
+For finite Euclidean vectors, `splice_sq` proves that any mixture of old and
+new whole coordinates has squared norm at most `‖old‖² + ‖new‖²`. For complex
+vectors, `components_sq` allows **independent real and imaginary write masks**
+and proves the same inequality directly in the complex Euclidean norm.
+Endpoints of norm at most `L ≥ 0` therefore give the squared bound `2 L²`;
+the exact guard `2 L² < 2^(2 b)` implies a strict norm bound `2^b`.
+
+These partial-store lemmas concern values made from the two specified
+endpoints. They do not automatically bound coefficient-building scratch or
+the internal instructions of a relabel recipe. Those states need their own
+representation and endpoint bounds before applying these lemmas.
+
+## Examples and hypothesis controls
+
+All examples use the same imported event semantics and are proved in Lean.
+See [THEOREMS.json](THEOREMS.json) for all 33 declarations.
+
+| Example | Exact evidence |
+| --- | --- |
+| Valid two-register word with identity/negation labels | `good_prefix_bound` applies the new theorem at every prefix; an intermediate cancellation gives zero. |
+| Mismatched ADD frames | Unitary exact recipes and a restored endpoint coexist with physical value `2` and scalar active-input coefficient `0` at an intermediate cut. `bad_not_labelled` proves the missing premise fails. |
+| Incorrect reverse recipe | Every recipe preserves norms and the word is well labelled, but the reverse map is wrong. `wrong_recipe_not_exact` and `wrong_recipe_cut` prove the failure and the `2` versus `0` discrepancy. |
+| Nonunitary labels | An exact, well-labelled relabel/inverse loop restores its input, but has physical value `8` against scalar coefficient `1` halfway through. |
+| Partial complex store | Old value `3/5 + 4i/5` and new value `1` each have squared norm `1`; writing the real component first gives squared norm `41/25`. |
+
+The verifier changes `2 L²` to `L²` in `components_uniform` in a disposable
+file and requires a Lean proof failure at that inequality. This is a meaningful
+failure control, not a completeness claim about proof tactics.
+
+`forward_bits_if` and `backward_bits_if` prove only the **conditional**
+arithmetic implications from endpoint bounds `131088` and `1154896` to
+component-store bounds `2^18` and `2^21`. Lean does not establish those endpoint
+premises for PR1094 here. Their numerical origin is PR1282 at
+`851e5232f7c9e105fb6e8f3a7be7a070e7524012`.
+
+## Reproduce and trust boundary
+
+From the repository root, with Python 3.12+ and elan/Lake on `PATH`:
+
+```sh
+python3 -I -B research/lean-unitary-prefix-norm/verify.py --work /tmp/unitary-prefix-norm
+```
+
+The command pins Lean **4.21.0**, Mathlib
+`308445d7985027f538e281e18df29ca16ede2ba3` and the complete inherited
+nine-package resolution in [lake-manifest.json](lake-manifest.json). It fetches
+the required Mathlib cache, copies `LemmaG/Stream.lean` byte-for-byte from its
+pinned source into a dedicated directory, then freshly compiles `LemmaG.Stream`,
+`PrefixNorm` and `PrefixNorm.Examples`. Dependency commits and clean tracked
+sources are checked before and after the build. Cached dependencies are reused;
+the package's own compiled files are removed before each build.
+
+Expected output:
+`PASS_LEAN_UNITARY_PREFIX_NORM core=13 examples=20 axioms=33 semantic_mutation=rejected`.
+The directory retains `TOOLCHAIN.log`, `BUILD.log`, `AXIOMS.log`, `CONTROL.log`
+and `RECEIPT.json`.
+Use a new empty directory or one created by this verifier. `--no-cache` uses
+already prepared dependencies; `--packages PATH` explicitly shares an existing
+`.lake/packages` directory into a new workspace. The frozen predecessor
+directory is never used as a build directory or edited.
+
+All 33 theorem axiom reports must match [AXIOMS.json](AXIOMS.json). Their union
+is exactly `{propext, Classical.choice, Quot.sound}`; there is no `sorryAx` or
+custom axiom. Acceptance relies on Lean's kernel, pinned Mathlib/dependency
+libraries and those standard axioms. The source policy scan rejects placeholders
+and external/native proof shortcuts as an additional guard; it is not a Lean
+parser or substitute for compilation.
+
+The generic registered hook runs **Python source/policy guards only**. Full
+Lean verification has a dedicated
+[workflow](../../.github/workflows/unitary-prefix-norm.yml).
+
+```sh
+python3 scripts/research_package.py --package research/lean-unitary-prefix-norm --check-only
+python3.12 scripts/research_package.py --package research/lean-unitary-prefix-norm
+python3 -I -B research/lean-unitary-prefix-norm/verify.py --source-only
+python3 -I -B research/lean-unitary-prefix-norm/test_verifier.py
+```
+
+[VALIDATION.md](VALIDATION.md) records observed commands and unrun obligations.
+[SOURCES.json](SOURCES.json) binds five live source inputs. The selected record
+and task catalogue are historical provenance at base
+`bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c`. The generic metadata checker needs
+full Git history; the direct source guard works on a minimal export.
+
+## Task and overlap
+
+Submitted as [PR1309](https://github.com/CrocSwap/integer-mult-bounds/pull/1309).
+
+[TASK.json](TASK.json) records the independent-verification assignment,
+OS nonce `0a4e57208d3517b8c57dc59d25be9445`, card `formal-interface-lemma`,
+scope key `636f26dec98e26b296e8` and refinement to PR1282's formalization
+follow-up. Coordination is in
+[Discussion1291](https://github.com/CrocSwap/integer-mult-bounds/discussions/1291).
+[OVERLAP.json](OVERLAP.json) gives fresh complete open-PR/Discussion coverage,
+nearby heads and search limits. PR1282 supplies the written norm argument and
+finite certificate; Lemma G supplies the formal conjugation theorem. This
+package connects the two in Lean. HPE residual-identity and cleanup-reordering
+formalizations address different statements. Search results do not prove novelty.
+
+## Open next questions
+
+1. **Bind a concrete emitted word and its row certificate to these theorems.**
+   This would formally connect the quantified theorem to a supplier program.
+   First encode one complete small word and prove that its imported `S` matches
+   an independently replayed rational row table. The blocker is a checked
+   translation of events, labels, recipes, coefficient scratch and every
+   relevant cut; the selected PR1094 word is not encoded here.
+2. **Connect partial stores to the full precision transfer.** This is needed
+   before using a smaller production charge. First formalize the actual
+   real/imaginary store schedule and establish its endpoint envelopes using
+   `components_bits`. Native recipes, roundoff, hosting, physical compiler/tape
+   accounting and all-size analytic transfer remain separate obligations.
+   This package does not assert a new multiplication theorem.
+
+## Credit
+
+Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance in proof,
+code, validation and writing; no independent human review is claimed. New work
+is Apache-2.0. PR1282 supplied the written norm argument and follow-up. Existing
+source and license notices are retained unchanged.
+
+The conjugation/scalar interface is credited to Zhihao Chen (PR425); the
+one-helper rule and wrappers to chafreaky (PR458); virtual entrance and
+normalization to Dugongue (PR471); the gauge construction, Lemma G and Python
+stage to DreamingOfClouds (PR484). This relies on the existing
+`research/e8-lemma-g-lean` formalization and Mathlib, with the Lean conventions
+of jamesyc's PR487/488. The selected-construction lineage remains credited in
+PR1282 and the selected review. The underlying conjugation theorem and norm
+argument are not claimed as new discoveries here.
diff --git a/research/lean-unitary-prefix-norm/SOURCES.json b/research/lean-unitary-prefix-norm/SOURCES.json
new file mode 100644
index 0000000000..ea4ce7f083
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/SOURCES.json
@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    },
+    {
+      "path": "research/e8-lemma-g-lean/LemmaG/Stream.lean",
+      "usage": "input",
+      "git_blob": "e89897190307a6f3fcfb858f8de00cc5a7f49b3e",
+      "sha256": "7138f4b859d0574a803e99401f05ef5e0ec9eeac0eb480775cd9b86595c365f8"
+    },
+    {
+      "path": "research/e8-lemma-g-lean/PROOF.md",
+      "usage": "input",
+      "git_blob": "6b24da0ab861902a6a3f65d9599bb9c0f964aa1c",
+      "sha256": "2a7d84a83d34495dcf46ff9241ee3d7ec18ffc7d49c5476ab15fe0834046f2a3"
+    },
+    {
+      "path": "research/e8-lemma-g-lean/lake-manifest.json",
+      "usage": "input",
+      "git_blob": "cda5516394595ce5e0ec67cd378b7d99af2bc95a",
+      "sha256": "a6082ec3e086d463f5eb3ba1befdbec45e868e2b328c6b066e25fcc82d1353f8"
+    },
+    {
+      "path": "research/e8-lemma-g-lean/lean-toolchain",
+      "usage": "input",
+      "git_blob": "980709bbbae28702ec58c368b84fdf6638093c63",
+      "sha256": "d24fed434d3b13adfaab57724a0a7f270ea8bf1c818b5ae5cf25cbce24dd685c"
+    },
+    {
+      "path": "research/hyperplane-end-lean/PROOF.md",
+      "usage": "input",
+      "git_blob": "a94a2ac168c088a1282ea411766bc859178620df",
+      "sha256": "1cbce5cf0ff0152f71e8ae7bef25841d1ce13010af248ff7209182d2328c21c9"
+    }
+  ]
+}
diff --git a/research/lean-unitary-prefix-norm/TASK.json b/research/lean-unitary-prefix-norm/TASK.json
new file mode 100644
index 0000000000..7b4f83a32f
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/TASK.json
@@ -0,0 +1,75 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 2,
+  "base_commit": "bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one small, precisely scoped interface lemma be formalized with its actual hypotheses?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/hyperplane-end-lean/PROOF.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read the exact hypotheses in the hyperplane-end proof and distinguish Lean theorems from finite supplier assumptions.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "State one missing boundary lemma in full before starting a proof-assistant build.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Formalize weighted and uniform norm bounds for every prefix of the existing LemmaG.Stream event semantics under norm-preserving label maps, exact recipes and well-labelled execution; formalize the coordinate partial-store bound with explicit hypotheses.",
+  "scope_change_reason": "Choose the formal-interface card, closing PR1282's explicit formalization handoff. Import the unchanged source definitions and theorem instead of rebuilding a parallel event model. The selected supplier's concrete all-prefix certificate and physical recipe binding remain separate.",
+  "bottleneck_link": "A checked quantified prefix-norm implication reduces one precision-transfer proof gap while retaining concrete compiler/hosting assumptions. No new kappa or supplier admission.",
+  "budget_minutes": 60,
+  "stop_rule": "One formal boundary package with explicit premise coverage, exact source/toolchain pins, axiom audit and nonvacuous examples. Do not extend into the full multiplication theorem or repeat the numeric certificate.",
+  "outcome": "completed",
+  "evidence": "Lean 4.21.0 freshly compiled unchanged LemmaG.Stream and the new PrefixNorm/Examples modules in three workspaces, including a fresh dependency setup with the final runner. All 13 core and 20 example theorems passed the complete standard-axiom audit. A false undercharged partial-store theorem was rejected. Seven Python guard tests passed, including read-only isolated optimized relocation and source corruption. See VALIDATION.md; this is a quantified boundary proof, not formalization of the selected finite certificate.",
+  "author": "Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance with proof, code, validation and writing; no subagents or independent human review.",
+  "open_questions": [
+    {
+      "question": "Can a concrete emitted word and its complete scalar-prefix certificate be bound to supported_certificate in Lean?",
+      "why_it_matters": "Closes the gap between the quantified theorem and an actual supplier program.",
+      "first_step": "Encode one small complete word and prove that its imported S agrees with an independently replayed rational row table.",
+      "blocked_by": "A checked translation of events, extended labels, exact recipes, coefficient scratch and every relevant cut; the selected PR1094 word is not encoded here."
+    },
+    {
+      "question": "Can the partial-component lemmas discharge the actual compiler store schedule in the full precision transfer?",
+      "why_it_matters": "A reduced production precision charge requires every physical intermediate and inherited transfer obligation.",
+      "first_step": "Formalize the real/imaginary store schedule and bind each old/new endpoint envelope to components_bits.",
+      "blocked_by": "Concrete native recipes, roundoff accumulation, hosting, physical compiler/tape accounting and all-size analytic transfer are outside this package."
+    }
+  ],
+  "assignment_nonce": "0a4e57208d3517b8c57dc59d25be9445",
+  "assigned_track": "independent-verification",
+  "assigned_scope_key": "636f26dec98e26b296e8",
+  "first_step": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+  "predecessor_pr": 1282,
+  "predecessor_head": "851e5232f7c9e105fb6e8f3a7be7a070e7524012",
+  "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/1309",
+  "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1291",
+  "mathematical_commit": "9dd1dab1b84d372037da88516b1eed1232579377"
+}
diff --git a/research/lean-unitary-prefix-norm/THEOREMS.json b/research/lean-unitary-prefix-norm/THEOREMS.json
new file mode 100644
index 0000000000..f85baac2e8
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/THEOREMS.json
@@ -0,0 +1,39 @@
+{
+  "core": [
+    "PrefixNorm.wellLabelled_take",
+    "PrefixNorm.recipesExact_take",
+    "PrefixNorm.inverse_norm",
+    "PrefixNorm.weighted_row",
+    "PrefixNorm.weighted_prefix",
+    "PrefixNorm.supported_prefix",
+    "PrefixNorm.supported_certificate",
+    "PrefixNorm.splice_sq",
+    "PrefixNorm.splice_uniform",
+    "PrefixNorm.splice_bits",
+    "PrefixNorm.components_sq",
+    "PrefixNorm.components_uniform",
+    "PrefixNorm.components_bits"
+  ],
+  "examples": [
+    "PrefixNorm.Examples.phases_norm",
+    "PrefixNorm.Examples.recipe_exact",
+    "PrefixNorm.Examples.good_labelled",
+    "PrefixNorm.Examples.good_prefix_bound",
+    "PrefixNorm.Examples.good_cancellation_cut",
+    "PrefixNorm.Examples.bad_not_labelled",
+    "PrefixNorm.Examples.bad_cut",
+    "PrefixNorm.Examples.bad_endpoint",
+    "PrefixNorm.Examples.asymmetric_preserves_norm",
+    "PrefixNorm.Examples.wrong_recipe_labelled",
+    "PrefixNorm.Examples.wrong_recipe_not_exact",
+    "PrefixNorm.Examples.wrong_recipe_cut",
+    "PrefixNorm.Examples.loop_labelled",
+    "PrefixNorm.Examples.loop_exact",
+    "PrefixNorm.Examples.eight_not_norm_preserving",
+    "PrefixNorm.Examples.loop_cut",
+    "PrefixNorm.Examples.loop_endpoint",
+    "PrefixNorm.Examples.half_store_overshoot",
+    "PrefixNorm.Examples.forward_bits_if",
+    "PrefixNorm.Examples.backward_bits_if"
+  ]
+}
diff --git a/research/lean-unitary-prefix-norm/VALIDATION.md b/research/lean-unitary-prefix-norm/VALIDATION.md
new file mode 100644
index 0000000000..fc8adaee20
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/VALIDATION.md
@@ -0,0 +1,118 @@
+# Observed verification, 2026-10-13
+
+The 13 core and 20 example theorems compiled with Lean 4.21.0
+(`6741444a63ee`, Linux x86_64, Release) and Mathlib
+`308445d7985027f538e281e18df29ca16ede2ba3`. All nine dependency commits and
+tracked source trees matched the inherited manifest before and after each
+successful full check. No warning or error occurred in the accepted builds.
+
+## Commands and receipts
+
+The local Lean distribution was on `PATH` as
+`/tmp/math-pass07-lean-download/lean-4.21.0-linux/bin`. Each command below
+freshly rebuilt `LemmaG.Stream`, `PrefixNorm` and `PrefixNorm.Examples`, printed
+all 33 axiom reports, and rejected the semantic partial-store mutation.
+
+```sh
+# Python 3.14.4; independently downloaded pinned dependencies/cache already present.
+python3 -I -B research/lean-unitary-prefix-norm/verify.py \
+  --work /tmp/math-pass25-lean-work --no-cache
+
+# Python 3.12.3; new workspace, explicitly shared immutable dependency sources.
+/usr/bin/python3.12 -I -O -B research/lean-unitary-prefix-norm/verify.py \
+  --work /tmp/math-pass25-lean-clean \
+  --packages /tmp/math-pass25-lean-work/.lake/packages --no-cache
+
+# Final runner, new empty workspace; clones all nine dependency repositories
+# and runs the targeted Mathlib cache command through the documented path.
+/usr/bin/python3.12 -I -B research/lean-unitary-prefix-norm/verify.py \
+  --work /tmp/math-pass25-lean-bootstrap-clean
+```
+
+All three successful runs produced:
+
+```text
+PASS_LEAN_UNITARY_PREFIX_NORM core=13 examples=20 axioms=33 semantic_mutation=rejected
+axioms_sha256=9e0091ab53901725b3f6b1cbd27171fbf3465138467b6cf025d7312e739c986b
+```
+
+The canonical complete `RECEIPT.json` SHA256 was identical in all three:
+`952d7066ce87a72d14c667d8743cd2a15d7779eee1bad0a6cbf43265f1b79b09`.
+Canonical encoding means `json.dumps(value, sort_keys=True,
+separators=(",", ":")).encode()`.
+
+The first attempted empty-workspace run exposed setup chatter before Lean's
+version line. The final runner parses exactly one exact-version report,
+retains `TOOLCHAIN.log`, and rejects wrong/prerelease/duplicate/missing reports.
+The third successful run above exercised that fix with real clone messages.
+It reused the installed Lean toolchain and the user's downloaded Mathlib
+archive cache; this was a fresh dependency workspace and proof build, not an
+empty-machine installation or an independent recheck of all Mathlib kernels.
+
+## Axioms, exact examples and semantic rejection
+
+`PrintAxioms.lean` covers every theorem listed in `THEOREMS.json`; the output
+matches `AXIOMS.json`. The union is exactly `propext`, `Classical.choice` and
+`Quot.sound`. No placeholder, extra axiom or native evaluator is used in the
+new proofs or imported Stream source.
+
+The examples prove a valid nonidentity-frame instance, mismatched-frame and
+incorrect-recipe discrepancies (`2` versus scalar coefficient `0`), a
+nonunitary relabel loop (`8` versus `1`, despite endpoint restoration), and
+the half-store squared norm `41/25` between endpoints of squared norm `1`.
+The two selected-number corollaries retain their endpoint bounds as premises.
+
+The verifier changes the conclusion of `components_uniform` from `2 * L^2`
+to `L^2` in `Undercharged.lean`. Lean exits nonzero with
+`linarith failed to find a contradiction` at the altered proof. A subsequent
+dependent theorem also reports a type mismatch; acceptance specifically
+requires the failure at the altered inequality. The original files are
+untouched. The independent `41/25` theorem explains why this strengthening
+is false, rather than relying on tactic failure as a mathematical argument.
+
+## Python guards and source integrity
+
+```sh
+python3 scripts/research_package.py --package research/lean-unitary-prefix-norm --check-only
+/usr/bin/python3.12 -I -B scripts/research_package.py --package research/lean-unitary-prefix-norm
+python3 -I -O -B research/lean-unitary-prefix-norm/verify.py --source-only
+python3 -I -O -B research/lean-unitary-prefix-norm/test_verifier.py
+python3 -I -B scripts/verify_selected_result.py
+git diff --check
+```
+
+Metadata/provenance/live pins passed. The registered Python 3.12 hook passed
+its source guard and seven tests. Direct isolated optimized Python 3.14.4
+source/test commands also passed. The generic hook intentionally requires
+Python 3.12 and rejects replay under 3.14; its metadata check is version
+independent. It is not the full Lean acceptance command.
+
+Tests cover nested comment handling and forbidden proof tokens; missing,
+duplicate and unapproved theorem axiom reports; exact-version parsing during
+cold setup; preservation of an unrecognized nonempty workspace; missing axiom
+requests; and source corruption after a successful read-only, minimal-export,
+isolated optimized relocation. File hashes are unchanged by that successful
+relocation. Critical verifier checks do not depend on Python `assert`.
+
+The selected-record integrity check retained
+`836330098538459/500000000000000000`. The working contribution adds only this
+package and its dedicated workflow. The refreshed main
+`bce54fb3f895cbe5cd4c0eb477c3afeed100190f` changed historical reconciliation
+evidence only; selected inputs, task guidance, catalogue and live proof inputs
+remain unchanged from the task base. Fresh overlap counts and exact nearby
+heads are in `OVERLAP.json`.
+
+## Coverage limits
+
+The full command proves the stated quantified lemmas using the original Lean
+event semantics. It does not encode the selected PR1094 word or check its
+concrete signed row table in Lean. It does not formalize the selected exact
+physical recipes, coefficient scratch implementation, native/Clifford
+execution, HPE/source-to-event translation, hosting, fixed-point roundoff,
+compiler/tape costs or all-size analytic transfer. The original supplier cold
+replay was not run for this formal lemma package; its selected files are
+unchanged. No reduced production precision or new kappa is claimed.
+
+The dedicated GitHub workflow is supplied, but these are local observations;
+hosted CI status must be read separately from the PR. No independent human or
+subagent review was performed.
diff --git a/research/lean-unitary-prefix-norm/VERIFY.json b/research/lean-unitary-prefix-norm/VERIFY.json
new file mode 100644
index 0000000000..60e69905d2
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/VERIFY.json
@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/e8-lemma-g-lean/LemmaG/Stream.lean",
+    "research/e8-lemma-g-lean/PROOF.md",
+    "research/e8-lemma-g-lean/lake-manifest.json",
+    "research/e8-lemma-g-lean/lean-toolchain",
+    "research/hyperplane-end-lean/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py",
+        "--source-only"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact live source/dependency/toolchain bindings, Lean declaration and axiom-request inventories, and source policy only. Does not run Lean or certify a mathematical theorem; use the dedicated workflow or full verify.py command."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/test_verifier.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Seven guard tests: nested-comment policy, axiom whitelist/completeness, preservation of unrecognized workspaces, read-only isolated optimized relocation, source corruption, exact Lean-version parsing during cold setup and missing axiom requests. Python guard validation only."
+    }
+  ]
+}
diff --git a/research/lean-unitary-prefix-norm/lake-manifest.json b/research/lean-unitary-prefix-norm/lake-manifest.json
new file mode 100644
index 0000000000..de69016f33
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/lake-manifest.json
@@ -0,0 +1,116 @@
+{
+  "version": "1.1.0",
+  "packagesDir": ".lake/packages",
+  "packages": [
+    {
+      "url": "https://github.com/leanprover-community/mathlib4",
+      "type": "git",
+      "subDir": null,
+      "scope": "",
+      "rev": "308445d7985027f538e281e18df29ca16ede2ba3",
+      "name": "mathlib",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v4.21.0",
+      "inherited": false,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/plausible",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "c4aa78186d388e50a436e8362b947bae125a2933",
+      "name": "plausible",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/LeanSearchClient",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
+      "name": "LeanSearchClient",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/import-graph",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "d07bd64f1910f1cc5e4cc87b6b9c590080e7a457",
+      "name": "importGraph",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/ProofWidgets4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "6980f6ca164de593cb77cd03d8eac549cc444156",
+      "name": "proofwidgets",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "v0.0.62",
+      "inherited": true,
+      "configFile": "lakefile.lean"
+    },
+    {
+      "url": "https://github.com/leanprover-community/aesop",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "8ff27701d003456fd59f13a9212431239d902aef",
+      "name": "aesop",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/quote4",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "e9c65db4823976353cd0bb03199a172719efbeb7",
+      "name": "Qq",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "master",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover-community/batteries",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover-community",
+      "rev": "8d2067bf518731a70a255d4a61b5c103922c772e",
+      "name": "batteries",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    },
+    {
+      "url": "https://github.com/leanprover/lean4-cli",
+      "type": "git",
+      "subDir": null,
+      "scope": "leanprover",
+      "rev": "7c6aef5f75a43ebbba763b44d535175a1b04c9e0",
+      "name": "Cli",
+      "manifestFile": "lake-manifest.json",
+      "inputRev": "main",
+      "inherited": true,
+      "configFile": "lakefile.toml"
+    }
+  ],
+  "name": "UnitaryPrefixNorm",
+  "lakeDir": ".lake"
+}
diff --git a/research/lean-unitary-prefix-norm/lakefile.toml b/research/lean-unitary-prefix-norm/lakefile.toml
new file mode 100644
index 0000000000..a9b1f7a46c
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/lakefile.toml
@@ -0,0 +1,13 @@
+name = "UnitaryPrefixNorm"
+defaultTargets = ["PrefixNorm", "PrefixNorm.Examples"]
+
+[[require]]
+name = "mathlib"
+git = "https://github.com/leanprover-community/mathlib4"
+rev = "v4.21.0"
+
+[[lean_lib]]
+name = "LemmaG"
+
+[[lean_lib]]
+name = "PrefixNorm"
diff --git a/research/lean-unitary-prefix-norm/lean-toolchain b/research/lean-unitary-prefix-norm/lean-toolchain
new file mode 100644
index 0000000000..980709bbba
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.21.0
diff --git a/research/lean-unitary-prefix-norm/test_verifier.py b/research/lean-unitary-prefix-norm/test_verifier.py
new file mode 100644
index 0000000000..74db553141
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/test_verifier.py
@@ -0,0 +1,100 @@
+#!/usr/bin/env python3
+"""Tests of proof-source and axiom guards; these do not replace the Lean build.
+
+Gareth Davidson, with OpenAI Codex assistance. Apache-2.0.
+"""
+import json
+from pathlib import Path
+import shutil
+import subprocess
+import sys
+import tempfile
+import unittest
+
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+import verify
+
+
+class GuardTests(unittest.TestCase):
+    def test_live_sources(self):
+        result = verify.source_check()
+        self.assertEqual((result["core_theorems"], result["example_theorems"]), (13, 20))
+
+    def test_nested_comments_and_forbidden_proofs(self):
+        text = "/- outer /- axiom hidden : False -/ sorry -/\n-- admit\ntheorem ok : True := by trivial"
+        verify.scan(text, "control")
+        for token in ("axiom fabricated : False", "theorem bad : False := by sorry",
+                      "set_option debug.skipKernelTC true"):
+            with self.assertRaises(verify.VerificationError):
+                verify.scan(text + "\n" + token, "control")
+        with self.assertRaises(verify.VerificationError):
+            verify.strip_comments("/- unclosed")
+
+    def test_axiom_whitelist_and_complete_coverage(self):
+        valid = "'A' depends on axioms: [propext, Quot.sound]\n'B' does not depend on any axioms\n"
+        self.assertEqual(verify.parse_axioms(valid, ["A", "B"]),
+                         {"A": ["Quot.sound", "propext"], "B": []})
+        for text in (valid.replace("Quot.sound", "sorryAx"), valid.splitlines()[0],
+                     valid + "'A' does not depend on any axioms\n"):
+            with self.assertRaises(verify.VerificationError):
+                verify.parse_axioms(text, ["A", "B"])
+
+    def test_exact_version_with_cold_setup_output(self):
+        version = "Lean (version 4.21.0, x86_64-unknown-linux-gnu, commit 6741444a63ee, Release)"
+        cold = "info: mathlib: cloning pinned dependency\n" + version + "\n"
+        self.assertEqual(verify.parse_lean_version(cold), version)
+        for bad in (cold.replace("4.21.0,", "4.21.1,"),
+                    cold.replace("4.21.0,", "4.21.0-rc1,"),
+                    cold + version + "\n", "info: download started\n"):
+            with self.assertRaises(verify.VerificationError):
+                verify.parse_lean_version(bad)
+
+    def test_unrecognized_workspace_is_preserved(self):
+        with tempfile.TemporaryDirectory() as path:
+            root = Path(path)
+            important = root / "user-file"
+            important.write_text("keep")
+            with self.assertRaises(verify.VerificationError):
+                verify.prepare(root)
+            self.assertEqual(important.read_text(), "keep")
+
+    def test_readonly_relocation_and_source_corruption(self):
+        with tempfile.TemporaryDirectory(prefix="norm proof source guard ") as path:
+            root = Path(path)
+            package = root / "research" / verify.HERE.name
+            shutil.copytree(verify.HERE, package, ignore=shutil.ignore_patterns("__pycache__", ".lake"))
+            for name in verify.INPUTS:
+                dest = root / name
+                dest.parent.mkdir(parents=True, exist_ok=True)
+                shutil.copyfile(verify.ROOT / name, dest)
+            files = [f for f in root.rglob("*") if f.is_file()]
+            before = {str(f.relative_to(root)): verify.sha(f.read_bytes()) for f in files}
+            try:
+                for f in files:
+                    f.chmod(0o444)
+                result = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py"),
+                                         "--source-only"], cwd="/tmp", capture_output=True, text=True)
+                self.assertEqual(result.returncode, 0, result.stdout + result.stderr)
+                self.assertIn("not_a_Lean_proof_check", result.stdout)
+                self.assertEqual(before, {str(f.relative_to(root)): verify.sha(f.read_bytes())
+                                          for f in root.rglob("*") if f.is_file()})
+            finally:
+                for f in files:
+                    f.chmod(0o644)
+            source = root / verify.SOURCE
+            source.write_text(source.read_text() + "\n-- source corruption control\n")
+            with self.assertRaisesRegex(verify.VerificationError, "source hash"):
+                verify.source_check(root, package)
+
+    def test_missing_axiom_request(self):
+        with tempfile.TemporaryDirectory() as path:
+            package = Path(path) / "package"
+            shutil.copytree(verify.HERE, package, ignore=shutil.ignore_patterns("__pycache__", ".lake"))
+            p = package / "PrintAxioms.lean"
+            p.write_text("\n".join(p.read_text().splitlines()[:-1]) + "\n")
+            with self.assertRaisesRegex(verify.VerificationError, "complete axiom audit requests"):
+                verify.source_check(verify.ROOT, package)
+
+
+if __name__ == "__main__":
+    unittest.main()
diff --git a/research/lean-unitary-prefix-norm/verify.py b/research/lean-unitary-prefix-norm/verify.py
new file mode 100644
index 0000000000..1d2dcd38c3
--- /dev/null
+++ b/research/lean-unitary-prefix-norm/verify.py
@@ -0,0 +1,248 @@
+#!/usr/bin/env python3
+"""Build the scoped Lean prefix-norm proofs and audit their exact source/axiom boundary.
+
+Gareth Davidson, with substantial OpenAI Codex assistance. Apache-2.0.
+Requires Lean/Lake 4.21.0. --source-only needs only Python and proves no theorem.
+The default build fetches the pinned Mathlib cache; --no-cache is for prepared
+dependencies. --work uses a dedicated marked workspace, never frozen sources.
+"""
+import argparse
+import hashlib
+import json
+from pathlib import Path
+import re
+import shutil
+import subprocess
+import sys
+import tempfile
+
+HERE = Path(__file__).resolve().parent
+ROOT = HERE.parent.parent
+SOURCE = "research/e8-lemma-g-lean/LemmaG/Stream.lean"
+INPUTS = {SOURCE, "research/e8-lemma-g-lean/PROOF.md",
+          "research/e8-lemma-g-lean/lake-manifest.json",
+          "research/e8-lemma-g-lean/lean-toolchain", "research/hyperplane-end-lean/PROOF.md"}
+LEAN_FILES = {"PrefixNorm.lean", "PrefixNorm/Examples.lean", "PrintAxioms.lean"}
+ALLOWED = {"propext", "Classical.choice", "Quot.sound"}
+FORBIDDEN = re.compile(r"\b(sorry|admit|axiom|native_decide|implemented_by|extern|unsafe|opaque|set_option)\b")
+MARKER = ".unitary-prefix-norm-workspace.json"
+OWNER = {"package": "lean-unitary-prefix-norm", "version": 1}
+CACHE_MODULES = ["Mathlib.Algebra.Module.Equiv.Defs", "Mathlib.Algebra.Module.Pi",
+                 "Mathlib.Algebra.BigOperators.Pi", "Mathlib.Algebra.Module.LinearMap.Basic",
+                 "Mathlib.LinearAlgebra.Span.Basic", "Mathlib.Analysis.InnerProductSpace.PiL2",
+                 "Mathlib.Tactic.Linarith", "Mathlib.Tactic.NormNum", "Mathlib.Tactic.FinCases"]
+
+
+class VerificationError(ValueError):
+    pass
+
+
+def require(condition, message):
+    if not condition:
+        raise VerificationError(message)
+
+
+def sha(data):
+    return hashlib.sha256(data).hexdigest()
+
+
+def encoded(value):
+    return json.dumps(value, sort_keys=True, separators=(",", ":")).encode()
+
+
+def strip_comments(source):
+    """Handle nested Lean block comments and line comments without swallowing code."""
+    out, i, depth = [], 0, 0
+    while i < len(source):
+        if source.startswith("/-", i):
+            depth += 1
+            i += 2
+        elif depth and source.startswith("-/", i):
+            depth -= 1
+            i += 2
+            out.append(" ")
+        elif depth:
+            i += 1
+        elif source.startswith("--", i):
+            end = source.find("\n", i)
+            i = len(source) if end < 0 else end
+        else:
+            out.append(source[i])
+            i += 1
+    require(depth == 0, "unclosed Lean comment")
+    return "".join(out)
+
+
+def scan(source, name):
+    match = FORBIDDEN.search(strip_comments(source))
+    require(match is None, "forbidden Lean token in " + name + (": " + match[0] if match else ""))
+
+
+def source_check(root=ROOT, package=HERE):
+    pins = json.loads((package / "SOURCES.json").read_text())
+    live = [x for x in pins["files"] if x["usage"] == "input"]
+    require(len(live) == len(INPUTS) and {x["path"] for x in live} == INPUTS, "mandatory input inventory")
+    for row in live:
+        require(sha((root / row["path"]).read_bytes()) == row["sha256"], "source hash: " + row["path"])
+    actual = {str(p.relative_to(package)) for p in package.rglob("*.lean") if ".lake" not in p.parts}
+    require(actual == LEAN_FILES, "Lean source inventory")
+    for name in sorted(LEAN_FILES):
+        scan((package / name).read_text(), name)
+    scan((root / SOURCE).read_text(), SOURCE)
+    index = json.loads((package / "THEOREMS.json").read_text())
+    names = index["core"] + index["examples"]
+    require(len(names) == len(set(names)) == 33, "theorem inventory")
+    for group, file, prefix in [("core", "PrefixNorm.lean", "PrefixNorm."),
+                                 ("examples", "PrefixNorm/Examples.lean", "PrefixNorm.Examples.")]:
+        parsed = [prefix + n for n in re.findall(r"^theorem (\w+)",
+                  strip_comments((package / file).read_text()), re.M)]
+        require(parsed == index[group], "declared theorem coverage: " + group)
+    printed = re.findall(r"^#print axioms (\S+)$", (package / "PrintAxioms.lean").read_text(), re.M)
+    require(printed == names, "complete axiom audit requests")
+    original = json.loads((root / "research/e8-lemma-g-lean/lake-manifest.json").read_text())
+    staged = json.loads((package / "lake-manifest.json").read_text())
+    original["name"] = "UnitaryPrefixNorm"
+    require(original == staged, "unchanged dependency resolution")
+    require((package / "lean-toolchain").read_bytes()
+            == (root / "research/e8-lemma-g-lean/lean-toolchain").read_bytes(), "toolchain pin")
+    require((package / "lean-toolchain").read_text().strip() == "leanprover/lean4:v4.21.0", "Lean version pin")
+    return dict(status="PASS_PREFIX_NORM_SOURCE_BINDINGS_ONLY", core_theorems=len(index["core"]),
+                example_theorems=len(index["examples"]), source_sha256={x["path"]: x["sha256"] for x in live},
+                lean_source_sha256={n: sha((package / n).read_bytes()) for n in sorted(LEAN_FILES)})
+
+
+def parse_axioms(output, names):
+    found = {}
+    for name, body in re.findall(r"'([\w.']+)' depends on axioms: \[([^\]]*)\]", output):
+        require(name not in found, "duplicate axiom report")
+        found[name] = sorted(a.strip() for a in body.split(",") if a.strip())
+    for name in re.findall(r"'([\w.']+)' does not depend on any axioms", output):
+        require(name not in found, "duplicate axiom report")
+        found[name] = []
+    require(set(found) == set(names), "incomplete/unexpected axiom reports")
+    for name, axioms in found.items():
+        require(set(axioms) <= ALLOWED, "unapproved theorem axiom: " + name)
+    return found
+
+
+def parse_lean_version(output):
+    # A fresh Lake workspace emits dependency-download messages before the
+    # version line. Require exactly one exact-version report, not quiet setup.
+    versions = [line.strip() for line in output.splitlines() if line.startswith("Lean (version ")]
+    require(len(versions) == 1 and
+            re.fullmatch(r"Lean \(version 4\.21\.0, [^\r\n]+\)", versions[0]) is not None,
+            "actual Lean version: " + output[-2000:])
+    return versions[0]
+
+
+def run(argv, work, timeout=300, expected_success=True):
+    process = subprocess.run(argv, cwd=work, text=True, stdout=subprocess.PIPE,
+                             stderr=subprocess.STDOUT, timeout=timeout)
+    if expected_success:
+        require(process.returncode == 0, "command failed: " + " ".join(map(str, argv)) + "\n" + process.stdout[-8000:])
+    return process
+
+
+def prepare(work, packages=None):
+    require(work.resolve() != ROOT.resolve() and work.resolve() != HERE.resolve(), "dedicated build workspace")
+    if work.exists() and any(work.iterdir()):
+        marker = work / MARKER
+        require(marker.is_file() and json.loads(marker.read_text()) == OWNER, "unrecognized nonempty workspace")
+    work.mkdir(parents=True, exist_ok=True)
+    (work / MARKER).write_text(json.dumps(OWNER) + "\n")
+    if packages is not None:
+        target = work / ".lake/packages"
+        target.parent.mkdir(parents=True, exist_ok=True)
+        require(not target.exists(), "dependency directory already exists")
+        require(packages.is_dir(), "shared dependency directory")
+        target.symlink_to(packages.resolve(), target_is_directory=True)
+    for name in LEAN_FILES | {"lakefile.toml", "lake-manifest.json", "lean-toolchain"}:
+        target = work / name
+        target.parent.mkdir(parents=True, exist_ok=True)
+        shutil.copyfile(HERE / name, target)
+    (work / "LemmaG").mkdir(exist_ok=True)
+    shutil.copyfile(ROOT / SOURCE, work / "LemmaG/Stream.lean")
+    (work / "LemmaG.lean").write_text("import LemmaG.Stream\n")
+    # Only this marked workspace's own compiled outputs are removed. Cached
+    # dependency libraries are retained; all new/imported local proofs rebuild.
+    output = work / ".lake/build"
+    if output.exists():
+        require(not output.is_symlink(), "local build output must not be a symlink")
+        shutil.rmtree(output)
+
+
+def dependency_check(work):
+    manifest = json.loads((HERE / "lake-manifest.json").read_text())
+    heads = {}
+    for package in manifest["packages"]:
+        path = work / ".lake/packages" / package["name"]
+        head = run(["git", "rev-parse", "HEAD"], path).stdout.strip()
+        require(head == package["rev"], "dependency commit: " + package["name"])
+        require(run(["git", "status", "--porcelain", "--untracked-files=no"], path).stdout == "",
+                "modified dependency source: " + package["name"])
+        heads[package["name"]] = head
+    return heads
+
+
+def full_check(work, no_cache, packages):
+    source = source_check()
+    prepare(work, packages)
+    version_output = run(["lake", "env", "lean", "--version"], work, timeout=600).stdout
+    (work / "TOOLCHAIN.log").write_text(version_output)
+    version = parse_lean_version(version_output)
+    if not no_cache:
+        run(["lake", "exe", "cache", "get", *CACHE_MODULES], work, timeout=900)
+    heads = dependency_check(work)
+    build = run(["lake", "build", "PrefixNorm", "PrefixNorm.Examples"], work, timeout=600)
+    require("warning:" not in build.stdout and "error:" not in build.stdout, "Lean build diagnostics")
+    (work / "BUILD.log").write_text(build.stdout)
+    require((work / "LemmaG/Stream.lean").read_bytes() == (ROOT / SOURCE).read_bytes(), "unchanged compiled Stream")
+    axioms = run(["lake", "env", "lean", "PrintAxioms.lean"], work, timeout=120).stdout
+    (work / "AXIOMS.log").write_text(axioms)
+    names = sum(json.loads((HERE / "THEOREMS.json").read_text()).values(), [])
+    checked = parse_axioms(axioms, names)
+    require(checked == json.loads((HERE / "AXIOMS.json").read_text()), "axiom dependency receipt")
+    # A semantically false strengthening of the partial-component theorem:
+    # replace 2*L^2 by L^2. Its proof must fail, as the 41/25 fixture predicts.
+    text = (HERE / "PrefixNorm.lean").read_text()
+    original = "‖components realDone imagDone old new‖ ^ 2 ≤ 2 * L ^ 2 := by"
+    require(text.count(original) == 1, "precision mutation target")
+    mutant = text.replace(original, "‖components realDone imagDone old new‖ ^ 2 ≤ L ^ 2 := by")
+    path = work / "Undercharged.lean"
+    path.write_text(mutant)
+    failure = run(["lake", "env", "lean", str(path)], work, timeout=120, expected_success=False)
+    require(failure.returncode != 0 and "linarith failed" in failure.stdout,
+            "undercharged partial-store theorem was not rejected for its proof")
+    (work / "CONTROL.log").write_text(failure.stdout)
+    path.unlink()
+    require(source_check() == source, "source changed during proof check")
+    require(dependency_check(work) == heads, "dependency changed during proof check")
+    receipt = dict(status="PASS_LEAN_UNITARY_PREFIX_NORM", lean_version=version,
+                   dependency_commits=heads, source=source, axioms=checked,
+                   undercharged_partial_store_rejected=True,
+                   freshly_built=["LemmaG.Stream", "PrefixNorm", "PrefixNorm.Examples"],
+                   scope="Quantified prefix and component-store lemmas on imported semantics; "
+                         "concrete selected event/row bindings and full physical/roundoff transfer remain open.")
+    (work / "RECEIPT.json").write_text(json.dumps(receipt, indent=2) + "\n")
+    print(receipt["status"], "core=13 examples=20 axioms=33 semantic_mutation=rejected")
+    print("axioms_sha256=" + sha(encoded(checked)))
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--source-only", action="store_true", help="bindings/policy only; does not run Lean")
+    parser.add_argument("--work", type=Path, help="dedicated persistent build directory")
+    parser.add_argument("--no-cache", action="store_true", help="reuse already available pinned dependencies")
+    parser.add_argument("--packages", type=Path, help="explicitly share an existing pinned dependency directory")
+    args = parser.parse_args()
+    if args.source_only:
+        print(source_check()["status"], "not_a_Lean_proof_check")
+    elif args.work:
+        full_check(args.work.resolve(), args.no_cache, args.packages)
+    else:
+        with tempfile.TemporaryDirectory(prefix="lean-prefix-norm-") as path:
+            full_check(Path(path), args.no_cache, args.packages)
+
+
+if __name__ == "__main__":
+    main()