ledgerSuperpositionTheorem
plain-language theorem explainer
Canonical packed witness that the one-tick recognition update is ℂ-linear on pairs and finite sums, and preserves the eight-component Hermitian inner product and its norm. Cited by anyone invoking T1 (Ledger Superposition) of Gravity from Recognition IV. Construction is a pure structure assembly of four already-proved lemmas; no new argument.
Claim. There is a complete witness that the cyclic recognition update $R$ on eight-component complex ledger signals satisfies: (i) $R(a\psi+b\phi)=a R\psi+b R\phi$ for all amplitudes $a,b\in\mathbb{C}$; (ii) $R$ commutes with finite linear combinations $\sum_{\alpha} c_\alpha |L_\alpha\rangle$; (iii) $R$ preserves the canonical Hermitian inner product $\langle Rf, Rg\rangle=\langle f,g\rangle$; (iv) consequently $R$ preserves the induced norm squared.
background
This module anchors two load-bearing results from Gravity from Recognition IV: The Quantum Channel. T1 (Ledger Superposition) asserts that the recognition state space is a complex Hilbert carrier on which the one-tick update is ℂ-linear and inner-product preserving, so coherent superpositions of definite ledger configurations are physical and evolve unitarily under recognition.
The carrier is the eight-component complex signal space (the eight-tick octave forced at T7). The update is the cyclic shift of those eight slots. The inner product is the canonical Hermitian form on that space, forced alongside the complex structure. Pair linearity is the Schrödinger-derivation linearity lemma repackaged in ledger language; finite-sum linearity is the explicit superposition principle $R\sum c_\alpha|L_\alpha\rangle=\sum c_\alpha R|L_\alpha\rangle$.
The master structure packages four fields: pair linearity, finite-sum linearity, inner-product preservation, and norm preservation (the last a corollary of the third).
proof idea
Pure structure inhabitant: each field is assigned an already-proved theorem. Pair linearity is the direct wrapper of the Schrödinger-derivation linearity result. Finite-sum linearity is the Finset induction theorem that extends pair linearity to arbitrary finite combinations. Inner-product preservation unfolds the eight-slot sum and uses that cyclic shift merely permutes summands. Norm preservation is the diagonal case of inner-product preservation. No new tactics or algebra appear at this site.
why it matters
This is the canonical T1 master witness: "ledger superpositions are physical and are preserved by recognition evolution." Downstream, the inhabitedness theorem cites it to obtain Nonempty of the master structure, closing the existence claim for the paper's Theorem 1.
In the forcing chain it sits on the eight-tick octave (T7) and the complex-structure/inner-product package from Foundation. It supplies the Hilbert-space backbone needed before T2 (cost-gradient functoriality under superposition) can extend classical density-to-gravity maps by free linear extension. No new RS axioms: all content is reused from Schrödinger derivation, the recognition operator, and complex-structure forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.