gap2_cost_eq
plain-language theorem explainer
The theorem states that the interaction cost for a gap-2 occupation on the golden-ratio ladder equals the J-cost evaluated at phi squared. Researchers modeling partition identities or phi-ladder constraints in Recognition Science would cite this as the explicit minimum non-trivial stable cost. The proof is a direct reflexivity that unfolds the gapCost definition.
Claim. The cost of a gap-2 occupation on the phi-ladder equals $J(phi^2)$, where $J(x) = (x + x^{-1})/2 - 1$.
background
In the phi-ladder stability setting, rung positions are at powers of the golden ratio phi. Gap k means two occupied rungs separated by k steps, so the ratio is phi^k. The gapCost function is defined to return the J-cost of that ratio, and J-cost itself is the interaction measure J(x) = (x + x^{-1})/2 - 1. The module shows that gap 1 produces positive cost while gap 2 yields the minimum non-trivial value, enforcing the differ-by-at-least-2 rule that appears in the Rogers-Ramanujan identities and in Zeckendorf representations.
proof idea
The proof is a one-line reflexivity that applies the definition of gapCost, which sets gapCost k to the J-cost of phi^k.
why it matters
This pins the minimum non-trivial stable interaction cost on the phi-ladder, supplying the concrete J-cost value that justifies the gap >=2 constraint in the Rogers-Ramanujan identities. It supports the broader phi-ladder stability arguments that connect to Zeckendorf uniqueness and the J-uniqueness step in the forcing chain. The result sits inside the module that translates the classical partition rule into an admissibility condition forced by the J-cost structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.