adjacent_Jcost_eq
plain-language theorem explainer
Adjacent phi-ladder occupations incur J-cost exactly equal to (phi plus phi inverse over 2) minus 1. Partition theorists and Recognition Science modelers cite this to ground the positive-cost instability that enforces the differ-by-at-least-2 rule. The proof is a one-line wrapper that unfolds the Jcost definition and normalizes the resulting algebraic expression.
Claim. $J(phi) = (phi + phi^{-1})/2 - 1$, where $J$ is the J-cost function on positive real ratios.
background
The phi-ladder consists of positions phi^n for integer n, with interaction costs governed by the J-cost function. Upstream definitions establish that cost for a multiplicative recognizer is the derived cost of its comparator, while the cost of a recognition event is Jcost of its state. The module sets the local setting by showing that adjacent rungs at ratio phi produce positive J-cost, which collapses under the golden recurrence and drives the non-adjacent occupation rule in Rogers-Ramanujan partitions.
proof idea
The proof unfolds the definition of Jcost and applies the ring tactic to normalize the algebraic expression to the target form.
why it matters
This identity supplies the explicit positive value of J(phi) that the module uses to explain why consecutive occupations are unstable on the phi-ladder. It directly supports the J-cost argument linking the Rogers-Ramanujan differ-by-at-least-2 constraint to Zeckendorf representations and the broader Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.