inner8_conj_symm
plain-language theorem explainer
Conjugate-symmetry of the standard Hermitian product on 8-tick complex signals: conjugating ⟨f,g⟩ recovers ⟨g,f⟩. Cited when building the DFT-8 Hilbert structure, Parseval, or any unitarity argument on the octave cycle. Proof is a short unfold-and-ring calculation: conjugation passes through the finite sum and product, then star-involution cancels pointwise.
Claim. Let $f,g:\{0,\ldots,7\}\to\mathbb{C}$. With the standard inner product $\langle f,g\rangle=\sum_{k=0}^{7}\overline{f(k)}\,g(k)$, one has $\overline{\langle f,g\rangle}=\langle g,f\rangle$.
background
This module forces complex structure from the eight-tick ledger cycle (T7): the cyclic shift $T$ on 8-tick states satisfies $T^8=I$, its spectrum is the 8th roots of unity, and $\omega^2=i$ has no real representative, so diagonalization over $\mathbb{R}$ is impossible. The DFT-8 is the canonical unitary diagonalization; Parseval and phase-invariant $J$-cost then require a genuine Hermitian product on complex signals.
A signal on the octave is Signal8, i.e. a map $\mathrm{Fin},8\to\mathbb{C}$. The standard product is defined by $\langle f,g\rangle=\sum_k \overline{f(k)},g(k)$ (conjugation via the star endomorphism of $\mathbb{C}$). Conjugate-symmetry is the first algebraic axiom needed before norm, Cauchy–Schwarz, or unitarity of the recognition update can be stated.
proof idea
Unfold the sum definition of the inner product. Push the complex conjugation map through the finite sum and through multiplication (map_sum, map_mul). After a congruence and pointwise extension over $k:\mathrm{Fin},8$, the star-involution identity $\overline{\overline{z}}=z$ together with commutativity of multiplication in $\mathbb{C}$ rewrites each summand $\overline{\overline{f(k)},g(k)}$ as $\overline{g(k)},f(k)$, which is exactly the summand of $\langle g,f\rangle$. Finish by ring.
why it matters
Hermitian conjugate-symmetry is a prerequisite for the complex Hilbert-space structure the module is closing: without it there is no norm from an inner product, no Parseval identity for DFT-8, and no route from cost axioms to unitarity of the recognition operator $\hat R$ (admissibility-preserving iff norm-preserving iff unitary). The module doc ties this chain to T5 (cost uniqueness), T7 (eight-tick octave), and T8 ($D=3$), and lists the registry gap "Complex Hilbert space from cost".
No downstream dependents are recorded yet for this lemma; it sits as local infrastructure beside the DFT-8 definition and the eigenvalue facts ($\omega^2=i$, no real root of $x^2+1$). Anyone proving sesquilinearity, positive-definiteness, or DFT unitarity on Signal8 will need it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.