IndisputableMonolith.Action.QuadraticLimit
The QuadraticLimit module supplies the small-strain quadratic approximation to the J-cost, rebranding the bound |J(1+ε)−ε²/2|≤ε²/10 for |ε|≤1/10 as the foundation for classical mechanics. Researchers deriving Newtonian limits from the Recognition Science J-action cite this when passing from the full variational principle to the standard Lagrangian. The module achieves the result by direct re-expression of the Cost.Jcost_small_strain_bound without new derivations.
claim$|J(1 + ε) - ε²/2| ≤ ε²/10$ whenever $|ε| ≤ 1/10$.
background
This module sits in the Action domain and rebrands the small-strain bound on Jcost to enable the transition from the general J-action to classical mechanics. PathSpace defines admissible paths and the action functional S[γ] = ∫ J(γ(t)) dt. FunctionalConvexity proves convexity of this functional, discharging earlier conditional hypotheses. Cost supplies the base Jcost function together with its Taylor bound near unity.
proof idea
This is a definition module. It rebrands Cost.Jcost_small_strain_bound into Jcost_taylor_quadratic and Jcost_quadratic_leading_coeff, then defines kineticAction and standardLagrangian directly from the quadratic term. No new lemmas or tactics are applied beyond the upstream bound.
why it matters in Recognition Science
The module closes the small-strain limit that feeds NewtonSecondLawDomainCert and Hamiltonian. Those downstream certificates package the equivalence between the J-action Euler-Lagrange equation and Newton's second law, using the quadratic term as the kinetic energy ½ m q̇². It thereby connects the Recognition Science forcing chain (T5 J-uniqueness) to standard mechanics without additional hypotheses.
scope and limits
- Does not prove the Taylor bound from first principles.
- Does not extend the approximation beyond |ε| ≤ 1/10.
- Does not include potential energy or full Lagrangian terms.
- Does not address higher-order corrections or relativistic regimes.