pulsarRegime_count
plain-language theorem explainer
The declaration asserts that the inductive type for pulsar emission regimes contains exactly five elements. Astrophysicists using the Recognition Science model for pulsar classification would cite this cardinality when certifying emission properties. The proof is a one-line decision procedure that counts the five constructors of the PulsarRegime inductive type.
Claim. The finite set of canonical pulsar emission regimes has cardinality five, consisting of the normal pulsar, millisecond pulsar, magnetar, rotating radio transient, and fast radio burst source.
background
The module encodes five canonical pulsar emission regimes as the constructors of the inductive type PulsarRegime: normal, millisecond, magnetar, rrat, and frbSource. This type derives DecidableEq, Repr, BEq, and Fintype instances. The local theoretical setting identifies these regimes with configDim D = 5 and states that adjacent-regime period ratios equal phi on the phi-ladder.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the inductive type PulsarRegime, whose five constructors are enumerated by the derived Fintype instance.
why it matters
This cardinality supplies the five_regimes field inside the PulsarEmissionCert definition, which certifies the full set of emission properties. It directly implements the module claim of five regimes corresponding to configDim D = 5 and the phi-ladder scaling. The result leaves open the derivation of the specific regime list from the Recognition Composition Law rather than direct enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.