Pith. sign in
module module moderate

IndisputableMonolith.Astrophysics.PulsarEmissionRegimesFromRS

show as:
view Lean formalization →

This module defines types and functions for classifying pulsar emission regimes in the Recognition Science framework. It introduces an inductive regime type, period and ratio functions, a count, and an emission certificate type, all built on the imported RS time quantum. Astrophysicists modeling periodic sources with RS constants would cite these objects. The module consists solely of definitions with no theorems.

claimInductive type for pulsar emission regimes, count of regimes, period function from regimes to positive integers, period ratio and position functions, and certificate type for emission validity.

background

The module sits in the astrophysics domain and imports IndisputableMonolith.Constants, whose sole documented content is the fundamental RS time quantum τ₀ = 1 tick. All objects are expressed in RS-native units (c = 1, ħ = φ^{-5}). The local setting applies the phi-ladder and eight-tick octave to periodic astrophysical phenomena without introducing new constants or extending the forcing chain.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

This module supplies the basic objects needed to apply Recognition Science to pulsar emission. It would feed parent theorems on specific emission properties or observational comparisons, though no used_by links exist yet. It touches the T7 eight-tick octave landmark by classifying periodic regimes.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)