actionJ_to_kinetic_bridge
The bridge theorem shows that when strain satisfies |ε(t)| ≤ 1/10 on [a,b], the J-cost J(1+ε(t)) stays within relative error 1/10 of the quadratic term ε(t)²/2. Researchers deriving classical mechanics from the Recognition Science cost functional cite this to equate the J-action with the standard kinetic action. The proof is a one-line wrapper that specializes the pointwise Taylor bound at each t.
claimLet $a ≤ b$ and let ε be continuous on $[a,b]$ with $|ε(t)| ≤ 1/10$ for all $t ∈ [a,b]$. Then for all $t ∈ [a,b]$, $|J(1+ε(t)) - ε(t)^2/2| ≤ ε(t)^2/10$, where $J(γ) = ½(γ + γ^{-1}) - 1$.
background
The Quadratic Limit module shows how the Recognition Science cost functional reduces to Newtonian mechanics for small strains γ = 1 + ε. The cost is defined by J(γ) = ½(γ + γ^{-1}) - 1, which vanishes at γ = 1 and has leading quadratic term ½ε². This theorem supplies the pointwise error control |J(1+ε) - ε²/2| ≤ ε²/10 whenever |ε| ≤ 1/10. It reuses the small-strain bound already proved in the Cost module and is the local ingredient needed to pass from the integrated J-action to the kinetic action ½∫ε² dt.
proof idea
The proof is a one-line wrapper. It introduces t in the interval and applies the upstream theorem Jcost_taylor_quadratic directly to the scalar value ε(t), using the pointwise hypothesis |ε(t)| ≤ 1/10.
why it matters in Recognition Science
This declaration supplies the exact error control that identifies the J-action with the standard kinetic action in the small-strain regime, thereby allowing Newton's second law to appear as the Euler-Lagrange equation of the quadratic Lagrangian. It fills the step described in the module's paper companion RS_Least_Action.tex, Section Newton's Second Law as a Corollary. The result sits between the J-uniqueness property (T5) and the emergence of classical mechanics, with the same framework later fixing D = 3 and the eight-tick octave.
scope and limits
- Does not hold when |ε| > 1/10 at any point.
- Does not integrate the pointwise bound to control the full action difference.
- Does not derive the Euler-Lagrange equation or equations of motion.
- Does not include a potential term or full Lagrangian.
formal statement (Lean)
124theorem actionJ_to_kinetic_bridge (a b : ℝ) (hab : a ≤ b)
125 (ε : ℝ → ℝ) (hε_cont : ContinuousOn ε (Icc a b))
126 (hε_small : ∀ t ∈ Icc a b, |ε t| ≤ (1 : ℝ) / 10) :
127 ∀ t ∈ Icc a b, |Jcost (1 + ε t) - (ε t) ^ 2 / 2| ≤ (ε t) ^ 2 / 10 := by
proof body
Term-mode proof.
128 intro t ht
129 exact Jcost_taylor_quadratic (ε t) (hε_small t ht)
130
131/-! ## Status report -/
132