inner8_self_eq
plain-language theorem explainer
The self-inner product of an 8-mode complex signal equals the sum of squared component norms, cast into ℂ. Anyone deriving the Born sector measure or applying Parseval on DFT-8 cites this identity. The proof unfolds the inner-product definition and reduces each summand via the conjugate-times-self formula for complex norm squared.
Claim. For every 8-mode signal $f:\mathrm{Fin}\,8\to\mathbb{C}$, the standard inner product satisfies $\langle f,f\rangle=\sum_{k=0}^{7}|f(k)|^2$ as an equality in $\mathbb{C}$ (right-hand side via the real-to-complex embedding of squared modulus).
background
The module forces the Born rule as the unique probability measure on 8-mode sectors that is normalised, phase-invariant, additive on disjoint mode sets, and consistent with the two-branch $\exp(-C)$ calibration. Signals live on the eight-tick octave (T7): an 8-mode signal is a map $\mathrm{Fin},8\to\mathbb{C}$.
The standard inner product is $\langle f,g\rangle=\sum_k \overline{f(k)},g(k)$. Squared modulus is the real number $|z|^2$, and the sibling lemma records $\overline{z},z=\uparrow|z|^2$. Sector measure is built from these squared norms; relating $\langle\psi,\psi\rangle$ to their sum is the bridge to Parseval and total-mass identities used later in the file.
proof idea
Unfold the inner product by simp, so both sides are finite sums over $\mathrm{Fin},8$. Congruence of the sum plus pointwise extensionality reduce the claim to one complex identity per mode: $\overline{f(k)},f(k)=\uparrow|f(k)|^2$. That is exactly the sibling lemma equating star-times-self to the real-to-complex cast of squared modulus (the symmetric form of the standard complex-norm identity).
why it matters
This private lemma is the algebraic hinge for the Parseval corollary that total sector measure is DFT-8 invariant: the total measure of a signal equals that of its DFT image. That identity sits inside the Born-rule forcing chain, which closes the Born-rule gap by proving $\mu(S)=\sum_{k\in S}|\psi_k|^2$ is the unique measure meeting the four axioms.
Framework landmarks: T7 (eight-tick octave) supplies the $\mathrm{Fin},8$ mode space; the construction depends on complex-structure forcing (inner product, DFT-8, Parseval) and the two-outcome Born calibration. Without equating $\langle f,f\rangle$ to the sum of squared norms, the sector total cannot be rewritten through the DFT-preserved inner product.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.