Jcost_taylor_quadratic
plain-language theorem explainer
The quadratic Taylor expansion of the J-cost functional near unity asserts that |J(1 + ε) - ε²/2| ≤ ε²/10 for |ε| ≤ 1/10, where J(x) = (x + x^{-1})/2 - 1. Researchers deriving Newtonian mechanics from the Recognition Science cost functional cite this bound to justify the small-strain approximation. The proof is a direct one-line application of the pre-existing small-strain bound lemma in the Cost module.
Claim. $|J(1 + ε) - ε²/2| ≤ ε²/10$ whenever $|ε| ≤ 1/10$, where $J(x) := (x + x^{-1})/2 - 1$.
background
In the Recognition Science framework the cost functional is J(x) = (x + x^{-1})/2 - 1 for x > 0. This satisfies J(1) = 0 with a minimum at x = 1 and vanishing first derivative. The module Action.QuadraticLimit examines the small-strain regime γ = 1 + ε with |ε| ≪ 1, where J reduces to its quadratic Taylor expansion ½ε² plus higher-order remainders. The upstream lemma Jcost_small_strain_bound from IndisputableMonolith.Cost supplies the explicit error control |J(1 + ε) - ε²/2| ≤ ε²/10 for |ε| ≤ 1/10. Module documentation states that this limit converts the J-action into the standard Lagrangian action whose Euler–Lagrange equation recovers Newton’s second law.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_small_strain_bound ε hε from the Cost module.
why it matters
This supplies the pointwise quadratic bound used by actionJ_to_kinetic_bridge to show that the J-action S[1 + ε] differs from the kinetic action (1/2)∫ε² dt by at most (1/10) of the kinetic term. It also appears in newtonSecondLawCert as the quadratic_taylor_bound witness. The declaration fills the quadratic-limit step in the derivation of Newton’s second law from the J-cost functional, as outlined in papers/RS_Least_Action.tex Section “Newton’s Second Law as a Corollary”. It relies on the Recognition Composition Law but does not invoke the full forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.