fixedEndpoints_refl
The lemma records that every admissible path satisfies the fixed-endpoints relation with itself. Workers on the variational formulation of least action in Recognition Science invoke this reflexivity when treating fixedEndpoints as an equivalence on path space. The argument is a direct unfolding of the definition of fixedEndpoints together with reflexivity of equality at the two endpoints.
claimLet $a,b$ be real numbers and let $γ$ be a continuous strictly positive function on the closed interval $[a,b]$. Then $γ$ agrees with itself at the endpoints: $γ(a)=γ(a)$ and $γ(b)=γ(b)$.
background
AdmissiblePath $a$ $b$ is the structure whose carrier is a function $ℝ→ℝ$ that is continuous on $[a,b]$ and strictly positive there. The predicate fixedEndpoints $γ₁$ $γ₂$ is the conjunction of the two endpoint equalities $γ₁(a)=γ₂(a)$ and $γ₁(b)=γ₂(b)$ (see the definition at line 91 of the same module).
proof idea
One-line wrapper that applies the definition of fixedEndpoints to the pair $(γ,γ)$ and introduces the two reflexive equalities.
why it matters in Recognition Science
The reflexivity statement supplies the first leg of the equivalence-relation structure on admissible paths that the module uses to set up the J-action variational problem. It sits alongside the symmetry and transitivity lemmas in the same file and supports the convex-interpolation closure recorded in the module documentation, which in turn enables the strict-convexity argument of Action.FunctionalConvexity.
scope and limits
- Does not apply to functions that fail strict positivity on the interval.
- Does not compute or bound the value of the action integral.
- Does not address paths outside the closed interval $[a,b]$.
formal statement (Lean)
94lemma fixedEndpoints_refl {a b : ℝ} (γ : AdmissiblePath a b) :
95 fixedEndpoints γ γ := And.intro rfl rfl
proof body
96