fixedEndpoints_trans
Transitivity of the fixed-endpoints relation on admissible paths. Researchers deriving the least-action principle from the J-cost functional cite it when chaining boundary conditions across sequences of paths. The proof is a one-line term-mode construction that applies equality transitivity to the pair of endpoint conditions.
claimLet $a,b$ be real numbers and let $γ_1,γ_2,γ_3$ be admissible paths on the closed interval $[a,b]$, i.e., continuous and strictly positive functions on $[a,b]$. If $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$, and likewise $γ_2(a)=γ_3(a)$ and $γ_2(b)=γ_3(b)$, then $γ_1(a)=γ_3(a)$ and $γ_1(b)=γ_3(b)$.
background
AdmissiblePath a b is the structure whose fields are a function toFun : R → R together with proofs that it is continuous on Icc a b and strictly positive there. fixedEndpoints γ1 γ2 is the proposition γ1.toFun a = γ2.toFun a ∧ γ1.toFun b = γ2.toFun b. The module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J, with paper companion papers/RS_Least_Action.tex. The key structural fact recorded here is that admissible paths remain admissible under convex interpolation.
proof idea
The proof is a term-mode construction that builds the required pair by applying transitivity of equality to the two components of the hypotheses: the a-endpoint equality via h1.1.trans h2.1 and the b-endpoint equality via h1.2.trans h2.2.
why it matters in Recognition Science
This lemma completes the equivalence-relation structure on fixedEndpoints (with the reflexivity and symmetry siblings in the same module). It supports the strict-convexity argument of Action.FunctionalConvexity by allowing consistent boundary conditions across interpolated paths. The module records that admissible paths remain admissible under convex combinations, which is what enables the J-action functional to be well-defined on path space without extra positivity hypotheses.
scope and limits
- Does not establish any properties of the J-action integral itself.
- Does not address convexity or positivity of the action functional.
- Does not extend to paths on open intervals or with non-fixed endpoints.
- Does not provide existence or uniqueness results for action minimizers.
formal statement (Lean)
101lemma fixedEndpoints_trans {a b : ℝ} {γ₁ γ₂ γ₃ : AdmissiblePath a b}
102 (h₁ : fixedEndpoints γ₁ γ₂) (h₂ : fixedEndpoints γ₂ γ₃) :
103 fixedEndpoints γ₁ γ₃ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩
proof body
Term-mode proof.
104
105/-! ## Convex interpolation in path space -/
106
107/-- The straight-line interpolation between two admissible paths.
108
109 `interp γ₁ γ₂ s = (1 - s) · γ₁ + s · γ₂`.
110
111 The key structural fact is that for `s ∈ [0,1]`, this convex combination
112 is again strictly positive and continuous, hence again admissible. -/