geodesic_minimizes_unconditional
A path minimizing the J-action along every convex interpolation segment to a competitor is a global minimizer among all admissible paths sharing endpoints. Recognition Science derivations cite it to obtain the unconditional principle of least action once convexity of the action functional is in hand. The tactic proof specializes the segment hypothesis at s=1 and uses the interpolation definition to identify the endpoint case with the competitor path.
claimLet $a,b$ be reals with $a≤b$ and let $γ_{geo},γ_{other}$ be admissible paths on $[a,b]$ that agree at the endpoints. If $S[γ_{geo}]≤S[(1-s)γ_{geo}+sγ_{other}]$ holds for every $s∈[0,1]$, where $S$ denotes the J-action integral, then $S[γ_{geo}]≤S[γ_{other}]$.
background
AdmissiblePath is a continuous strictly positive function on the closed interval. The J-action is the integral of Jcost along the path, the central functional whose critical points are geodesics for the Hessian metric derived from J. fixedEndpoints asserts agreement at the interval endpoints. interp constructs the pointwise convex combination, which stays admissible for $s∈[0,1]$ by the upstream lemma interp_apply. actionJ_convex_on_interp supplies the integrated convexity inequality $S[(1-s)γ_1+sγ_2]≤(1-s)S[γ_1]+sS[γ_2]$, obtained by integrating the pointwise convexity of Jcost that follows from the d'Alembert functional equation.
proof idea
Specialize the universal hypothesis at s=1 using the fact that 1 lies in the unit interval. Apply interp_apply to equate the interpolated path at s=1 with the competitor path pointwise, then rewrite the action integral to obtain equality of the two actions. The desired inequality follows immediately by transitivity.
why it matters in Recognition Science
The result supplies the unconditional principle of least action in the Recognition framework, feeding directly into functionalConvexity_status and geodesic_minimizes_via_convexity. It discharges the interpolation-minimality witness previously required by the legacy convex_implies_geodesic_minimizes, leaving only the existence of a critical point as an open hypothesis. The argument rests on convexity of Jcost, itself a theorem of d'Alembert uniqueness, and closes the variational step after J-uniqueness in the T0-T8 chain.
scope and limits
- Does not prove existence of any critical point or geodesic.
- Does not establish uniqueness of the minimizer.
- Does not apply outside the class of admissible paths.
- Does not treat time-dependent costs or higher-dimensional domains.
formal statement (Lean)
188theorem geodesic_minimizes_unconditional (_hab : a ≤ b)
189 (γ_geo γ_other : AdmissiblePath a b)
190 (_h_endpoints : fixedEndpoints γ_geo γ_other)
191 (h_critical_along_segment :
192 ∀ (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1),
193 actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s hs)) :
194 actionJ γ_geo ≤ actionJ γ_other := by
proof body
Tactic-mode proof.
195 -- Specialize the segment-minimality at s = 1.
196 have hs1 : (1 : ℝ) ∈ Icc (0:ℝ) 1 := ⟨by norm_num, le_refl 1⟩
197 have h_at_one : actionJ γ_geo ≤ actionJ (interp γ_geo γ_other 1 hs1) :=
198 h_critical_along_segment 1 hs1
199 -- The interpolation at s = 1 is γ_other (pointwise equal).
200 have h_interp_one_eq :
201 actionJ (interp γ_geo γ_other 1 hs1) = actionJ γ_other := by
202 unfold actionJ
203 apply intervalIntegral.integral_congr
204 intro t _
205 have h_eq : (interp γ_geo γ_other 1 hs1).toFun t = γ_other.toFun t := by
206 simp [interp_apply]
207 exact congrArg Jcost h_eq
208 rw [← h_interp_one_eq]
209 exact h_at_one
210
211/-- **Even stronger headline.** If `γ_geo` is a critical point of the
212 action functional in the convexity-witness sense (action does not
213 *decrease* under any infinitesimal interpolation perturbation toward
214 a competitor), then by convexity it is a global minimum.
215
216 Specifically: if for every `γ_other` and every `s ∈ [0,1]`,
217 `actionJ γ_geo ≤ actionJ (interp γ_geo γ_other s)`, then
218 `actionJ γ_geo ≤ actionJ γ_other`.
219
220 The convexity inequality already proved (`actionJ_convex_on_interp`)
221 says `actionJ (interp γ_geo γ_other s) ≤ (1-s) actionJ γ_geo + s actionJ γ_other`.
222 Combining: `actionJ γ_geo ≤ (1-s) actionJ γ_geo + s actionJ γ_other`
223 for all `s ∈ [0,1]`. Taking `s = 1` gives the result.
224
225 The point is: the "interpolation-minimality" hypothesis used by the
226 legacy `convex_implies_geodesic_minimizes` is **automatically
227 satisfied** by any candidate critical point, given convexity. -/