Jcost_taylor_quadratic
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 in Recognition Science
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.
scope and limits
- Does not extend the bound beyond |ε| ≤ 1/10.
- Does not compute higher-order terms in the Taylor series.
- Does not integrate the bound over time intervals.
- Does not address multi-dimensional or relativistic extensions.
Lean usage
theorem use_in_bridge (a b : ℝ) (hab : a ≤ b) (ε : ℝ → ℝ) (hε_small : ∀ t ∈ Icc a b, |ε t| ≤ 1/10) (t : ℝ) (ht : t ∈ Icc a b) : |Jcost (1 + ε t) - (ε t)^2 / 2| ≤ (ε t)^2 / 10 := Jcost_taylor_quadratic (ε t) (hε_small t ht)formal statement (Lean)
45theorem Jcost_taylor_quadratic (ε : ℝ) (hε : |ε| ≤ (1 : ℝ) / 10) :
46 |Jcost (1 + ε) - ε ^ 2 / 2| ≤ ε ^ 2 / 10 :=
proof body
Term-mode proof.
47 Jcost_small_strain_bound ε hε
48
49/-- The leading-order coefficient of `Jcost` at the cost minimum is
50 exactly `1/2`. Combined with `Jcost_unit0` (J(1) = 0) and
51 `J'(1) = 0` from `Cost.Convexity`, this is the Taylor expansion
52 `J(1 + ε) = ε²/2 + O(ε³)`. -/