quadratic_emergence
plain-language theorem explainer
The J-cost of a small deviation expands as J(1 + ε) = ε²/2 + c ε³ with |c| ≤ 2 whenever |ε| ≤ 1/2. Modelers of emergent Hamiltonians from recognition dynamics cite this to justify the quadratic kinetic term in the small-deviation regime. The proof is a direct one-line application of the core J-cost quadratic lemma.
Claim. For every real number ε satisfying |ε| ≤ 1/2 there exists a real number c such that J(1 + ε) = ε²/2 + c ε³ and |c| ≤ 2.
background
In the Hamiltonian Emergence module the Recognition Operator R̂ acts on states near equilibrium, parameterized by small deviations ε from unity. The J-cost function, calibrated via the Recognition Composition Law and d'Alembert factorization, measures the recognition cost of a state. The module establishes that near x = 1 this cost reduces to a quadratic form that supplies the kinetic energy of the emergent Hamiltonian Ĥ, turning discrete recognition steps into approximate Schrödinger evolution.
proof idea
This is a one-line wrapper that applies the lemma Jcost_one_plus_eps_quadratic from IndisputableMonolith.Cost.JcostCore (and its duplicate in JcostCore). The underlying lemma proceeds by classical case analysis on the bound |ε| ≤ 1/2, verifies positivity of 1 + ε, and performs the algebraic expansion of the J-cost definition to isolate the quadratic and cubic terms with the stated coefficient bound.
why it matters
The declaration supplies the proved scalar foundation for the Hamiltonian emergence claim. It is invoked directly by the downstream theorem per_bond_remainder_bounded to bound the cubic remainder per bond. Within the Recognition Science framework it justifies the quadratic kinetic term in the small-deviation limit of the Recognition Operator, consistent with the J-uniqueness property and the eight-tick octave structure; the operator-level passage to a self-adjoint Hamiltonian via Stone's theorem remains conditional on additional Hilbert-space infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.