Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.PulsarPeriodFromRung

show as:
view Lean formalization →

The module defines median canonical recognition-rungs for normal and millisecond pulsars together with period functions derived from those rungs on the phi-ladder. Astrophysicists modeling pulsar timing populations in the Recognition Science framework would cite these definitions. It consists of a sequence of definitions and elementary lemmas establishing positivity, geometric ratios, and inequalities for the derived quantities.

claimMedian canonical recognition-rung $r_{ m normal}$ for normal pulsars, millisecond median rung $r_{ m ms}$, recycling shift, and period $P(r)$ at rung $r$ obtained from the phi-ladder with time quantum $\tau_0$.

background

The module sits in the astrophysics domain and imports the fundamental RS time quantum $\tau_0 = 1$ tick from Constants together with the Cost module. It introduces the phi-ladder rung assignments for pulsar classes, extending the mass formula yardstick $\times \phi^{{\rm rung}-8+{\rm gap}(Z)}$ to periods via the same self-similar structure. The local setting uses the Recognition Composition Law and the eight-tick octave to fix the discrete rung values that label observable timing properties.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the rung-to-period map that links the T5 J-uniqueness, T6 phi fixed point, and T7 eight-tick octave of the UnifiedForcingChain to concrete astrophysical observables. It provides the base layer for any later application of the Recognition Composition Law to pulsar populations, even though no downstream used_by edges are recorded yet.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (19)