J_at_one
plain-language theorem explainer
The recognition cost J satisfies J(1) = 0. Derivations of baseline masses from cube geometry and canonical cost systems cite this normalization. The proof is a direct unfolding of the J definition followed by numerical simplification.
Claim. $J(1) = 0$, where $J(x) = (1/2)(x + x^{-1}) - 1$ is the recognition cost functional.
background
The recognition cost functional is defined by $J(x) = (1/2)(x + x^{-1}) - 1$ for $x > 0$. This module upgrades prior boundary assumptions to derived status by applying standard combinatorics of the 3-cube $Q_3$ at $D = 3$, yielding items such as non-triviality (B-20) from the fact that $J(1) = 0$ implies the identity is unobservable. Upstream results include the algebraic normalization of J established in CostAlgebra.
proof idea
This is a one-line wrapper that unfolds the definition of J and applies norm_num to verify the equality.
why it matters
This supplies the normalization required by canonicalCostAlgebra in CostAlgebra, which packages J together with the recognition composition law, reciprocal symmetry, and non-negativity to form the canonical cost system. It fills the B-20 non-triviality slot in the baseline rung derivations from cube geometry. The result aligns with J-uniqueness (T5) in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.