const_apply
plain-language theorem explainer
The constant admissible path at fixed value c > 0 evaluates to c at every real t. Researchers deriving the variational principle for the J-action functional cite this when reducing integrals over stationary trajectories. The proof is a direct reflexivity reduction on the definition of the constant-path constructor.
Claim. Let γ be the constant admissible path on [a, b] taking the fixed value c > 0. Then γ(t) = c for every real t.
background
AdmissiblePath a b is the structure consisting of a continuous function toFun : ℝ → ℝ that is strictly positive on the closed interval Icc a b. The constant-path constructor builds an element of this structure by setting toFun to the constant value c (with the positivity hypothesis hc : 0 < c) and supplying the trivial continuity proof continuousOn_const. The module sets up the J-action functional S[γ] = ∫_a^b J(γ(t)) dt whose minimizers are geodesics of the Hessian metric g(x) = J''(x) = 1/x³ among paths with fixed endpoints.
proof idea
The proof is a one-line term-mode reflexivity that matches the toFun field of the constant-path constructor directly against the constant value c.
why it matters
This lemma is invoked by the downstream result showing that the J-action of the constant path at value 1 vanishes, confirming that the unit constant trajectory realizes the cost minimum. It therefore supports the variational principle derived from the d'Alembert cost J and the Recognition Science forcing chain at the stage where J-uniqueness (T5) and the self-similar fixed point phi (T6) are already in place. The module documentation records that admissible paths are closed under convex interpolation, which this constant-path fact helps to instantiate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.