Action Path Space Interp Fixed Endpoints

Blending paths without moving the ends

In the calculus of variations, a common move is to take two candidate curves between the same two points and form a weighted average of them. The declaration interp_fixedEndpoints in the Recognition Science library proves that this move is safe inside its own setting: if two admissible paths agree at both ends of an interval, then every convex combination of them, with weight s between 0 and 1, also agrees at both ends. The proof is a direct calculation from the definition of the interpolation and the shared boundary conditions.

The setting matters. An admissible path here is a continuous, strictly positive function on a closed interval. The framework's action functional, written S[γ] = ∫ J(γ(t)) dt, uses the cost function J(x) = (x + 1/x)/2 - 1, and the paths it cares about are the ones that minimize this action. The interpolation result is the technical hinge that lets a convexity argument run: because the blend of two admissible paths is again admissible, the framework can show that a minimizer exists without adding extra assumptions about staying positive.

The declaration also records the boundary behavior at the two extremes. Setting s = 0 returns the first path; setting s = 1 returns the second. These are not separate claims but part of the same definition, spelled out as lemmas. The whole module, including this result, is checked by the machine with no unproved axioms in its own code, a status string in the file confirms.

What the declaration does not do is assert that the blended path is the minimizer, or even that a minimizer exists. It only guarantees that the interpolation preserves the fixed-endpoint condition. The existence of a minimizing path, and the claim that it solves an Euler-Lagrange equation, live in separate parts of the library that this declaration does not touch. The result is a piece of infrastructure, not a conclusion about physics.

/-- Interpolation preserves shared endpoints. -/
lemma interp_fixedEndpoints {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
    (h : fixedEndpoints γ₁ γ₂) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
    fixedEndpoints γ₁ (interp γ₁ γ₂ s hs) := by
  refine ⟨?_, ?_⟩
  · simp [interp_apply, h.1]; ring
  · simp [interp_apply, h.2]; ring

/-- Interpolation at `s = 0` is the first path. -/
lemma interp_zero {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
    ∀ t, (interp γ₁ γ₂ 0 ⟨le_refl 0, by norm_num⟩).toFun t = γ₁.toFun t := by
  intro t; simp [interp_apply]

/-- Interpolation at `s = 1` is the second path. -/
lemma interp_one {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) :
    ∀ t, (interp γ₁ γ₂ 1 ⟨by norm_num, le_refl 1⟩).toFun t = γ₂.toFun t := by
  intro t; simp [interp_apply]

What this page does not claim

This declaration does not prove that a minimizing path exists. It does not assert that the blended path is the minimizer. It does not derive the Euler-Lagrange equations or any physical law.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Action/PathSpace.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: