ledger_superposition_preserved
plain-language theorem explainer
The one-tick recognition update on eight-tick ledger signals is ℂ-linear: it sends a linear combination of two configurations to the same combination of their images. Gravity-from-recognition authors cite this as T1.i, the binary form of ledger superposition. The proof is a one-line re-export of the foundation linearity lemma for the discrete Schrödinger step.
Claim. For eight-tick signals $\psi,\varphi:\mathrm{Fin}\,8\to\mathbb{C}$ and amplitudes $a,b\in\mathbb{C}$, the one-tick recognition update $R$ satisfies $R(a\psi+b\varphi)=a\,R(\psi)+b\,R(\varphi)$.
background
The module Gravity IV anchors Theorem 1 (Ledger Superposition) of Gravity from Recognition IV: The Quantum Channel. The carrier is Signal8, the eight-tick analytic signal type $\mathrm{Fin},8\to\mathbb{C}$, identified with the forced complex structure from ComplexStructureForcing. The one-tick recognition update is the cyclic shift on that register; the module treats it as the discrete Schrödinger step of the recognition operator.
Upstream, SchrodingerDerivation already proves that this cyclic shift is ℂ-linear on general states: "the one-tick recognition evolution is ℂ-linear, so the discrete Schrödinger equation extends from eigenmodes to arbitrary linear combinations." That lemma is the sole mathematical content here; the present declaration only renames it into the ledger-superposition vocabulary of T1.
No new RS axioms enter. The surrounding T1 package also records inner-product and norm preservation of the same update, so that coherent superpositions of definite ledger configurations remain physical states under one tick.
proof idea
One-line term proof: apply schrodinger_linear from Foundation.SchrodingerDerivation to the same four arguments. That upstream lemma expands by rewriting with additivity and scalar-homogeneity of the cyclic shift (cyclic_shift_add and cyclic_shift_smul twice). No local calculation is added.
why it matters
This is clause T1.i of Ledger Superposition: binary ℂ-linearity of the recognition update on ledger configurations. It is wired directly into the structure inhabitant ledgerSuperpositionTheorem as the linearity field, alongside the finite-sum form, inner-product preservation, and norm preservation.
In the paper narrative, T1 asserts that Signal8 is a complex Hilbert carrier and that coherent superpositions of definite ledger states are physical and preserved by the update. Linearity is the first half of that claim; without it the free linear extension used in T2 (cost-gradient functoriality under superposition) would not be available. The eight-tick register itself is the T7 octave forced earlier in the chain; the complex structure is forced rather than postulated.
The result is unconditional and proved. It does not by itself address gravitational readout; that is T2's MODEL-tagged interpretation of unique linear extension of classical density-to-gravity maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.