recognition_update_norm_preserved
plain-language theorem explainer
The one-tick recognition update (cyclic shift on the eight-tick complex signal) preserves the squared Hermitian norm of every ledger state. Anyone citing T1 (ledger superposition) needs this as the norm half of unitarity of the update. The proof is a one-line specialization of inner-product preservation to equal arguments.
Claim. For every eight-tick complex signal $f : \mathrm{Fin}\,8 \to \mathbb{C}$, if $U$ denotes the one-tick cyclic shift, then $\langle Uf, Uf\rangle = \langle f, f\rangle$, where $\langle\cdot,\cdot\rangle$ is the standard Hermitian sum $\sum_{k} \overline{f(k)}\,g(k)$.
background
This module anchors Theorem 1 of Gravity from Recognition IV: The Quantum Channel: the recognition state space is a complex Hilbert carrier, and the one-tick update is $\mathbb{C}$-linear and inner-product preserving, so coherent superpositions of definite ledger configurations are physical and evolve unitarily under recognition.
The carrier Signal8 is the eight-tick analytic signal $\mathrm{Fin},8 \to \mathbb{C}$, forced by the eight-tick octave (T7) and $D=3$ (T8) in the unified forcing chain. The canonical Hermitian product is $\langle f,g\rangle = \sum_{k:\mathrm{Fin},8} \overline{f(k)},g(k)$. The recognition update is the cyclic shift on that eight-slot register.
Norm preservation is listed as T1.iii: the squared-norm corollary of full inner-product preservation (T1.ii). No new RS axioms are introduced; the argument reuses the foundation complex-structure and recognition-operator layers.
proof idea
One-line term proof: instantiate the sibling lemma that the cyclic shift preserves the full sesquilinear form, at the diagonal pair $(f,f)$. That immediately yields $\langle Uf,Uf\rangle=\langle f,f\rangle$. No separate algebraic expansion of the sum is required here.
why it matters
Fills the norm_preserved field of the canonical LedgerSuperpositionTheorem witness, which packages T1 as a complete record: $\mathbb{C}$-linearity, finite-sum linearity, inner-product preservation, and norm preservation. Downstream, that witness is the formal content of "ledger superpositions are physical and are preserved by recognition evolution."
In the paper chain this is T1.iii, the unitarity-on-norms half of the claim that recognition evolution is a $\mathbb{C}$-linear isometry of the eight-tick Hilbert carrier. It sits on the eight-tick octave forced at T7 and the $D=3$ period identity at T8; without norm preservation the superposition story would only give linearity, not conservation of the ledger amplitude budget under a tick.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.