inner8
plain-language theorem explainer
Defines the standard Hermitian inner product on 8-tick complex signals: sum of conj(f(k)) g(k) over Fin 8. Anyone proving Parseval for DFT-8, unitary evolution, or the complex-structure certificate cites this. The body is a one-line finite sum; no proof content.
Claim. For signals $f,g:\mathrm{Fin}\,8\to\mathbb{C}$, set $\langle f,g\rangle:=\sum_{k=0}^{7}\overline{f(k)}\,g(k)\in\mathbb{C}$.
background
The module Complex Structure Forcing argues that the 8-tick shift on the ledger cannot be diagonalized over the reals, so complexification is forced. A signal on the cycle is a map Signal8 from Fin 8 to $\mathbb{C}$. The eight-tick period (T7) supplies a cyclic shift $T$ with $T^8=I$ whose eigenvalues are the 8th roots of unity; $\omega^2=i$ has no real square root, so the carrier must be complex.
Once the state space is $\mathbb{C}^8$, the natural sesquilinear form is the standard Hermitian product used in DFT-8 and Plancherel. The module doc states Parseval as $\langle F(f),F(g)\rangle=\langle f,g\rangle$ with exactly this pairing, and ties norm preservation to unitarity of admissible recognition updates. Downstream packages (Born-rule forcing, ledger superposition) re-export the same form as a local abbreviation.
proof idea
Definition only: expand as the finite sum $\sum_{k:\mathrm{Fin},8}\overline{f(k)},g(k)$ via the complex conjugation endomorphism. No tactics or lemmas.
why it matters
This is the inner product that makes DFT-8 unitary and closes the "complex Hilbert space from cost" gap. It appears in the master ComplexStructureCertificate as the form preserved by DFT-8 (dft_unitary), in dft8_preserves_inner / dft8_preserves_norm (Parseval and its norm corollary), and in UnitaryEvolution.preserves_inner as the admissibility condition that forces unitarity together with J-cost non-increase.
Born-rule work uses inner8 f f to recover the sum of squared moduli. The unified forcing bridge from T7 to the canonical carrier also depends on it. Framework landmarks: T7 (eight-tick octave), the forced complex eigenvalues of the shift, and the step from cost axioms to genuine Hilbert-space unitarity. Without a fixed Hermitian product, phase invariance of J and unitary evolution cannot be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.