perturbation_cost_small_bound
plain-language theorem explainer
The perturbation cost small bound theorem shows that for real perturbations ε around the ground state with |ε| ≤ 1/10, the J-cost of 1+ε deviates from its quadratic approximation ε²/2 by at most ε²/10. Analysts of zero-defect stability in Recognition Science cite this when bounding the energy cost of small departures from unity. The proof is a direct one-line wrapper invoking the small-strain lemma from the Cost module.
Claim. For every real number $ε$ with $|ε| ≤ 1/10$, $|Jcost(1 + ε) - ε²/2| ≤ ε²/10$.
background
The StillnessGenerative module establishes that x=1 is the unique zero-defect ground state from the Law of Existence (T5) and shows it functions as a generative source rather than passive equilibrium. The J-cost function, imported from the Cost module, quantifies recognition cost with Jcost(1)=0; its small-strain expansion around unity is the quadratic term ε²/2. The module derives all steps from the T0–T8 chain, including the 8-tick cycle (T7) that forces non-uniformity and the finite barrier J(φ)<1 that bounds creation cost.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_small_strain_bound from IndisputableMonolith.Cost (and its JcostCore sibling) directly to the supplied ε and hypothesis hε.
why it matters
This bound quantifies the cost of small perturbations from the ground state, supporting the module's claim that x=1 cannot remain uniform under the 8-tick octave requirement (T7) and the recognition forcing (T4). It fills the finite-barrier step in the derivation chain listed in the module documentation, where adjacent Fibonacci relations populate the phi-ladder. No downstream theorems are recorded yet, but the result underpins later analyses of phi-perturbation boundedness and ladder positivity within the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.