gapCost_mono
plain-language theorem explainer
Gap cost monotonicity asserts that for natural numbers j ≤ k with j positive the J-cost of a gap of size j is at most that of size k on the φ-ladder. Researchers formalizing Rogers-Ramanujan identities or Zeckendorf representations cite the result to justify the minimal separation rule. The short term proof reduces the claim by simplification to the known monotonicity of J-cost on [1, ∞) together with the monotonicity of powers of φ.
Claim. For natural numbers $j ≤ k$ with $j > 0$, gapCost$(j) ≤$ gapCost$(k)$, where gapCost$(n) := J(φ^n)$ and $J(x) = (x + x^{-1})/2 - 1$.
background
The φ-ladder places positions at successive powers φ^n. The J-cost of a ratio x is J(x) = (x + x^{-1})/2 - 1, which quantifies defect or interaction energy. gapCost(n) is therefore the J-cost of the ratio φ^n that corresponds to a gap of n rungs. The module derives the classical Rogers-Ramanujan “differ by ≥ 2” rule as the unique J-cost admissible constraint on this ladder, because adjacent occupation (gap 1) yields positive cost while gap 2 is the minimal non-trivial stable configuration.
proof idea
Simplification unfolds the definition of gapCost. The proof obtains the bound 1 ≤ φ^j from phi_pow_ge_one and the comparison φ^j ≤ φ^k from phi_pow_mono. It then applies the lemma Jcost_mono_on_one to these bounds to obtain the desired inequality.
why it matters
The result supports the Rogers-Ramanujan Stability Theorem stated later in the same module by confirming that gap costs are non-decreasing, which selects non-adjacent partitions as minimal-cost configurations. It rests on J-uniqueness (T5) and the self-similar fixed point φ (T6) from the forcing chain, together with the Recognition Composition Law. No downstream uses are recorded yet, but the monotonicity closes a required step in translating Zeckendorf uniqueness into RS-native language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.