PulsarPeriodFromRungCert
plain-language theorem explainer
PulsarPeriodFromRungCert is the record that packages the eight canonical properties of the pulsar-period ladder: median rungs at 4 for both families, an 8-tick recycling shift, exact geometric progression by phi, and tight bounds on the bimodal ratio together with a gap of 7 rungs. Modelers comparing Recognition Science to ATNF catalog data would cite this certificate when testing the predicted 47-fold separation against observed bimodality. The definition is a plain structure whose fields are filled by reflexivity on the rung constants and by
Claim. A certificate asserting that the normal-pulsar median rung is 4, the millisecond-pulsar median rung is 4, the recycling shift is 8, periods satisfy $P_{k+1}=P_k·φ$ for integer rungs, the ratio $r$ of the two medians obeys $0<r<φ^9$ and $r>30$, and the structural gap between families is 7 rungs.
background
The module treats neutron-star spin periods as forced to integer rungs of the recognition-cost ladder. Normal pulsars occupy rungs $k_normal$ with periods $τ_neutron·φ^{k_normal}$ and median at rung 4; millisecond pulsars occupy a shifted family with $τ_recycled≈τ_neutron/φ^8$ and the same median rung. The eight-tick shift is taken from the canonical recycling window. Upstream definitions supply the ratio $r=φ^8$ (bimodal_ratio) and the gap size $recycling_rung_shift-1$ (gap_size). The module doc states the structural prediction $P_median(normal)/P_median(ms)=φ^8≈47$ and notes the empirical gap at 30–100 ms.
proof idea
This is a structure definition. Its eight fields are discharged by reflexivity on the three rung and shift constants, by the already-proved geometric-progression lemma for the period relation, and by the three ratio theorems (positivity, >30, <φ^9) together with the gap-size equality proved earlier in the same file.
why it matters
The certificate is the master object inhabited by pulsarPeriodFromRungCert, thereby closing Track AS7. It encodes the phi-ladder explanation for the observed 47-fold separation between normal and millisecond populations and the 7-rung gap, directly implementing the eight-tick octave (T7) and D=3 spatial forcing from the UnifiedForcingChain. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.