cost_of_the_first_distinction
plain-language theorem explainer
The recognition cost of the ratio 2 equals one quarter: J(2)=1/4. Anyone fixing the absolute scale of the RS cost functional after uniqueness and input-scale minimality cites this evaluation. The proof is a one-step numerical unfolding of the closed form of J.
Claim. With the recognition cost $J(x)=(x+x^{-1})/2-1$ for $x>0$, one has $J(2)=1/4$.
background
The recognition cost is the unique functional forced by the Recognition Composition Law (RCL): $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Its closed form is $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$, which is the T5 landmark (J-uniqueness) in the forcing chain.
The module Cost.UnitFromMinimality treats the remaining gauge freedom after RCL has fixed the output scale. Rescaling $J$ breaks the composition law, so only the input scale was free; minimality among discrete powers then selects the unit. Against that background the concrete value at the first nontrivial integer ratio becomes a derived number rather than a convention.
Upstream definitions of $J$ (Cost, CoherenceCollapse, EnergyProcessingBridge) all use the same formula; the present theorem simply evaluates it at 2.
proof idea
One-line tactic proof: unfold the definition of $J$ and reduce the rational arithmetic by norm_num. Explicitly, $(2+2^{-1})/2-1=(5/2)/2-1=5/4-1=1/4$. No lemmas beyond the definition are required.
why it matters
This pins the absolute cost of the elementary distinction "one versus two" once composition-law uniqueness and input-scale minimality are in place. Downstream it is consumed by discrete_gauge_has_a_floor_and_continuous_gauge_does_not, which contrasts the discrete carrier (strict least cost among odd powers) with the continuum (halving the exponent always undercuts). The doc-comment states the conceptual payoff: the number is now determined rather than stipulated. In the broader framework it sits under T5 (J-uniqueness) and the RCL, giving a concrete calibration point before ladder and mass formulae are built.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.