PhiLadderAdmissible
plain-language theorem explainer
A list of integers is admissible on the φ-ladder when every pair differs by at least 2 in absolute value. Partition theorists linking Rogers-Ramanujan identities to Recognition Science would cite this as the J-cost stability filter on rung occupations. The definition encodes the separation condition directly via the pairwise predicate on the input list.
Claim. A list of integers $(p_i)$ is admissible on the φ-ladder if $|p_i - p_j| ≥ 2$ for all distinct indices $i,j$.
background
The module establishes why the classical Rogers-Ramanujan condition of consecutive parts differing by at least 2 arises naturally from Recognition Science. Positions on the φ-ladder are powers φ^n for integer n. Adjacent rungs (ratio φ) produce positive J-cost J(φ) ≈ 0.118, violating minimality, while a gap of 2 yields the lowest stable non-trivial cost via the golden recurrence φ² = φ + 1. This matches Zeckendorf representations, where every positive integer is a unique sum of non-consecutive Fibonacci numbers, translated here as non-adjacent rung occupations.
proof idea
The definition is a direct one-line wrapper that applies the Pairwise predicate to the input list, enforcing the absolute-difference lower bound of 2 on every pair.
why it matters
This supplies the core admissibility filter for φ-ladder partitions in the RamanujanBridge module, making the Rogers-Ramanujan identities a direct consequence of J-cost minimality rather than an arbitrary rule. It sits downstream of the J-uniqueness and phi fixed-point steps in the forcing chain and supports later stability arguments that connect to the eight-tick octave. No downstream uses are recorded yet, leaving open how the filter integrates with mass formulas or gap derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.