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

IsNormalized

show as:
view Lean formalization →

A cost function F is normalized precisely when F(1) equals zero. Researchers proving T5 uniqueness of the J-cost under composition and calibration cite this predicate as the zero-point anchor. The declaration is a direct one-line definition that supplies the base hypothesis for downstream Aczél and cost-algebra results.

claimLet $F : (0,∞) → ℝ$. The function $F$ is normalized when $F(1) = 0$.

background

The Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. Normalization fixes the zero of the cost at unit scale and pairs with the reparametrization $G(t) := F(e^t)$ together with the Calibration axiom requiring $G''(0) = 1$. Upstream, DAlembert.Inevitability supplies the identical predicate while CostAxioms.Calibration states that the second derivative at the origin equals 1, ensuring a unique solution rather than a family.

proof idea

This is a one-line definition that directly encodes the predicate $F(1) = 0$. No lemmas or tactics are applied; the declaration serves as the base predicate for results such as H_one_of_normalized and the uniqueness theorems in CostAlgebra.

why it matters in Recognition Science

The definition supplies the normalization hypothesis required by the parent theorems cost_algebra_unique and cost_algebra_unique_aczel, which establish that any cost satisfying the composition law, reciprocity, and calibration must coincide with the J function. It corresponds to the first calibration step in T5 J-uniqueness of the forcing chain and touches the question of minimal regularity needed to force the self-similar fixed point.

scope and limits

Lean usage

have hNorm : IsNormalized F := by simpa [IsNormalized] using hF1

formal statement (Lean)

 597def IsNormalized (F : ℝ → ℝ) : Prop := F 1 = 0

proof body

Definition body.

 598
 599/-- **Calibration (Condition 1.2)**:
 600lim_{t→0} 2·F(e^t)/t² = 1, equivalently G''(0) = 1 where G(t) = F(e^t). -/

used by (23)

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

depends on (10)

Lean names referenced from this declaration's body.