period_at_rung
plain-language theorem explainer
The definition assigns the pulsar period at recognition rung k to the base period scaled by phi to the power k. Researchers deriving the bimodal neutron-star spin distribution from the phi-ladder would cite this scaling when computing median periods for normal and recycled populations. It is introduced as a direct definition that unfolds immediately to the arithmetic expression without lemmas or tactics.
Claim. The period at rung $k$ is $P_0 · ϕ^k$, where $P_0$ is the base recognition time for the given pulsar family and $ϕ$ is the golden-ratio fixed point of the forcing chain.
background
In the Recognition Science setting, neutron-star periods are forced onto integer rungs of the phi-ladder. Normal pulsars use base time $τ_neutron$ at rungs $k ∈ {0,…,8}$ with median at rung 4; millisecond pulsars use a recycled base shifted by exactly eight ticks, the canonical octave length. The supplied module_doc states that this produces the observed bimodality with median ratio $ϕ^8 ≈ 47$ and a gap at 30–100 ms. The definition period_at_rung supplies the explicit scaling law used by all subsequent statements in the file.
proof idea
Direct definition that expands to the product $P_base · phi ^ k$. No lemmas are invoked and no tactics are required; the expression is the primitive rung-scaling operation for the module.
why it matters
This supplies the core scaling relation inside the PulsarPeriodFromRungCert structure, which records the normal median rung = 4, millisecond median rung = 4, recycling shift = 8, and the geometric progression property. It realizes the structural prediction of the eight-tick octave (T7) for the bimodal distribution and feeds the positivity and geometric lemmas that close the AS7 track. The definition therefore anchors the claim that pulsar periods are discrete phi-ladder states rather than continuous.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.