Action Path Space Fixed Endpoints Symm

The symmetry of shared endpoints

In the calculus of variations, a path is a continuous curve between two points, and the action is a number assigned to that curve. The classical problem is to find the path that minimizes the action among all curves with the same endpoints. The framework's library sets up this stage with a specific action functional, and one of its basic lemmas, fixedEndpoints_symm, states a simple symmetry: if two admissible paths share their starting value and their ending value, then that relation holds in reverse as well. If path A and path B both begin at 5 and end at 9, then B and A also both begin at 5 and end at 9. The proof is immediate from the definition, but recording it as a formal theorem is what lets later arguments use the symmetry without rechecking it.

The definition of admissible path requires continuity and strict positivity on the interval. The action functional is the integral of Jcost, a cost function that vanishes at 1 and grows as the path moves away from that value. The constant path at 1 has zero action, and all admissible paths have non-negative action. The symmetry lemma itself does not depend on the specific form of Jcost; it holds for any two paths that satisfy the endpoint condition. This is a structural fact about the path space, not a claim about the minimizer.

The library also proves that the endpoint relation is reflexive and transitive, and that straight-line interpolation between two admissible paths preserves shared endpoints. These are the basic tools for the convexity argument that shows the action functional has a unique minimizer. The symmetry lemma is the smallest piece of that structure: it says the comparison of two paths does not care about order, which is what makes the later convexity argument symmetric in its two inputs.

In Recognition Science, the action functional is derived from the cost function J, and the variational principle selects the path that minimizes it. The framework's library records this as a machine-checked collection of formal theorems, and the symmetry lemma is one of the first steps in that chain. What it does not claim is that the minimizer itself is symmetric, or that the action value is the same for two paths that merely share endpoints. It claims only the symmetry of the endpoint relation, nothing more.

lemma fixedEndpoints_symm {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
    (h : fixedEndpoints γ₁ γ₂) : fixedEndpoints γ₂ γ₁ :=
  ⟨h.1.symm, h.2.symm⟩

lemma fixedEndpoints_refl {a b : ℝ} (γ : AdmissiblePath a b) :
    fixedEndpoints γ γ := And.intro rfl rfl

lemma fixedEndpoints_trans {a b : ℝ} {γ₁ γ₂ γ₃ : AdmissiblePath a b}
    (h₁ : fixedEndpoints γ₁ γ₂) (h₂ : fixedEndpoints γ₂ γ₃) :
    fixedEndpoints γ₁ γ₃ := ⟨h₁.1.trans h₂.1, h₁.2.trans h₂.2⟩

/-- Interpolation preserves shared endpoints. -/
lemma interp_fixedEndpoints {a b : ℝ} {γ₁ γ₂ : AdmissiblePath a b}
    (h : fixedEndpoints γ₁ γ₂) (s : ℝ) (hs : s ∈ Icc (0:ℝ) 1) :
    fixedEndpoints γ₁ (interp γ₁ γ₂ s hs) := by
  refine ⟨?_, ?_⟩
  · simp [interp_apply, h.1]; ring
  · simp [interp_apply, h.2]; ring

/-- The action of any admissible path is non-negative. -/
lemma actionJ_nonneg {a b : ℝ} (hab : a ≤ b) (γ : AdmissiblePath a b) :
    0 ≤ actionJ γ := by
  unfold actionJ
  exact intervalIntegral.integral_nonneg hab
    (fun t ht => Jcost_nonneg (γ.pos t ht))

What this page does not claim

The symmetry lemma does not claim that the action value is the same for two paths that merely share endpoints. It does not claim that the minimizer itself is symmetric under reversal of the path order. It does not claim that the endpoint relation holds for paths that are not admissible.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Action/PathSpace.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: