gap_size_eq
plain-language theorem explainer
Gap size equals seven on the recognition-cost ladder separating pulsar families. Astrophysicists modeling bimodal period distributions cite this result when deriving the structural gap from the eight-tick recycling shift. The proof reduces the definition directly via unfolding and numeric normalization.
Claim. The structural rung gap between the normal and millisecond pulsar families on the recognition-cost ladder equals 7.
background
In the Recognition Science treatment of pulsar periods, neutron-star spin periods are quantized to rungs of the recognition-cost ladder. The normal pulsar family occupies rungs around a median of 4, while the millisecond family is shifted by the recycling rung shift of 8 ticks. The gap size is defined as recycling rung shift minus 1, representing the number of unstable rungs in the millisecond family (rungs 1 through 7).
proof idea
The proof is a one-line wrapper that unfolds the definitions of gap size as recycling rung shift minus one and recycling rung shift as 8, then applies norm_num to evaluate the subtraction to 7.
why it matters
This equality closes the definition of the rung gap and feeds gap size positivity as well as the master certificate PulsarPeriodFromRungCert. It supports the one-statement theorem on the bimodal pulsar period distribution forced by the 8-tick shift, consistent with the eight-tick octave in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.