pith. machine review for the scientific record. sign in
structure definition def or abbrev high

AdmissiblePath

show as:
view Lean formalization →

Admissible paths on a closed interval [a, b] are continuous strictly positive real-valued functions. Variational analysts in the Recognition Science setting cite this structure when constructing the J-action functional and proving convexity-based minimization. The declaration is a direct structure definition that bundles the underlying map with its continuity and positivity fields.

claimAn admissible path on the interval $[a, b]$ is a function $f : [a, b] → ℝ$ that is continuous on the closed interval $[a, b]$ and satisfies $f(t) > 0$ for all $t ∈ [a, b]$.

background

The PathSpace module sets up the variational stage for the principle of least action derived from the d'Alembert cost functional J. It defines admissible paths as continuous strictly positive functions on [a, b], together with the action integral actionJ γ = ∫ J(γ(t)) dt and the fixedEndpoints relation. The module records that such paths remain admissible under convex interpolation, which removes any need for extra positivity hypotheses in later convexity arguments.

proof idea

The declaration is a structure definition with three fields: toFun for the underlying map, cont for ContinuousOn on Icc a b, and pos for the strict positivity forall condition. No lemmas or tactics are invoked; the structure simply packages the required properties.

why it matters in Recognition Science

This definition supplies the domain for the action functional and feeds directly into the convexity theorems of FunctionalConvexity, including actionJ_convex_on_interp, geodesic_minimizes_unconditional, and principle_of_least_action. It thereby supports the unconditional least-action result that connects the J-functional to the Recognition Science forcing chain and the derivation of spatial dimensions.

scope and limits

formal statement (Lean)

  33structure AdmissiblePath (a b : ℝ) where
  34  /-- The underlying function. -/
  35  toFun : ℝ → ℝ
  36  /-- Continuity on the closed interval. -/
  37  cont : ContinuousOn toFun (Icc a b)
  38  /-- Strict positivity on the closed interval. -/
  39  pos : ∀ t ∈ Icc a b, 0 < toFun t
  40
  41namespace AdmissiblePath
  42
  43variable {a b : ℝ}
  44
  45instance : CoeFun (AdmissiblePath a b) (fun _ => ℝ → ℝ) := ⟨AdmissiblePath.toFun⟩

proof body

Definition body.

  46

used by (23)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.