IsNormalized
plain-language theorem explainer
Normalized cost functions satisfy F(1)=0. Researchers proving T5 uniqueness via the composition law or Aczél classification cite this condition to fix the additive constant before invoking calibration or reciprocity. The declaration is a direct abbreviation with no further reduction.
Claim. A function $F : (0,∞) → ℝ$ is normalized when $F(1) = 0$.
background
The module supplies functional-equation lemmas for the T5 cost-uniqueness proof. Normalization pairs with the Calibration axiom (second derivative of G at 0 equals 1, where G(t) = F(exp t)) and with the reparametrization G(F,t) = F(exp t). The same predicate appears upstream in the DAlembert inevitability module as the statement F(1)=0.
proof idea
Direct definition of the zero-at-unity condition.
why it matters
It supplies the normalized hypothesis in cost_algebra_unique and cost_algebra_unique_aczel, both of which conclude that cost equals J. The predicate also appears inside PrimitiveCostHypotheses and H_one_of_normalized. It therefore anchors the T5 step of the forcing chain (T5 J-uniqueness) once the composition law and calibration are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.