Normalization
plain-language theorem explainer
Normalization encodes the zero-cost condition at unity for any cost functional F. Algebraists deriving the J-cost function cite this axiom as the fixed point for the Recognition Composition Law. The declaration is a direct class definition introducing the unit_zero field with no further proof obligations.
Claim. Let $F : (0,∞) → ℝ$ be a cost functional. Then $F(1) = 0$.
background
The module CostAxioms introduces the three primitive axioms of Recognition Science. Axiom 1 (Normalization) states that the cost at unity vanishes: F(1) = 0. This encodes that perfect balance (ratio = 1) has no cost. Any cost functional measuring deviation must vanish at the reference point. Axiom 2 (Composition) is the Recognition Composition Law: F(xy) + F(x/y) = 2 F(x) F(y) + 2 F(x) + 2 F(y) for positive x, y. Axiom 3 (Calibration) fixes the second derivative of the log-transformed functional at the origin to equal 1. These axioms sit at LEVEL 0 and force the unique J-cost at LEVEL 1.
proof idea
This is a class definition with a single field unit_zero. No tactics or lemmas are applied; the declaration directly asserts F 1 = 0 as a Prop.
why it matters
Normalization is Axiom 1 in the primitive hierarchy and feeds directly into CostAlgebraData and the cost_algebra_certificate. It anchors the uniqueness proof for J(x) = ½(x + x⁻¹) − 1 (T5) and the subsequent derivation of the phi-ladder, eight-tick octave, and D = 3. Downstream results such as composition_law_equiv_coshAdd and JcostN_eq_cosh_logsum rely on this zero-cost reference to convert the multiplicative law into the additive cosh identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.