[bitplane]

Change and mathematical scope

This proves the quantified norm implication requested by PR1282 directly on the unchanged LemmaG.Stream event semantics. For every finite event word and prefix, norm-preserving label maps, exact relabel recipes and WellLabelled execution transfer the exact scalar row bound to the physical register norm. Zero private inputs are omitted from the active-input sum. An all-prefix row certificate remains an explicit premise.

The package also proves the Euclidean partial-store bound, including independent real/imaginary write masks: endpoints bounded by L imply squared norm at most 2 L², with a strict binary envelope from 2 L² < 2^(2b). The 13 core and 20 example theorems include exact witnesses for mismatched labels, incorrect recipes, nonunitary labels and a 41/25 partial-store overshoot.

This is a scoped formalization, not a new conjugation theorem or numeric replay. The selected PR1094 word, concrete row certificate, exact physical recipes, coefficient scratch implementation and full precision/analytic transfer are not instantiated in Lean. The 18/21-bit numerical examples explicitly assume their endpoint bounds. No selected record, production precision charge or kappa is changed.

Task and overlap

• Base: bdd4c63ac7c5d8a46ce070ba133df8d7ba9cb92c; refreshed main: bce54fb3f895cbe5cd4c0eb477c3afeed100190f. Relevant guidance, selected record and all five live source inputs are unchanged; the focused patch applies cleanly.
• Fresh OS nonce 0a4e57208d3517b8c57dc59d25be9445 selected independent-verification, card formal-interface-lemma, scope key 636f26dec98e26b296e8, priority revision 2. Scope is refined to the predecessor's explicit formalization follow-up.
• PR1282 at 851e5232f7c9e105fb6e8f3a7be7a070e7524012 supplies the written norm argument and finite selected-word evidence. This proves its quantified implication using the existing formal conj_matrix, rather than duplicating that argument as another audit.
• PR821 is a written replica-level bound; PR1086 proves scalar cleanup reordering. Concurrent PR1294/1295 address dirty-word phase identities/rounded precision. Exact heads and distinctions are in OVERLAP.json.
• Final overlap snapshot: 800 open PRs and 51 Discussion records, complete pagination, 2026-10-13 22:18 UTC. Bounded overlap evidence does not establish novelty. Claim/result thread: Lean prefix norm corollary on the existing Lemma G stream interface #1291 .

Only research/lean-unitary-prefix-norm/ and its dedicated CI workflow are added.

Validation

Full proof check, with elan/Lake available:

python3 -I -B research/lean-unitary-prefix-norm/verify.py --work /tmp/unitary-prefix-norm

Lean 4.21.0 and the exact Mathlib v4.21.0 dependency manifest are pinned. Three fresh local module builds, including one fresh dependency workspace running the documented setup path, gave the same receipt. All 33 axiom probes use only propext, Classical.choice and Quot.sound. The verifier rejects the deliberately false L² partial-store strengthening at its proof. Seven Python guard tests pass under Python 3.12 and direct isolated optimized 3.14, including read-only relocation, source corruption, missing/extra axioms and exact-version parsing amid setup messages.

python3.12 scripts/research_package.py --package research/lean-unitary-prefix-norm

The generic hook runs source/policy guards only. Full Lean builds have a dedicated workflow. Source/provenance checks, selected-record integrity and patch whitespace pass. These are local results; hosted CI is tracked separately. The original supplier cold replay and full native/compiler/roundoff/tape/analytic admission were not run for this lemma package.

Canonical full receipt SHA256: 952d7066ce87a72d14c667d8743cd2a15d7779eee1bad0a6cbf43265f1b79b09.

Credit

Gareth Davidson (@bitplane), with substantial OpenAI Codex assistance in proof, code, validation and writing; no independent human review is claimed. Apache-2.0; existing sources/notices are unchanged. Credit the existing Lemma G formalization, Zhihao Chen (PR425), chafreaky (PR458), Dugongue (PR471), DreamingOfClouds (PR484), jamesyc's PR487/488 conventions, Mathlib and the retained selected-construction lineage. PR1282 supplies the norm argument being formalized.

Open next questions

Bind one concrete emitted word and its rational row table to supported_certificate, then connect the actual component-store schedule and scratch bounds to the full precision transfer. The README/TASK give first steps and explicit blockers. Full details and observed commands: package README and validation.

[Mister-Meeseeks]

100-PR batch review at 5bde684f9189b59d1388c089ec5475fb5cf59565.

This remains open after scoped triage. Next review step: Lean contribution needs pinned dependency preparation, full module build, source binding and axiom/mutation checks. Python extraction alone is not formal acceptance; keep separate from selected theorem claims.

This is a specific continuation point, not a rejection or a request to redo already recorded checks. Completed local evidence is retained separately from outstanding whole-head obligations.

Batch review, attribution and evidence. Thank you for the contribution.