actionJ_to_kinetic_bridge
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.