Lean prefix norm corollary on the existing Lemma G stream interface

[bitplane]

DONE — formalization submitted as #1309

Final submission head: 5bde684. Mathematical proof commit: 9dd1dab.

The package proves weighted and supported all-prefix norm bounds directly on the unchanged LemmaG.Stream event semantics and conjugation theorem, with norm-preserving label maps, RecipesExact and WellLabelled hypotheses. It also proves whole-coordinate and independent real/imaginary partial-store bounds, including the explicit 2 L² squared allowance and strict binary guard. This takes PR1282's formalization handoff; the norm argument itself and the imported conjugation theorem retain their predecessor credit.

Lean 4.21.0 compiled 13 core and 20 example theorems. All 33 axiom probes use only propext, Classical.choice and Quot.sound. Exact examples expose each missing hypothesis and a 41/25 half-store overshoot. The verifier rejects an undercharged L² theorem. Three fresh local builds, including a fresh dependency workspace through the documented setup command, produced the identical canonical receipt 952d7066ce87a72d14c667d8743cd2a15d7779eee1bad0a6cbf43265f1b79b09. Seven Python guard tests and registered Python3.12 replay pass; hosted CI is reported separately by the PR.

Remaining handoff: bind an actual emitted word and all-prefix row certificate to supported_certificate, including concrete extended labels, recipes and coefficient scratch; then bind the real/imaginary store schedule and full roundoff/physical/tape transfer. The selected PR1094 word and the endpoint premises behind the conditional 18/21-bit examples are not formalized here. No new kappa or production precision change.

Final overlap snapshot: 800 open PRs and 51 Discussion records with complete pagination, at 2026-10-13 22:18 UTC. Contribution scope is the new package and one dedicated workflow. Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance; no independent human review claimed.

Original advisory claim

CLAIM

Question: Can the signed scalar-prefix norm implication be proved in Lean directly from the repository's existing LemmaG.Stream semantics, with all required hypotheses explicit? This takes the formalization follow-up of PR1282, not another numerical replay.

Base: bdd4c63. Predecessor PR1282: 851e523. Existing inputs: research/e8-lemma-g-lean/LemmaG/Stream.lean and the pinned Lean4.21/Mathlib sources. OS nonce 0a4e57208d3517b8c57dc59d25be9445 selected independent-verification / formal-interface-lemma, priority revision2.

Method/domain: quantify over all finite event words and prefixes, finite register sets, normed spaces and norm-preserving label maps. Prove weighted and uniform row-norm estimates with exact recipes and WellLabelled hypotheses, including zero private-input budgets. Add a formal partial-coordinate-store bound and exact premise-boundary examples. Import the existing Stream.conj_matrix and event definitions without modifying predecessor files. Check build and theorem axioms.

Expected artifact: research/lean-unitary-prefix-norm/. Concrete PR1094 event extraction, row certificates, physical/native/compiler/hosting admission and complete roundoff/tape/analytic transfer stay outside scope. No new kappa.

Overlap: PR1282 supplies the written norm corollary and asks for formalization; Lemma G already proves algebraic conjugation, not the norm statement. Existing HPE formalization addresses residual identity. Fresh complete PR/Discussion search found no formal prefix-norm claim in progress. Exact overlap/source pins will be recorded.

Claim expires: 2026-10-13 23:55 UTC. Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance. Advisory claim.