quadraticEnergy
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove operator-level emergence of a self-adjoint Hamiltonian.
- Does not incorporate the cubic remainder into the energy expression itself.
- Does not address the discrete-to-Schrödinger evolution step.
- Does not depend on specific N beyond the Fin N indexing in the state.
formal statement (Lean)
66def quadraticEnergy (s : SmallDeviationState N) : ℝ :=
proof body
Definition body.
67 Finset.univ.sum fun i => (s.deviations i) ^ 2 / 2
68
69/-- The cubic remainder per bond is bounded. -/