actionJ_minimum_unique_value
plain-language theorem explainer
Two admissible paths that each minimize the J-action among all paths sharing their endpoints must share the same action value. Researchers deriving the unconditional principle of least action cite this uniqueness step to close the comparison before invoking convexity. The argument is a direct symmetric application of the two minimality hypotheses, which forces equality by linear arithmetic.
Claim. Let $a ≤ b$ and let $γ_1, γ_2$ be admissible paths on $[a,b]$ that share endpoints. If $S[γ_1] ≤ S[γ]$ for every admissible $γ$ sharing endpoints with $γ_1$, and likewise $S[γ_2] ≤ S[γ]$ for every admissible $γ$ sharing endpoints with $γ_2$, then $S[γ_1] = S[γ_2]$, where $S[γ] = ∫_a^b J(γ(t)) dt$.
background
The J-action functional is the integral $S[γ] = ∫_a^b Jcost(γ(t)) dt$ over an admissible path, where admissible paths are continuous strictly positive real functions on the closed interval $[a,b]$. Fixed endpoints is the predicate that two paths agree at the endpoints $a$ and $b$. The interpolation operator produces the convex combination $(1-s)γ_1 + s γ_2$, which remains admissible for $s ∈ [0,1]$. This module proves that the action inherits convexity on such interpolations from the pointwise convexity of Jcost, which itself follows from d'Alembert uniqueness. The upstream definition of actionJ and the fixedEndpoints predicate supply the objects used here.
proof idea
One-line wrapper. Apply the first minimality hypothesis to γ₂ (using the shared-endpoints assumption) to obtain actionJ γ₁ ≤ actionJ γ₂. Apply the second hypothesis to γ₁ after symmetry of fixedEndpoints to obtain actionJ γ₂ ≤ actionJ γ₁. Linear arithmetic then yields equality.
why it matters
This uniqueness result closes the comparison step inside the headline unconditional principle of least action (geodesic_minimizes_unconditional) and the broader principle_of_least_action sibling. It removes the need for an extra h_min witness once convexity of actionJ on interpolations is available, which traces directly to the J-functional equation and d'Alembert factorization. The module doc notes that the deep content is the convexity statement itself; this lemma is the elementary convex-calculus consequence that propagates local segment minimization to global uniqueness of the action value.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.