J_at_one
plain-language theorem explainer
The lemma establishes that the Recognition cost function J vanishes at the multiplicative identity. Researchers constructing canonical cost algebras cite this normalization when verifying the full set of axioms for J. The proof is a direct one-line wrapper that unfolds the definition of J and applies numerical simplification.
Claim. $J(1) = 0$, where $J(x) := (1/2)(x + x^{-1}) - 1$ for $x > 0$.
background
J is the fundamental cost function defined by $J(x) = (1/2)(x + x^{-1}) - 1$. This is the unique cost satisfying d'Alembert's equation plus normalization and calibration (T5 J-uniqueness). The Modal.Possibility module uses this lemma to record the zero-cost property of the identity configuration. Upstream results in CostAlgebra and BaselineDerivation establish the identical normalization, confirming the property holds uniformly across the framework.
proof idea
This is a one-line wrapper that unfolds the definition of J and applies norm_num to simplify the resulting arithmetic expression to zero.
why it matters
This normalization feeds directly into canonicalCostAlgebra, which packages J together with RCL, reciprocal symmetry, and non-negativity. It appears in cost_algebra_certificate and canonicalRecognitionCostSystem_cost_one, and supports derivations in BaselineDerivation and HiggsMechanism. The result corresponds to the T5 normalization step in the forcing chain, ensuring the identity carries zero cost in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.