const
plain-language theorem explainer
Definition of the constant admissible path at height c > 0 on any interval [a, b]. Researchers deriving the J-action or testing convexity in path space cite this constructor for uniform trajectories. It is assembled directly from the AdmissiblePath structure by supplying the constant function, continuousOn_const, and the given positivity hypothesis.
Claim. Let $a, b, c$ be real numbers with $c > 0$. The constant function $tmapsto c$ on the closed interval $[a, b]$ is continuous and strictly positive, hence an admissible path.
background
AdmissiblePath a b is the structure whose fields are a function toFun : R to R, a proof cont that it is ContinuousOn the closed interval Icc a b, and a proof pos that toFun t > 0 for every t in Icc a b. The PathSpace module introduces this structure together with the J-action integral and the fixedEndpoints relation to set up the variational principle of least action derived from the d'Alembert cost J. The constant-path definition supplies the simplest admissible trajectory for evaluating that integral.
proof idea
One-line wrapper that applies the AdmissiblePath constructor to the constant function, using continuousOn_const for the cont field and the hypothesis hc directly for the pos field.
why it matters
The definition is invoked by actionJ_const_one to show that the action of the unit constant path is zero, and appears in downstream arguments in GalaxyRotation, ILGDerivation, and the LinearLogicBridge. It supports the least-action setup recorded in papers/RS_Least_Action.tex by furnishing explicit admissible paths needed for the strict-convexity argument in Action.FunctionalConvexity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.