rcl_normalised
plain-language theorem explainer
The normalisation axiom asserts that the cost function J satisfies J(1) = 0. Researchers deriving the Recognition Composition Law would cite this as the first of three axioms that, with continuity, force uniqueness of J. The proof is a direct one-line application of the upstream lemma establishing the explicit squared-ratio form of J.
Claim. Let $J(x) = (x-1)^2/(2x)$ for $x > 0$. Then $J(1) = 0$.
background
The Recognition Composition Law (RCL) is the functional equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. This module certifies the three axioms (normalisation, reciprocal symmetry, positivity) that make J the unique solution. The local setting is the structural backing for uniqueness, with zero sorry or axiom in Lean. J is expressed as the squared ratio $J(x) = (x-1)^2/(2x)$, which is equivalent to $(x + x^{-1})/2 - 1$. The upstream lemma Jcost_unit0 establishes the normalisation by direct simplification from this definition.
proof idea
This is a one-line wrapper that applies the lemma Jcost_unit0. That lemma itself follows by simp on the definition of Jcost as the squared ratio.
why it matters
This supplies the normalisation component assembled into the uniqueness axioms theorem and packaged in the RCL certificate definition. It underpins the claim that J is the unique cost function satisfying the RCL, linking directly to J-uniqueness (T5) in the forcing chain. The result is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.