Normalization
plain-language theorem explainer
Normalization is the class asserting that any cost functional F satisfies F(1) = 0. Derivations of the J-cost function and the full cost algebra cite it as the first primitive axiom in the Recognition Science hierarchy. The declaration is a class with the single field unit_zero encoding the zero-cost condition at the multiplicative identity.
Claim. A function $F : ℝ → ℝ$ satisfies Normalization when $F(1) = 0$.
background
The CostAxioms module states the three primitive axioms from which Recognition Science derives all structure. Normalization is Axiom 1: the cost at unity is zero. This encodes that perfect balance (ratio = 1) has no cost; any cost functional measuring deviation must vanish at the reference point. The module then introduces Axiom 2 (Composition), the d'Alembert equation $F(xy) + F(x/y) = 2F(x)F(y) + 2F(x) + 2F(y)$ for positive x, y, and Axiom 3 (Calibration) fixing the log-second derivative at the origin to 1.
proof idea
one-line wrapper that introduces the Normalization class with the single field unit_zero : F 1 = 0.
why it matters
Normalization supplies the zero-cost condition required by CostAlgebraData and cost_algebra_certificate to package the complete algebraic data for J. It is the base level of the axiomatic hierarchy that forces J-uniqueness (T5) via the Recognition Composition Law and the eight-tick octave. The economic reading in the module doc-comment states that J(1) = 0 means unity costs nothing while J(0) → ∞ prevents self-recognition of nothingness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.