gap_size
plain-language theorem explainer
The gap_size definition encodes the structural separation of seven rungs between normal and millisecond pulsar families on the phi-ladder. Astrophysicists modeling the observed bimodal period distribution would cite this constant to explain the absence of pulsars in the 30-100 ms interval. It is obtained by direct subtraction of one from the fixed recycling rung shift of eight.
Claim. Define the structural rung gap by $g := s - 1$, where $s$ is the canonical recycling rung shift of eight between the normal and millisecond pulsar families on the recognition-cost ladder.
background
In the Recognition Science treatment of pulsar periods, neutron-star spins are forced to integer rungs of the phi-ladder. Normal pulsars occupy rungs $k$ with period $P = tau_neutron · phi^k$ for $k$ near 4; millisecond pulsars occupy a parallel family whose base period is shifted by the recycling mechanism. The upstream recycling_rung_shift is defined as the constant eight, the average angular-momentum addition from binary accretion that matches the eight-tick octave of the framework.
proof idea
One-line definition that subtracts one from the recycling_rung_shift constant.
why it matters
This definition supplies the numerical gap size used by gap_size_eq, gap_size_pos, PulsarPeriodFromRungCert and pulsar_period_one_statement. It quantifies the unstable rungs 1-7 in the ms family, closing the structural account of bimodality forced by the eight-tick recycling shift that aligns with the eight-tick octave and T7 of the Recognition chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.