IsNormalizedCost
plain-language theorem explainer
Normalized cost requires that a cost function F satisfies F(1) = 0. Researchers establishing the minimal foundations of Recognition Science cite this definition when isolating the three primitive requirements for cost functions. It is introduced as a direct one-line definition that encodes the physical requirement that zero deviation produces zero cost.
Claim. A cost function $F : ℝ → ℝ$ is normalized when $F(1) = 0$.
background
The module states the tightest form of RCL inevitability by reducing the five assumptions from Unconditional to three primitive requirements: symmetry, normalization, and consistency. Normalization is defined as F(1) = 0, expressing that no deviation from the reference incurs no cost; the module presents this as definitional rather than a physics assumption. The local setting treats calibration F''(1) = 1 and smoothness C² as separate regularity conditions, not part of the core requirements.
proof idea
The declaration is a direct definition that sets IsNormalizedCost F to the proposition F 1 = 0.
why it matters
This definition supplies the normalization requirement inside the ultimate_inevitability theorem, which shows that symmetry, normalization, and consistency plus regularity force F to equal J and the combiner to equal the RCL. It marks the second of the three primitive requirements in the minimal foundation, confirming that the RCL emerges as what comparison means rather than an extra postulate. The parent theorems are normalization_is_essential and ultimate_inevitability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.