perturbation_cost_quadratic
plain-language theorem explainer
The theorem supplies a cubic-error expansion for the J-cost of a small deviation from the ground state. Researchers tracing the T7 eight-tick instability would cite it to bound the energy cost of the first non-uniform ledger entry. The proof is a one-line wrapper that invokes the quadratic lemma already proved in the Cost module.
Claim. For any real number $ε$ with $|ε| ≤ 1/2$, there exists a real number $c$ such that $Jcost(1 + ε) = ε²/2 + c ε³$ and $|c| ≤ 2$.
background
The module proves that the uniform ground state x=1 is unstable under the 8-tick cycle and therefore generates non-trivial structure. Jcost is the cost function satisfying the Recognition Composition Law, with Jcost(x) = J(x) where J(x) = (x + x⁻¹)/2 − 1. The upstream lemma Jcost_one_plus_eps_quadratic from the Cost module already establishes the explicit quadratic leading term together with a uniform cubic remainder bound.
proof idea
One-line wrapper that applies Jcost_one_plus_eps_quadratic ε hε from the Cost module.
why it matters
The bound quantifies the finite creation cost of the first departure from x=1, closing the argument that the ground state is generative rather than passive. It directly supports the T7 eight-tick requirement and the finite barrier J(φ) < 1 stated in the module derivation chain. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.