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

const

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

Lean usage

AdmissiblePath.const a b 1 (by norm_num)

formal statement (Lean)

  52def const (a b c : ℝ) (hc : 0 < c) : AdmissiblePath a b where
  53  toFun := fun _ => c

proof body

Definition body.

  54  cont := continuousOn_const
  55  pos := fun _ _ => hc
  56

used by (17)

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.