normalization_is_essential
plain-language theorem explainer
The map F(x) = (x + x^{-1})/2 fails the normalization condition F(1) = 0. Researchers deriving the minimal axioms for multiplicative cost functions cite the result to show why the raw hyperbolic form must be shifted before it can serve as a cost. The argument is a direct simplification of the normalization predicate after assuming the contrary.
Claim. The function defined by $F(x) := (x + x^{-1})/2$ does not satisfy $F(1) = 0$.
background
In the Ultimate Inevitability module the five assumptions of the unconditional RCL theorem are reduced to three primitive requirements: symmetry (F(x) = F(1/x)), normalization (F(1) = 0), and multiplicative consistency. Normalization is presented as the definition of a cost of deviation rather than an extra hypothesis. The sibling definition IsNormalizedCost encodes exactly this predicate: F 1 = 0. Upstream, the cost functions extracted from MultiplicativeRecognizerL4 and ObserverForcing are the concrete maps to which the predicate is applied.
proof idea
One-line wrapper that applies simplification to the IsNormalizedCost predicate after introducing the assumption.
why it matters
The declaration sits inside the module that states the tightest form of RCL inevitability, showing that normalization is definitional for any cost of comparison. It directly supports the claim that the raw (x + x^{-1})/2 form cannot serve as a cost without the additive shift that produces J, thereby feeding the T5 J-uniqueness step of the forcing chain. The result closes one route by which a non-normalized candidate could evade the minimal foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.