inner8
plain-language theorem explainer
Canonical Hermitian inner product on eight-tick complex signals: ⟨f,g⟩ = Σ_k conj(f(k)) g(k). Re-exported here so OperatorCore proofs can cite the same pairing used in complex-structure forcing and ledger superposition. Pure abbreviation of the Foundation definition; no extra proof content.
Claim. For eight-component complex signals $f,g:\mathrm{Fin}\,8\to\mathbb{C}$, define the standard Hermitian pairing $\langle f,g\rangle=\sum_{k=0}^{7}\overline{f(k)}\,g(k)\in\mathbb{C}$.
background
Signal8 is the space of maps Fin 8 → ℂ: complex amplitudes on the eight-tick octave forced by T7 (period 2³). The module OperatorCore.ComplexStructureForcing re-exports the Foundation complex-structure toolkit so unitary and Born-rule arguments share one carrier.
The upstream definition states: "The standard inner product on Signal8: ⟨f,g⟩ = Σ conj(f(k)) · g(k)." Conjugation is the starRingEnd involution on ℂ. The same alias appears in Gravity.LedgerSuperposition as the "canonical Hermitian inner product on Signal8," so ledger and foundation layers agree on norms and orthogonality.
This pairing is the Hilbert structure against which DFT-8 unitarity, phase invariance of J-cost, and Born-rule normalisation are stated.
proof idea
One-line abbreviation: inner8 is definitionally equal to Foundation.ComplexStructureForcing.inner8. No tactics, no lemmas. Unfolding yields the finite sum Σ_k star(f k) * g k over Fin 8.
why it matters
Every unitary and probability claim on the eight-tick carrier needs this pairing. Downstream, dft8_preserves_inner is Parseval for DFT-8 (⟨F(f),F(g)⟩=⟨f,g⟩), and dft8_preserves_norm is the norm corollary. inner8_conj_symm records conjugate symmetry; inner8_self_eq in BornRuleForcing rewrites ⟨f,f⟩ as Σ |f(k)|² for sector measures.
The master certificate ComplexStructureCertificate lists dft_unitary : ∀ f g, inner8 (dft8 f) (dft8 g) = inner8 f g as a field, tying the product into the T5–T8 chain: J-uniqueness, φ, eight-tick period, and forced complex structure. UnitaryEvolution and the T7-to-canonical-carrier bridge also depend on it. Without a shared inner product, unitarity of the shift/DFT and Born normalisation would not type-check across modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.