quadraticEnergy
plain-language theorem explainer
quadraticEnergy defines the leading quadratic term in the energy of a small-deviation state as half the sum of squared deviations. Researchers deriving the emergent Hamiltonian from the Recognition Operator cite it when approximating total J-cost near equilibrium. The definition is a direct one-line sum that implements the scalar expansion J(1 + ε) ≈ ε²/2.
Claim. For a small-deviation state $s$ with deviations $ε_i$ ($i=1$ to $N$), the quadratic energy is $E(s) = (1/2) ∑_i ε_i²$.
background
The module shows that the Recognition Operator reduces to a quadratic energy form for states near equilibrium. SmallDeviationState encodes these configurations: a vector of deviations ε_i in Fin N with |ε_i| ≤ 1/2, so that bond multipliers equal 1 + ε_i. The J-cost expansion J(1 + ε) = ε²/2 + O(ε³) supplies the local setting, with this definition extracting the quadratic piece as the sum of (ε_i)²/2.
proof idea
One-line definition that sums (s.deviations i)² / 2 over Finset.univ.
why it matters
This supplies the scalar foundation for Hamiltonian emergence. It is invoked by totalJcost_approx_quadratic, which bounds |totalJcost s - quadraticEnergy s| by a cubic remainder, and by the hypothesis H_HamiltonianIsGenerator that the Recognition Operator generates a self-adjoint Hamiltonian in the small-deviation limit. The module states that the scalar expansion is proved while the operator-level claim requires discrete Stone theorem infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.