kineticAction
plain-language theorem explainer
kineticAction defines the standard kinetic action as the integral of half the square of the strain function ε over the interval from a to b. Researchers deriving classical mechanics from the Recognition Science J-cost functional cite this as the explicit form of the quadratic limit. The definition consists of a direct integral expression without additional lemmas or reductions.
Claim. The kinetic action is defined by $T[ε] := (1/2) ∫_a^b ε(t)^2 dt$ for a real-valued strain field ε on the interval [a,b], obtained as the leading quadratic term in the Taylor expansion of the J-cost when the local scale factor satisfies γ(t) = 1 + ε(t).
background
In the Recognition Science framework the J-cost is given by J(γ) = (1/2)(γ + γ^{-1}) - 1. The module Action.QuadraticLimit examines the small-strain regime where the scale factor takes the form γ = 1 + ε with |ε| ≪ 1. Under this substitution the J-cost reduces to its quadratic Taylor term (1/2)ε², which is integrated to form the action. The upstream result from Cosmology.InflatonPotentialFromJCost supplies V(φ_inf) := J(1 + φ_inf), confirming that the same functional appears as the inflaton potential on the recognition manifold.
proof idea
The definition is a direct one-line integral expression that substitutes the quadratic approximation (1/2)ε² into the action integral. No lemmas are applied beyond the standard Lebesgue integral on the real line.
why it matters
This definition supplies the explicit kinetic term that enters the bridge theorem quadraticLimit_status, which asserts that the full J-action differs from the kinetic action by at most one-tenth of the kinetic action itself when |ε| ≤ 1/10. It realizes the paper proposition that Newton's second law follows as a corollary of the J-action principle in the small-strain limit. The construction sits inside the forcing chain after T5 (J-uniqueness) and provides the concrete link from the Recognition Composition Law to classical mechanics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.