AccretionRegime
plain-language theorem explainer
AccretionRegime enumerates the five accretion flow states around compact objects under the Recognition Science J-cost model. High-energy astrophysicists would cite the type when enforcing configuration dimension five for disk regime transitions. The definition proceeds by direct inductive enumeration of the five cases followed by automatic derivation of Fintype.
Claim. The accretion regimes form the finite type consisting of the five states sub-Eddington thin disk, thick disk, slim disk, photon-trapped disk, and super-critical disk.
background
Accretion disks around black holes and neutron stars transition between regimes as the mass accretion rate crosses the Eddington limit. The module imports CanonicalJBand to supply the J-cost function and its certification. The local theoretical setting states that these five regimes realize configuration dimension five, with the slim-to-photon-trapped transition predicted to occur when the accretion rate ratio crosses J(φ) in the interval (0.11, 0.13).
proof idea
The declaration is an inductive definition that directly introduces the five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances automatically.
why it matters
The definition supplies the finite set required by the downstream AccretionDiskCert structure, which asserts both Fintype.cardinality equal to five and satisfaction of CanonicalCert for the transition threshold. It realizes the astrophysical application of the J-cost framework, linking the abstract forcing chain to observable accretion phenomenology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.