recycling_rung_shift_eq
plain-language theorem explainer
The recycling rung shift equals 8, encoding the canonical 8-tick offset between normal and millisecond pulsar families on the phi-ladder. Modelers of the bimodal pulsar period distribution cite it to obtain the structural median ratio of phi to the eighth. The proof is a one-line reflexivity that matches the definition directly to the integer constant 8.
Claim. The canonical recycling rung shift between normal and millisecond pulsar families equals 8.
background
In the Recognition Science reading of pulsar data, neutron-star periods are assigned to rungs on the phi-ladder. Normal pulsars use base period tau_neutron at integer rungs k in 0 to 8; millisecond pulsars use the recycled base tau_neutron over phi to the eighth. The upstream definition states: 'The canonical 8-tick recycling shift between normal and millisecond families.' Period at rung k is defined as phi to the k. The module sets this inside the structural account of the observed bimodal distribution with its 30-100 ms gap.
proof idea
The proof is a one-line wrapper that applies reflexivity to equate the recycling rung shift definition to the integer 8.
why it matters
This equality supplies one clause of the Pulsar Period from Recognition-Rung Master Certificate, which assembles the structural predictions for bimodality. It encodes the 8-tick recycling shift that realizes the eight-tick octave landmark, enabling the phi^8 median ratio. The result supports gap_size_pos and closes part of Track AS7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.