IsNormalized
plain-language theorem explainer
The normalization condition requires a cost function F to satisfy F(1) = 0. Uniqueness arguments for the canonical J-cost under T5 invoke this predicate together with calibration and the composition law. The declaration is a direct one-line predicate definition.
Claim. A cost function $F : ℝ → ℝ$ is normalized when $F(1) = 0$.
background
The FunctionalEquation module supplies helper definitions for the T5 cost uniqueness proof. Normalization requires the cost to vanish at the multiplicative unit. The reparametrization G(t) = F(exp t) converts this to G(0) = 0. Upstream, the Calibration axiom from CostAxioms states that the second derivative of G at zero equals 1, pairing with normalization to select a unique solution. The identical predicate appears in the DAlembert.Inevitability module as the first normalization step before the functional equation is applied.
proof idea
One-line definition of the predicate F(1) = 0.
why it matters
This definition supplies the normalization hypothesis in cost_algebra_unique and cost_algebra_unique_aczel, both of which conclude that any cost algebra obeying the axioms equals J. It therefore fills the normalization slot in the T5 uniqueness result of the forcing chain. The same predicate is reused in PrimitiveCostHypotheses and in the AczelClassification lemmas that derive H(0) = 1 from normalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.