module module moderate

`IndisputableMonolith.Astrophysics.PulsarPeriodFromRung`

This module defines the median canonical recognition-rung for normal pulsars together with associated period expressions derived from the phi-ladder. Astrophysicists applying Recognition Science to timing observations would cite these relations to connect periods to rung structure. The module consists of definitions and elementary properties built on the imported Constants and Cost modules.

claimLet $r_{\text{normal}}$ denote the median canonical recognition-rung for normal pulsars. The period at rung $r$ is given by $P(r) = \tau_0 \cdot \phi^{r}$ (with $\tau_0 = 1$ tick) and satisfies the geometric scaling $P(r+1)/P(r) = \phi$.

background

The module sits in the astrophysics domain and imports the fundamental RS time quantum $\tau_0 = 1$ tick from Constants together with the J-cost machinery from Cost. It introduces sibling objects normal_median_rung, ms_median_rung, recycling_rung_shift, period_at_rung, period_geometric and bimodal_ratio that encode the rung-to-period map for pulsars. These rest on the Recognition Composition Law and the phi-ladder already established in the upstream modules.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the rung and period definitions that support pulsar timing applications inside the Recognition framework. It directly implements the T7 eight-tick octave and phi-ladder scaling for astrophysical objects, feeding the mass formula and Berry creation threshold into concrete predictions. No downstream theorems are recorded yet.

scope and limits

Does not incorporate measured pulsar periods or observational catalogs.
Does not derive the median rung from first principles; it states it as a definition.
Does not treat relativistic or binary corrections to the period formula.
Does not address the transition between normal and millisecond pulsar regimes beyond the listed siblings.

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