pith. sign in
module module high

IndisputableMonolith.Action.PathSpace

show as:
view Lean formalization →

The PathSpace module defines the space of admissible paths for the J-action as continuous strictly positive functions on closed intervals, together with the integrated action functional and fixed-endpoint predicates. Researchers formalizing the variational principle in Recognition Science cite it when constructing the domain for cost-rate minimization. The module is purely definitional and supplies the basic objects used by the three downstream Action modules.

claimAn admissible path on $[a,b]$ is a continuous function $γ:[a,b]→ℝ^+$ with $γ(t)>0$ for all $t$. The associated action is $S[γ]=∫_a^b J(γ(t))dt$ where $J(x)=½(x+x^{-1})-1$, together with the predicates fixedEndpoints$(γ,γ_0,γ_1)$ enforcing $γ(a)=γ_0$ and $γ(b)=γ_1$.

background

The module belongs to the Action domain and imports Cost (which supplies the pointwise cost $J$) and Cost.Convexity (which establishes strict convexity of $J$ on $ℝ^+$). Its central definition states that an admissible path on $[a,b]$ is a continuous, strictly positive function. The fixedEndpoints relation and the constant-path constructor are introduced to support later variational arguments. The upstream Convexity module states: “This module proves that Jlog(t)=cosh t−1 is strictly convex on ℝ and Jcost(x)=½(x+x^{-1})−1 is strictly convex on ℝ₊.”

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

PathSpace supplies the path space, action functional, and endpoint conditions required by EulerLagrange (which reduces the EL equation to the constant path γ≡1), FunctionalConvexity (which uses the definitions to prove convexity of S and discharge the h_min hypothesis), and QuadraticLimit (which performs the small-strain expansion of J). It therefore forms the definitional base for the J-action variational principle that connects to the Recognition Science cost manifold.

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)