gap0_cost_zero
plain-language theorem explainer
The J-cost of a zero gap on the φ-ladder is identically zero, confirming that identical rung occupation carries no interaction penalty. Partition theorists and Recognition Science researchers cite this as the trivial base case when analyzing admissible configurations under the J-cost constraint. The proof is a direct one-line simplification that invokes the unit lemma for the J-cost function.
Claim. The interaction cost for occupying the same rung (gap of size zero) on the φ-ladder is zero: $gapCost(0) = 0$, where $gapCost$ measures the J-interaction cost between rungs separated by the given integer gap.
background
The φ-ladder places positions at integer powers of the golden ratio φ, with stability determined by the J-cost function J(x) = (x-1)^2/(2x). This cost vanishes exactly at x=1, corresponding to identical positions. The module develops why Rogers-Ramanujan partitions require consecutive parts to differ by at least 2: adjacent occupations (gap 1) incur positive J-cost and collapse via the recurrence φ^2 = φ + 1. Upstream, the lemma Jcost_unit0 states that Jcost 1 = 0, supplying the algebraic identity needed for the zero-gap case.
proof idea
This is a one-line term proof that applies simplification to the definition of gapCost together with the lemma Jcost_unit0 asserting Jcost 1 = 0.
why it matters
This supplies the trivial base case inside the Rogers-Ramanujan stability theorem, which states that gap-0 is trivial, gap-1 is unstable (positive J-cost plus absorption), and gap ≥2 is stable. It anchors the J-cost admissibility constraint that forces the classical “differ by ≥2” rule, linking directly to J-uniqueness in the forcing chain and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.