pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS

show as:
view Lean formalization →

This module defines pulsar emission regimes derived from Recognition Science, including the regime type, count, period functions, and emission certificates based on RS time quanta. Astrophysicists modeling compact object signals with RS constants would cite these objects. It consists entirely of definitions and supporting functions with no embedded proofs.

claimDefines the type $PulsarRegime$ of emission regimes, the count $pulsarRegime_count$, the functions $period$, $period_ratio$, $period_pos$ for timing, and the certificate structure $PulsarEmissionCert$ with constructor $pulsarEmissionCert$, all relative to the RS time quantum.

background

Recognition Science derives physics from a single functional equation whose forcing chain yields the phi self-similar fixed point and three spatial dimensions. This module imports the fundamental RS time quantum from Constants, where the native time unit satisfies τ₀ = 1 tick. It introduces sibling definitions that classify pulsar emission modes, compute periods and ratios on the phi-ladder, and certify validated regimes.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the core objects needed to apply Recognition Science to pulsar astrophysics and feeds into larger results on emission properties derived from the phi-ladder and Recognition Composition Law. It bridges the abstract T0-T8 chain to concrete observables without yet linking to any downstream theorems in the dependency graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)