IsNormalizedCost
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove existence of any F satisfying the condition.
- Does not enforce symmetry or multiplicative consistency.
- Does not incorporate smoothness or unit calibration.
- Does not restrict the domain beyond real numbers.
formal statement (Lean)
68def IsNormalizedCost (F : ℝ → ℝ) : Prop := F 1 = 0
proof body
Definition body.
69
70/-- Consistency: F(xy) + F(x/y) = P(F(x), F(y)) for some P.
71 This is the DEFINITION of multiplicative consistency. -/