normal_median_rung
plain-language theorem explainer
The declaration sets the median canonical recognition-rung for normal pulsars to the integer 4. Researchers deriving the bimodal pulsar-period distribution from the phi-ladder in Recognition Science would cite this constant when stating the normal family median. It is supplied as a direct definition with no further reduction.
Claim. The median canonical recognition-rung for normal pulsars is the natural number $4$.
background
Pulsar periods are modeled as geometric sequences on the phi-ladder: the period function returns phi raised to the rung index. Normal pulsars occupy one family of rungs with base period tau_neutron; millisecond pulsars occupy a second family shifted by the recycling mechanism. The module doc states that the median for the normal family sits at rung 4, producing a predicted period near 0.7 s in RS-native units. Upstream results supply the period definition as phi^k and multiple independent rung constants in arithmetic and engineering contexts.
proof idea
One-line definition that directly assigns the natural number 4.
why it matters
This supplies the normal-median value required by PulsarPeriodFromRungCert and pulsar_period_one_statement. It completes the structural claim for Track AS7: normal pulsars at median rung 4, millisecond pulsars also at median rung 4, with the 8-tick recycling shift producing the bimodal ratio phi^8. The placement ties directly to the eight-tick octave landmark and the phi-ladder mass/period formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.