totalJcost_approx_quadratic
plain-language theorem explainer
For small-deviation states the total J-cost differs from the quadratic energy by at most twice the sum of cubed absolute deviations. Researchers deriving emergent Hamiltonians from recognition operators cite this bound to justify the quadratic kinetic term. The proof unfolds the sum definitions, applies the triangle inequality, and invokes the per-bond cubic remainder bound on each term.
Claim. Let $s$ be a small-deviation state with deviations $ε_i$ satisfying $|ε_i|≤1/2$ for each $i=1,…,N$. Then $|∑_i J(1+ε_i) - ∑_i ε_i²/2| ≤ 2 ∑_i |ε_i|³.
background
The HamiltonianEmergence module shows how the Recognition Operator reduces to a quadratic form near equilibrium. A SmallDeviationState consists of bond multipliers 1+ε_i with |ε_i|≤1/2 for all i. totalJcost sums Jcost(1+ε_i) over bonds while quadraticEnergy sums ε_i²/2, matching the leading term of the J-cost expansion J(1+ε)=ε²/2 + O(ε³).
proof idea
Unfold totalJcost and quadraticEnergy. Rewrite the difference of sums as a sum of per-bond differences via sum subtraction. Apply the triangle inequality to bound the sum of absolutes. Invoke per_bond_remainder_bounded on each term to replace the remainder with 2|ε_i|³. Factor the constant 2 out of the sum.
why it matters
This supplies the scalar approximation used by emergence_scalar_proved to establish the HamiltonianIsGenerator. It completes the proved scalar foundation of the emergence hypothesis in the Recognition Science framework, where the J-cost quadratic form becomes the kinetic energy of the emergent Hamiltonian. The bound supports the small-deviation regime in which recognition dynamics approximate discrete Schrödinger evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.