gap_size_pos
plain-language theorem explainer
The structural gap of unstable rungs between normal and millisecond pulsar families on the recognition-cost ladder is strictly positive. Astrophysicists deriving the bimodal pulsar-period distribution from the phi-ladder would cite this to confirm the separation of the two populations. The proof is a one-line wrapper that rewrites via the gap-size equality and applies numerical normalization.
Claim. The structural rung gap between the normal and millisecond pulsar families satisfies $0 < 7$.
background
In the Recognition Science model of pulsar periods, neutron-star spins occupy discrete rungs of the phi-ladder. Normal pulsars sit at median rung 4 while millisecond pulsars are displaced by the canonical 8-tick recycling shift, leaving a gap of unstable intermediate rungs. The gap size is defined as the recycling rung shift minus one, which the equality theorem fixes at exactly 7. Upstream results establish that the bimodal ratio is positive, exceeds 30, and lies below phi^9, all derived from the same 8-tick shift and phi-arithmetic.
proof idea
One-line wrapper that rewrites the goal using the gap-size equality theorem and then applies norm_num to confirm that 7 is positive.
why it matters
This result supplies the final positivity clause in the eight-part master certificate for the pulsar-period bimodal distribution (Track AS7). It directly implements the eight-tick octave (T7) and the structural gap of 7 rungs that produces the observed 30-100 ms period desert. The theorem rests on the phi-ladder mass formula and the recycling shift already fixed by Constants.phi and Patterns.eight_tick_min; no open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.