per_bond_remainder_bounded
plain-language theorem explainer
The theorem bounds the cubic remainder term in the J-cost expansion for a single bond deviation ε satisfying |ε| ≤ 1/2. Researchers deriving emergent Hamiltonians from recognition dynamics cite it to control the error when replacing the full J-cost by its quadratic kinetic approximation. The proof extracts the cubic coefficient from the quadratic_emergence lemma, rewrites the difference via ring, and applies absolute-value bounds with nlinarith to reach the stated 2|ε|³ estimate.
Claim. For any real ε with |ε| ≤ 1/2, |Jcost(1 + ε) − ε²/2| ≤ 2|ε|³.
background
The HamiltonianEmergence module shows that the Recognition Operator reduces to a quadratic energy form near equilibrium. For states parameterized by small deviations ε, the J-cost satisfies J(1 + ε) = ε²/2 + O(ε³); this quadratic piece is identified with the kinetic term of the emergent Hamiltonian, while the cubic remainder controls the approximation error in the discrete Schrödinger evolution ψ(t + Δt) ≈ (1 − iĤΔt)ψ(t). The module supplies SmallDeviationState, quadraticEnergy, and the embedding into Hilbert space as the concrete types needed for this reduction.
proof idea
Obtain the cubic coefficient c together with the equality Jcost(1 + ε) = ε²/2 + c ε³ and the bound |c| ≤ 2 from quadratic_emergence. Rewrite the target difference as c ε³ by ring, apply abs_mul, then bound |c| |ε|³ ≤ 2 |ε|³ by nlinarith using the known bound on |c| and non-negativity of |ε|³. Finish by rewriting |ε³| as |ε|³ via abs_pow.
why it matters
This per-bond bound supplies the scalar error control required by totalJcost_approx_quadratic, which lifts the estimate to the summed J-cost over an entire SmallDeviationState and thereby justifies replacing totalJcost by quadraticEnergy up to a cubic remainder. It directly supports the module’s claim that the scalar expansion J(1 + ε) = ε²/2 + O(ε³) is proved and forms the foundation for the operator-level emergence hypothesis H_HamiltonianIsGenerator. In the larger framework it anchors the small-deviation regime that converts the eight-tick recognition dynamics into quadratic energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.