fixedEndpoints
fixedEndpoints encodes the boundary condition requiring two admissible paths on [a,b] to agree at the endpoints a and b. Variational analysts deriving uniqueness and minimization results for the J-action cite this relation to restrict the class of competitors. The definition is the direct conjunction of two pointwise equalities on the underlying functions of the paths.
claimLet $a,b$ be real numbers with $a≤b$ and let $γ_1,γ_2$ be continuous strictly positive functions on the closed interval $[a,b]$. Then $γ_1(a)=γ_2(a)$ and $γ_1(b)=γ_2(b)$.
background
AdmissiblePath a b is the structure whose underlying function is continuous on the closed interval Icc a b and strictly positive at every point of that interval. Module PathSpace sets up the variational stage for the principle of least action derived from the J-cost functional. It introduces admissible paths, the action integral, the fixedEndpoints boundary relation, and the straight-line interpolation in path space; the module records that admissible paths remain admissible under convex combinations. This boundary condition is the explicit hypothesis in downstream uniqueness and minimization statements.
proof idea
The definition is the conjunction of the two equalities that the underlying functions agree at the left endpoint a and at the right endpoint b.
why it matters in Recognition Science
This supplies the shared-endpoint hypothesis required by the uniqueness and minimization theorems in FunctionalConvexity. It appears directly in actionJ_minimum_unique_value, geodesic_minimizes_unconditional, geodesic_minimizes_via_convexity, and principle_of_least_action, which together establish that a critical path for the J-action is a global minimizer among all admissible competitors with the same endpoints. In the Recognition Science framework the relation closes the variational stage that converts convexity of the action functional into the unconditional principle of least action.
scope and limits
- Does not require differentiability of the paths.
- Does not constrain values of the paths in the open interval (a,b).
- Does not depend on the explicit form of the J functional.
- Does not assert existence of admissible paths satisfying the condition.
Lean usage
theorem min_unique_example (hab : a ≤ b) (γ1 γ2 : AdmissiblePath a b) (h : fixedEndpoints γ1 γ2) (h1 : ∀ γ, fixedEndpoints γ1 γ → actionJ γ1 ≤ actionJ γ) (h2 : ∀ γ, fixedEndpoints γ2 γ → actionJ γ2 ≤ actionJ γ) : actionJ γ1 = actionJ γ2 := actionJ_minimum_unique_value hab γ1 γ2 h h1 h2formal statement (Lean)
91def fixedEndpoints {a b : ℝ} (γ₁ γ₂ : AdmissiblePath a b) : Prop :=
proof body
Definition body.
92 γ₁.toFun a = γ₂.toFun a ∧ γ₁.toFun b = γ₂.toFun b
93