IndisputableMonolith.Action.QuadraticLimit
QuadraticLimit rebrands the small-strain bound on Jcost to establish |J(1+ε) - ε²/2| ≤ ε²/10 for |ε|≤1/10. Researchers deriving classical mechanics from the J-action cite it to justify the kinetic term in the standard Lagrangian. The module consists of direct rebranding plus supporting definitions with no new derivations.
claim$|J(1 + \epsilon) - \epsilon^2/2| \leq \epsilon^2/10$ whenever $|\epsilon| \leq 1/10$.
background
PathSpace defines AdmissiblePath a b as continuous strictly positive paths on [a,b] and actionJ γ as the integral of J over the path. FunctionalConvexity proves convexity of the J-action functional S[γ] = ∫ J(γ(t)) dt to support the variational principle. Cost supplies the base Jcost_small_strain_bound that is rebranded here as the quadratic Taylor expansion near unity.
proof idea
This is a definition module that rebrands Cost.Jcost_small_strain_bound as Jcost_taylor_quadratic and introduces related objects such as kineticAction, standardLagrangian, and newton_second_law. No new proofs are performed; the argument relies entirely on the upstream bound.
why it matters in Recognition Science
This module supplies the small-strain limit required by NewtonSecondLawDomainCert and Hamiltonian to derive Newton's laws and energy conservation from the J-action. It fills the step connecting the Recognition Science J-functional to the classical Lagrangian ½m q̇² - V(q). The downstream modules package the equivalences proved here into domain certificates.
scope and limits
- Does not establish the full variational principle for arbitrary strains.
- Does not derive numerical values of mass or potential.
- Does not address the large-strain regime of the J-action.
- Does not prove convexity properties, which are imported from FunctionalConvexity.