IndisputableMonolith.Action.QuadraticLimit
The QuadraticLimit module supplies the small-strain quadratic approximation to the J-cost function, enabling recovery of the standard kinetic Lagrangian from the Recognition Science action. Physicists deriving Newtonian mechanics from the J-functional would cite this bound. It consists of a direct re-statement of the Cost module's small-strain inequality with no additional argument.
claim$|J(1 + ε) - ε²/2| ≤ ε²/10$ whenever $|ε| ≤ 1/10$.
background
The module resides in the Action domain and imports PathSpace (which defines admissible paths and the integral actionJ γ = ∫ J(γ(t)) dt), FunctionalConvexity (which establishes convexity of the J-action functional), and Cost (source of the base Jcost definition). It rebrands the existing small-strain bound to serve as the quadratic limit bridge. The local setting is the variational principle for the d'Alembert cost J, with the small-strain regime recovering classical mechanics.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the quadratic limit required by Hamiltonian and NewtonSecondLawDomainCert to derive the standard Lagrangian L = ½ m q̇² - V(q) and the associated Euler-Lagrange and Hamilton equations from the J-action. It closes the small-strain step in the chain from J-uniqueness (T5) through the eight-tick octave to classical dynamics, and is imported by EnergyConservationDomainCert.
scope and limits
- Does not prove the bound from first principles.
- Does not extend the approximation beyond |ε| ≤ 1/10.
- Does not address higher-order terms in the Taylor expansion.
- Does not apply outside the admissible-path setting of PathSpace.