identity_Jcost_zero
plain-language theorem explainer
Identity ratio carries zero J-cost, anchoring the ground state for admissible phi-ladder configurations in Recognition Science. Partition theorists and modelers of Rogers-Ramanujan identities cite it when deriving the differ-by-at-least-two rule from positivity of interaction costs. The argument reduces directly to the unit-cost lemma in the Cost module.
Claim. $J(1) = 0$, where $J(x) = (x + x^{-1})/2 - 1$ denotes the cost of a positive ratio $x$ and the identity ratio is the unique minimum on the positive reals.
background
The J-cost function is defined on positive reals by $J(x) = (x + x^{-1})/2 - 1$, equivalently $(x-1)^2/(2x)$, and measures the interaction energy of a ratio on the phi-ladder. It is induced by the multiplicative recognizer comparator and appears as the cost of any recognition event. The phi-ladder positions are powers of phi, with adjacent occupations unstable because the golden recurrence collapses them into a single higher rung while incurring positive J-cost. This module derives the Rogers-Ramanujan differ-by-at-least-two rule as the unique J-cost admissible constraint. The result relies on the upstream unit lemma Jcost_unit0, which states Jcost 1 = 0 by direct simplification of the definition.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module (and its duplicate in JcostCore). No further tactics are required; the term simply invokes the already-proved unit identity.
why it matters
This identity supplies the zero baseline required for the J-cost admissibility argument that converts the classical Rogers-Ramanujan partition rule into a forced minimum on the phi-ladder. It sits inside the T5 J-uniqueness step of the forcing chain and directly enables the adjacent_Jcost_positive and gapCost siblings. No open scaffolding remains; the result is fully discharged by the Cost core.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.