recycling_rung_shift
plain-language theorem explainer
This definition sets the recycling rung shift to the integer 8, marking the canonical separation between normal and millisecond pulsar families on the phi-ladder. Researchers constructing the bimodal period distribution cite it to obtain the median ratio phi to the eighth. The declaration is introduced as a direct numerical assignment with no reduction steps.
Claim. The recycling rung shift is the natural number 8.
background
The module assigns neutron-star periods to integer rungs of the recognition-cost phi-ladder. Normal pulsars occupy rungs k_normal in {0, ..., 8} with base time tau_neutron, while millisecond pulsars use a recycled base time tau_recycled equal to tau_neutron divided by phi to the eighth. The module states that the 8-rung shift comes from the recycling mechanism (accretion from a binary companion adds 8 ticks of angular momentum on average), which is exactly the canonical 8-tick window from Patterns.eight_tick_min.
proof idea
The declaration is a direct definition that binds the constant value 8.
why it matters
It supplies the fixed exponent for the bimodal ratio definition, which supports the theorems establishing that the ratio exceeds 30 and lies below phi to the ninth. The module presents the shift as the structural basis for the predicted median period ratio phi^8, aligning with the eight-tick octave in the forcing chain. It closes the rung-gap explanation for the observed absence of pulsars between 30 and 100 ms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.