const
plain-language theorem explainer
Constant paths at a fixed positive height c on a closed interval [a, b]. Analysts deriving the least-action principle from the J-cost cite this when they need explicit positive test functions. The definition assembles the AdmissiblePath record by wiring the constant map to the continuity and positivity fields.
Claim. Let $a, b, c$ be real numbers with $c > 0$. The function $tmapsto c$ is continuous and strictly positive on the closed interval $[a, b]$, hence an admissible path.
background
PathSpace equips the variational calculus for the J-action functional. An admissible path on the interval [a, b] is a continuous map from the closed interval Icc a b into the positive reals. The module records that such paths remain admissible under convex combinations, which later supports strict convexity arguments.
proof idea
The definition is a direct structure constructor. It sets the toFun field to the constant function, fills the cont field with the library lemma continuousOn_const, and supplies the pos field by lambda-abstraction over the hypothesis hc : 0 < c.
why it matters
This supplies the constant test paths required to show that the J-action vanishes on the unit constant path. Downstream it appears in galaxy rotation models and in the linear logic bridge for counted-once resources. It anchors the comparison between constant and non-constant paths inside the Recognition least-action derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.