adjacent_absorptive
plain-language theorem explainer
Adjacent rungs on the phi-ladder are absorptive: for any integer index n the sum of positions at n and n+1 equals the position at some higher index m. Partition theorists linking Rogers-Ramanujan identities to J-cost constraints would cite this to justify the differ-by-at-least-2 rule. The proof is a one-line wrapper that invokes the adjacent collapses identity to witness m = n + 2.
Claim. For every integer $n$, there exists an integer $m$ such that $P(n) + P(n+1) = P(m)$, where $P(k) = phi^k$ is the position of rung $k$ on the golden-ratio ladder.
background
Positions on the phi-ladder are the discrete set $phi^k$ for $k in Z$, with the golden ratio satisfying the recurrence $phi^{k+2} = phi^{k+1} + phi^k$. J-cost is defined as $J(x) = (x + x^{-1})/2 - 1$ and is positive for the ratio $phi$, marking adjacent occupations as unstable. Upstream results from ObserverForcing and MultiplicativeRecognizerL4 establish that recognition-event cost equals this J-cost, while LedgerFactorization calibrates the underlying multiplicative structure.
proof idea
The proof is a one-line wrapper that applies the adjacent_collapses lemma to supply the explicit witness m = n + 2.
why it matters
This supplies the absorption step inside the Rogers-Ramanujan stability theorem, which equates the classical differ-by-at-least-2 partition rule with J-cost admissibility on the phi-ladder. It fills the gap=1 case in the stability classification, confirming collapse via the golden recurrence and positive J-cost. The result anchors the phi-ladder construction that descends from the self-similar fixed point phi in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.