Lemma G of #484: clean proof and Lean 4 formalisation of its core

[DreamingOfClouds]

This PR gives Lemma G (entrance gauge: target-side compensation at nonzero frames, labelled targets, chain scatter) a clean,
self-contained proof and formalises its abstract core in Lean 4.

Lemma G is worth +1.80% of complex b under no-bank hosting:

word	complex b
Lemma-G-free path (kernel79 only, #500)	1.310216e-3
full gauge/kernel word (#496/#500)	1.333854e-3

#484 is not modified. This branch is stacked on #484's head and adds only research/e8-lemma-g-lean/.

What is proved (Lean 4.21.0 + Mathlib v4.21.0, the pin of formal/lean on main)

theorem LemmaG.Stream.conj_matrix (T : Λ → M ≃ₗ[K] M) (rec : Λ → Λ → M → M) (es : List (Event ι Λ K))
    (l : ι → Λ) (h : ι → M) (hrec : RecipesExact T rec es) (hw : WellLabelled es l) (r : ι) :
    physRun rec es h r = T (labRun es l r) (∑ s, S es r s • (T (l s)).symm (h s))

The theorem holds for every semiring K, every K-module M and every family of linear automorphisms T. Take any stream of relabel/add/scale/copy/clear events that is well labelled and whose relabels execute T_B T_A⁻¹. Then for every input it computes

h_r ↦ T_{λ¹_r}(Σ_s S_rs T_{λ⁰_s}⁻¹ h_s),

where the non-private columns of S are exactly what #484's rational scalar replay computes (S_rowform; the replay starts the private copies empty, and their columns drop out on inputs with empty private registers).

The other Lean results:

• Row lemmas (row_unit, row_pair). A unit row gives the block T_{λ¹}T_{λ⁰}⁻¹; for an entering helper this is the virtual entrance with its wrappers. A paired row gives T_{λ¹_r}(T_{λ⁰_r}⁻¹h_r + a·T_{λ⁰_s}⁻¹h_s).
• Schedule (emit_spec, comp_segment, centre_forward, centre_backward), proved for an abstract order with strictly monotone rank and instantiated for the subspaces of F₂⁹.
  • The compensation segment and the centre phase are well labelled as soon as the partners stay at their frames.
  • Under (b) and (c), every move is a strict nested ascent (or descent).
  • Each target ends at L_t = max ℰ_t.
• Accounting (paid_telescopes). Paid ranks telescope to rk λ¹ − rk λ⁰ per register.
• Bit-side entrance identities (Dbit_one_mul, Dbit_conj). D_I D_P = D_{I−P}, and conjugation by diag(g,g) for gᵀg = 1, for every P.

All theorems are general: there is no instance enumeration and no decide/native_decide. Lean proves the abstract core. The schedule lemmas are an a-priori route that is not instantiated on the emitted stream; the stream itself is checked in Python (below). Combining the Lean core with those checks gives that the data rows are W's and the mass identity mass(W) − Σ_j dim E_j. #print axioms reports only propext, Classical.choice and Quot.sound. verify.py builds the package, scans for sorry/axiom/native_decide, and checks every axiom report.

What stays checked in Python

The instance hypotheses on the emitted streams:

hypothesis	check	result
well-labelledness	#484 G0/G2/G3, plus the new code/check_extended_labels.py	0 violations on all four words, both orientations; 3 adapter mutants rejected on every word, 2 wrapper mutants on the wrapper words
exact transition recipes; the adapter/wrapper bridge	#484 I-tr on all 512 columns (recipes are linear circuits); one non-identity adapter per source and per target, all others identities (check_extended_labels.py)	2945/2945
the scalar identity S	#484 replay, all 800 columns	exact
endpoint labels	#484 G4	0 violations
accounting	#484 G2/G3/ACC	0 violations
#433's data-adapter identities	the new code/check_adapters.py, every port, all 512 columns, exact	0 failures on all four words

Why the extended-label check: #484 §2.1 left adapters and wrappers outside Lemma C as endpoint operators. Register-wise that is right. Each non-identity adapter and each wrapper is the first or last event on its register, and the adapters that sit mid-stream (headline forward: 550 entry, 672 exit) are all identities. So #484's description was imprecise but harmless. Lemma C as stated still needed an unwritten commutation step. The clean proof reads adapters and wrappers as relabel events of an extended label set (tag × frame), so the theorem covers the complete emitted stream, and the condition is checked directly.

With these hypotheses checked exhaustively, and Lemma A (#484 I-helper, exhaustive), the end-to-end identity holds for every input with empty private registers. #484's lg_e2e.py tested it on 814 sampled columns.

PROOF.md §5 lists the other clarifications:

• the relabel-source condition;
• the inherited facts behind "every input" (Split centres and source-basis reuse for conditional κ = 0.001120864952258278 #433's adapter identities, Lemma A);
• the minimal label condition;
• (a)–(d) are accounting-only;
• explicit side conditions;
• the kernel updates as an instance of the same emitter.

Reproduce

python3 research/e8-lemma-g-lean/verify.py                                   # Lean only: cache get + build + axioms
python3 research/e8-lemma-g-lean/verify.py --instances /abs/out/of/484/verify # plus the instance checks (numpy)

Credits

• κ = 1.048005508028206e-3: mutable-basis Hamming packets (≈2^-9.89814; conditional; complex +4.97%) #425 (Zhihao Chen): the common-frame conjugation lemma and scalar interface.
• Conditional κ = 0.001274032589159993: complex kernel with paid residual adapters #458 (chafreaky): the one-helper rule and paid wrappers.
• Conditional kappa = 0.001274548075945587: full-nine-axis kernel normalization and same-owner spectator borrowing #471 (Dugongue): the virtual entrance and complete-invocation normalisation.
• Complex supplier b ≈ 1.327·10⁻³ (+4.7%) on whole-residual hosting: shared-donor kernel and entrance gauges with paid residual wrappers (conditional on two lemmas) #484 (DreamingOfClouds): the gauge construction, Lemma G and its Python check stage.
• formal/lean on main: the Lean toolchain and Mathlib pin.
• [Lean] Verification of selected 1320-port bijection, κ=0.000661885549259598 #487/[Lean] Verification of binary input preparation, κ=0.000661885549259598 #488 (jamesyc): the standalone Lean package layout and axiom reporting.

Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code.

🤖 Generated with Claude Code

[Mister-Meeseeks]

Integrated into published main at 681e8923a0f23a19f93c7105c3a9c96149aa8362, preserving the original commits, notices and contributor credit. Thank you for the contribution.

The general Lemma G proofs build in Lean 4.21.0, with 16 named axiom reports and finite hypothesis checks on the four freshly reconstructed words.

The scoped review and pinned execution receipts record the exact coverage and remaining assumptions. This strengthens specific interfaces and preserves useful research; it does not change the selected κ or establish the complete multiplication theorem. Local checks passed; fresh Linux CI was queued at publication.