ground_state_is_identity
plain-language theorem explainer
The ground state on the φ-ladder has vanishing J-cost at x=1. Researchers modeling minimal-energy configurations for the Rogers-Ramanujan constraint in Recognition Science cite this as the zero-interaction reference point. The proof is a direct one-line application of the unit lemma for J-cost.
Claim. $J(1)=0$, where $J(x)=((x-1)^2)/(2x)$ is the J-cost on the φ-ladder.
background
The φ-ladder places states at positions φ^n for n∈ℤ. J-cost measures the interaction energy of a ratio x, with the explicit form J(x)=(x-1)^2/(2x) supplied by the upstream lemma Jcost_unit0. The module on φ-Ladder Stability shows that adjacent rungs collapse under the golden recurrence φ^2=φ+1, so the minimal non-trivial stable occupation requires a gap of at least 2; the identity event at x=1 supplies the zero-cost base case for this constraint.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_unit0 from the Cost module, which reduces Jcost 1 to zero by direct simplification of the squared-ratio definition.
why it matters
This supplies the zero-cost ground state required for the J-cost admissibility constraint that enforces the 'differ by ≥2' rule on the φ-ladder. It anchors the module's derivation of Rogers-Ramanujan stability from the Recognition Composition Law and the T5 J-uniqueness step. The result closes the base case before higher-rung arguments such as adjacent_Jcost_positive and gapCost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.