ms_median_rung
plain-language theorem explainer
Defines the median canonical recognition rung for millisecond pulsars as the natural number 4. Astrophysicists deriving the bimodal pulsar-period distribution from the phi-ladder cite this constant to fix the shared rung index while applying the eight-tick base-period shift. The declaration is a direct constant assignment with no computation or lemmas.
Claim. The median canonical recognition rung for millisecond pulsars is the natural number $4$.
background
Recognition Science places neutron-star spin periods on the phi-ladder with the fundamental tick as the RS-native time quantum. Normal pulsars use base period tau_neutron times phi to the power k for integer rungs k, while millisecond pulsars employ a recycled base shifted by the canonical eight-tick window. The module treats both families as sharing the same median rung index but differing in base period by exactly that octave shift from the Beat structure. Upstream results supply the canonical arithmetic object for the integer indices and the non-parasitic schedule that keeps rung assignments consistent with the forcing chain.
proof idea
Direct constant definition that assigns the value 4. No lemmas or tactics are applied; the assignment is primitive and serves as the target for the reflexivity proof of the downstream equality theorem.
why it matters
Supplies the millisecond median rung index to the PulsarPeriodFromRungCert structure and the one-statement theorem pulsar_period_one_statement. It encodes the structural claim that both pulsar families share rung 4 while the eight-tick recycling shift produces the phi^8 bimodal ratio, aligning with the T7 octave in the unified forcing chain. The definition closes the rung-index part of the Track AS7 structural theorem without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.