const_apply
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.
claimLet γ 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 in Recognition Science
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.
scope and limits
- Does not prove continuity or positivity of the path.
- Does not compute or bound the J-action integral.
- Does not apply to non-constant paths.
- Does not address boundary conditions or endpoint fixing.
Lean usage
unfold actionJ; simp [const_apply, Jcost_unit0]formal statement (Lean)
57@[simp] lemma const_apply {a b c : ℝ} (hc : 0 < c) (t : ℝ) :
58 (const a b c hc).toFun t = c := rfl
proof body
Term-mode proof.
59
60end AdmissiblePath
61
62/-! ## The J-action functional -/
63
64/-- The J-action functional `S[γ] = ∫_a^b J(γ(t)) dt`.
65
66 This is the central object of the variational principle. Geodesics of
67 the Hessian metric `g(x) = J''(x) = 1/x³` minimize this functional
68 among admissible paths with fixed endpoints. -/