inner8
plain-language theorem explainer
Local alias for the canonical Hermitian product on eight-tick signals: ⟨f,g⟩ = Σ_k conj(f(k)) g(k) over Fin 8. Gravity and foundation modules cite it when stating that recognition updates preserve norms and superpositions. The body is a one-line re-export of the ComplexStructureForcing definition.
Claim. For eight-component complex signals $f,g:\{0,\ldots,7\}\to\mathbb{C}$, write $\langle f,g\rangle:=\sum_{k=0}^{7}\overline{f(k)}\,g(k)\in\mathbb{C}$. This is the standard Hermitian inner product on the eight-tick analytic carrier.
background
Gravity IV formalizes ledger superposition: the recognition state space is an eight-tick complex carrier, and the one-tick update must act as a unitary linear map so coherent superpositions remain physical. The carrier is Signal8, identified with maps Fin 8 → ℂ from ComplexStructureForcing (the discrete 8-tick octave forced by T7).
The canonical product on that space is the standard $\ell^2$ Hermitian form $\langle f,g\rangle=\sum_k \overline{f(k)} g(k)$. Upstream, ComplexStructureForcing defines it exactly that way and proves conjugate symmetry, DFT-8 unitarity (Parseval), and the master complex-structure certificate. SchrödingerDerivation supplies $\mathbb{C}$-linearity of the cyclic shift on the same carrier.
This module only re-exports that product under a local name so T1 (linearity and inner-product preservation of the recognition update) can be stated without long qualified paths.
proof idea
Definitional abbreviation: the body is a single application of Foundation.ComplexStructureForcing.inner8. No tactics, no new proof obligations. All algebraic properties (conjugate symmetry, positivity of the diagonal, DFT preservation) are inherited from the upstream definition and its lemmas.
why it matters
T1 of Gravity from Recognition IV needs a named Hilbert product on Signal8 so that preservation of coherent superpositions is a concrete statement: the recognition update is $\mathbb{C}$-linear and inner-product preserving. Downstream, ComplexStructureForcing uses the same product for DFT-8 unitarity, norm preservation, conjugate symmetry, UnitaryEvolution, and the ComplexStructureCertificate (cost + 8-tick forcing of complex structure, tying T5–T8 to the Hilbert carrier). BornRuleForcing reduces the diagonal $\langle f,f\rangle$ to a sum of norm-squares for sector measures.
In-module siblings (recognition_update_inner_preserved, ledger_superposition_preserved, the LedgerSuperpositionTheorem bundle) cite this alias as the product that the cyclic shift must preserve. Without it, the quantum-channel reading of the ledger update has no fixed inner-product language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.