IndisputableMonolith.Action.PathSpace
PathSpace defines admissible paths as continuous strictly positive functions on closed intervals for use in J-action functionals. Researchers deriving Euler-Lagrange equations or action convexity cite it as the basic domain. It also supplies fixed-endpoint relations and basic action definitions. The module is purely definitional.
claimAn admissible path on an interval $[a,b]$ is a continuous function $\gamma:[a,b]\to\mathbb{R}_{>0}$.
background
The module sits in the Action domain and imports J-cost definitions together with the convexity results on Jcost(x) = ½(x + x⁻¹) - 1. The upstream Convexity module states that Jlog(t) = cosh t - 1 is strictly convex on ℝ and that Jcost is strictly convex on ℝ₊, foundational for the uniqueness theorem T5. AdmissiblePath and fixedEndpoints encode the paths and endpoint-matching relation over which the action integral is taken.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
It supplies the path space required by EulerLagrange to reduce the EL equation to γ(t) ≡ 1, by FunctionalConvexity to establish convexity of S[γ] = ∫ J(γ(t)) dt and remove conditional hypotheses, and by QuadraticLimit to recover the Newtonian small-strain regime. It therefore anchors the variational formulation of the J-action.
scope and limits
- Does not equip the path space with a topology or metric.
- Does not prove existence or uniqueness of minimizers.
- Does not connect paths to the phi-ladder or mass formula.
- Does not address the forcing chain steps T0-T8.
used by (3)
depends on (2)
declarations in this module (18)
-
structure
AdmissiblePath -
lemma
coe_mk -
def
const -
lemma
const_apply -
def
actionJ -
lemma
actionJ_def -
lemma
actionJ_nonneg -
lemma
actionJ_const_one -
def
fixedEndpoints -
lemma
fixedEndpoints_refl -
lemma
fixedEndpoints_symm -
lemma
fixedEndpoints_trans -
def
interp -
lemma
interp_apply -
lemma
interp_zero -
lemma
interp_one -
lemma
interp_fixedEndpoints -
def
pathSpace_status