embed_norm_sq
plain-language theorem explainer
The squared norm of the complex embedding of a small-deviation state equals the sum of its squared real deviations. Researchers deriving the emergent Hamiltonian from the recognition operator cite this identity to equate the Hilbert-space norm with the quadratic J-cost term. The proof is a direct term-mode application of sum congruence followed by simplification of the embedding cast and norm squared.
Claim. For a small-deviation state $s$ on $N$ bonds, let $embed(s)$ be the vector in $DeviationHilbert N$ obtained by casting each real deviation to $ℂ$. Then $∑_{i} |embed(s)_i|^2 = ∑_{i} (deviations(s)_i)^2$.
background
The HamiltonianEmergence module shows that the Recognition Operator reduces to quadratic form near equilibrium. A SmallDeviationState is a structure holding real deviations $ε_i$ with $|ε_i| ≤ 1/2$, so that bond multipliers are $1 + ε_i$. The embed function maps these deviations to a vector in the complex space $DeviationHilbert N$ by direct cast to $ℂ$ (see the sibling definition at line 106). This identity therefore equates the squared Euclidean norm of the embedded vector with the sum of squared deviations. Upstream, the $H$ reparametrization from CostAlgebra gives $H(x) = J(x) + 1 = (x + x^{-1})/2$, which yields the expansion $J(1 + ε) = ε^2/2 + O(ε^3)$ that makes the quadratic term the emergent kinetic energy.
proof idea
The proof applies Finset.sum_congr with reflexivity to reduce the global equality to a pointwise claim for each index $i$. It then invokes simp on the embed definition and Complex.normSq_ofReal, after which ring closes the resulting algebraic identity between the squared real number and its complex norm squared.
why it matters
This supplies the norm identity required to identify the quadratic J-cost with the energy expectation value in the emergent Hilbert space. It directly supports the module's construction of DiscreteEvolution and the conditional hypothesis that recognition dynamics generate a self-adjoint Hamiltonian. In the Recognition Science framework it realizes the small-deviation limit in which the eight-tick octave approximates Schrödinger evolution, with the quadratic term supplying the energy scale. No downstream uses are recorded, leaving the full operator-level emergence open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.