IsNormalized
plain-language theorem explainer
IsNormalized encodes the normalization condition that a cost functional vanishes at unity. Researchers proving uniqueness of the canonical J-cost in Recognition Science cite it when assembling the primitive hypothesis bundle for T5. The declaration is a direct one-line abbreviation of F(1) = 0 with no further proof steps.
Claim. A function $F : (0,∞) → ℝ$ is normalized when $F(1) = 0$.
background
The module proves that any cost functional obeying symmetry, normalization, and a symmetric quadratic composition law must reduce to the d'Alembert form. Normalization is introduced explicitly as the statement that the cost of no deviation from unity is zero. This matches the upstream definition in Cost.FunctionalEquation.IsNormalized, which supplies the first calibration condition in the axiom bundle. The local theoretical setting is the inevitability argument that closes the gap between the three axioms (normalization, reciprocity, composition) and the RCL equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
This declaration is a direct definition with no computational content or proof steps.
why it matters
It supplies axiom A1 (normalization) in the core theorem of the module. Downstream results cost_algebra_unique and cost_algebra_unique_aczel invoke it to conclude that any CostAlgebraData satisfying the remaining hypotheses must equal J, completing T5 of the forcing chain. The same condition appears in PrimitiveCostHypotheses and washburn_uniqueness_of_contDiff, where it combines with the composition law to derive reciprocity without separate assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.