fixedEndpoints_refl
plain-language theorem explainer
The reflexivity of endpoint agreement for any admissible path is recorded here. Analysts building the variational formulation of least action from the J-cost would cite this when verifying that fixedEndpoints forms a reflexive relation on positive continuous paths. The proof is a direct one-line reduction to the definition of fixedEndpoints via reflexivity of equality.
Claim. Let $a, b$ be real numbers and let $γ$ be a continuous strictly positive function on the closed interval $[a, b]$. Then $γ(a) = γ(a)$ and $γ(b) = γ(b)$.
background
The PathSpace module defines admissible paths as continuous functions from the closed interval $[a, b]$ to the positive reals. The predicate fixedEndpoints between two such paths holds exactly when the functions agree at the left endpoint $a$ and the right endpoint $b$ (see the upstream definition). This supplies the reflexive instance of that predicate.
proof idea
The proof is a one-line wrapper that applies the definition of fixedEndpoints and invokes reflexivity of equality on each endpoint value.
why it matters
This supplies the reflexive case for the fixedEndpoints relation used to set up the variational stage for the J-action functional. It is a prerequisite for later convexity and interpolation arguments in the same module that support the least-action principle. No downstream theorems are recorded among the dependents.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.