module module moderate

`IndisputableMonolith.Astrophysics.PulsarPeriodFromRung`

The module defines the median canonical recognition-rung for normal pulsars together with period-at-rung functions and bimodal ratios. Astrophysicists applying Recognition Science to timing data would cite these when mapping rung numbers to observed periods. Content is organized as a sequence of definitions for rungs and periods followed by equality and positivity lemmas.

claimDefines the median recognition rung $r_N$ for normal pulsars, the period function $P(r)$ at rung $r$, the geometric period, and the bimodal ratio $R$ between normal and millisecond populations, all expressed in RS-native units with time quantum $τ_0$.

background

The module sits in the astrophysics domain and imports the fundamental RS time quantum $τ_0 = 1$ tick from Constants together with cost machinery from Cost. It introduces the phi-ladder scaling for periods, where rung number determines scale via the self-similar fixed point, and applies the recognition composition law to pulsar timing. Upstream Constants supplies the base time quantum while Cost supplies the underlying J-cost and defect measures used to assign rungs.

proof idea

This is a definition module. It introduces median rungs for normal and millisecond pulsars, a recycling shift, the period_at_rung function, geometric period, and bimodal ratio, then establishes basic properties through direct algebraic identities and positivity checks.

why it matters in Recognition Science

The module supplies the explicit pulsar-period formulas that connect rung numbers to observable timing in the Recognition Science framework. It fills the astrophysics application layer downstream of the forcing chain (T5 J-uniqueness through T8 D=3) and the eight-tick octave. No parent theorems are listed among used_by edges, indicating it functions as a terminal calculation module.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (19)

def normal_median_rung L97
def ms_median_rung L101
def recycling_rung_shift L105
theorem normal_median_rung_eq L107
theorem ms_median_rung_eq L108
theorem recycling_rung_shift_eq L109
def period_at_rung L119
theorem period_at_rung_pos L121
theorem period_geometric L127
def bimodal_ratio L137
theorem bimodal_ratio_pos L140
theorem bimodal_ratio_gt_thirty L146
theorem bimodal_ratio_lt_phi_nine L158
def gap_size L177
theorem gap_size_eq L179
theorem gap_size_pos L183
structure PulsarPeriodFromRungCert L205
def pulsarPeriodFromRungCert L218
theorem pulsar_period_one_statement L241