reconnectionRegimeCount
plain-language theorem explainer
Recognition Science fixes the number of magnetic reconnection regimes at five in its astrophysical MHD model. Researchers modeling solar flares or plasma instabilities would reference this enumeration to classify reconnection events. The proof is a direct decision procedure that counts the constructors of the regime enumeration.
Claim. The cardinality of the set of canonical reconnection regimes is five: $|$slow, Sweet-Parker, Petschek, Hall-mediated, turbulent$| = 5$.
background
In the module on magnetic reconnection from J-cost, Recognition Science models reconnection as triggered when the magnetic-flux recognition ratio enters the canonical J-band, with rates following phi-ladder decay. The five regimes are slow, Sweet-Parker, Petschek, Hall-mediated, and turbulent, set equal to a configuration dimension of five. This rests on the inductive definition of the regimes together with the derived Fintype instance.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the cardinality equality. It succeeds immediately because the inductive type derives DecidableEq, BEq, and Fintype from its five constructors.
why it matters
This result supplies the five_regimes field inside the magnetic reconnection certificate definition. It realizes the framework claim that the number of reconnection regimes equals the configuration dimension of five, closing the enumeration step in the astrophysical MHD section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.