pith. sign in
module module high

IndisputableMonolith.Action.PathSpace

show as:
view Lean formalization →

PathSpace defines admissible paths as continuous strictly positive functions on a closed interval. It supplies the basic type and operations (constant paths, endpoint fixing) used by the variational modules. The module is imported by EulerLagrange, FunctionalConvexity and QuadraticLimit; it contains only definitions and elementary lemmas with no proofs.

claimAn admissible path on a closed interval $I=[a,b]$ is a continuous map $γ:I→ℝ_{>0}$. The module also equips this type with constant paths and the reflexive, symmetric and transitive relations for fixed endpoints.

background

The module belongs to the Action domain and imports Cost together with Cost.Convexity. The latter proves that Jlog(t)=cosh t−1 is strictly convex on ℝ and that Jcost(x)=½(x+x⁻¹)−1 is strictly convex on ℝ₊; these facts support the J-uniqueness result T5. The local theoretical setting is the construction of the path space on which the cost-rate action S[γ]=∫J(γ(t))dt is defined.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

PathSpace supplies the domain for the Euler–Lagrange equations in EulerLagrange and for the convexity arguments that discharge the conditional hypothesis in FunctionalConvexity. It is also required for the small-strain reduction to Newton’s second law in QuadraticLimit.

scope and limits

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (18)