accretionRegimeCount
plain-language theorem explainer
The declaration proves that the set of accretion regimes around compact objects has cardinality exactly five. Astrophysicists modeling sub-Eddington to super-Eddington transitions in black hole and neutron star disks cite this count when anchoring the J-cost threshold near 0.12. The proof is a one-line decision tactic that enumerates the five inductive cases and confirms the finite cardinality.
Claim. The set of accretion regimes has cardinality five, consisting of the sub-Eddington thin disk, the thick disk, the slim disk, the photon-trapped regime, and the super-critical regime.
background
The module models accretion disks around compact objects using the J-cost function from Recognition Science. Accretion regimes are introduced as an inductive type with five constructors that label the distinct flow phases: sub-Eddington thin, thick, slim, photon-trapped, and super-critical. The local setting is the B12 astrophysical MHD framework, where the slim-disk to photon-trapping transition occurs when the mass accretion rate ratio crosses J(φ) in (0.11, 0.13) and the regime count equals the configuration dimension of 5.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the cardinality statement. This succeeds because the inductive definition automatically generates DecidableEq and Fintype instances, allowing the decision procedure to count the five constructors directly.
why it matters
This result supplies the five_regimes field inside the accretionDiskCert definition that certifies the full regime structure together with the transition threshold. It realizes the Recognition Science prediction that five regimes arise from the J-cost structure in accretion flows, consistent with the forcing chain and the eight-tick octave. The count closes the astrophysical application without remaining open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.