accretionDiskCert
plain-language theorem explainer
The accretionDiskCert definition supplies a concrete certificate asserting exactly five accretion regimes around compact objects together with a canonical transition threshold. Astrophysicists applying Recognition Science to super-Eddington flows would cite it when linking the J-cost function to the slim-disk to photon-trapping boundary. It is assembled as a one-line structure instantiation that pulls the regime count from a decidable theorem and the threshold from an imported cert.
Claim. A certificate for accretion disks exists such that the cardinality of the set of accretion regimes equals 5 and the transition threshold satisfies the canonical property.
background
The Astrophysics.AccretionDiskFromJCost module formalizes accretion-disk behavior derived from the J-cost function in Recognition Science. The structure AccretionDiskCert requires two fields: the cardinality of AccretionRegime equals 5, and the transition threshold belongs to CanonicalCert. The upstream theorem accretionRegimeCount establishes the cardinality by a decision procedure. The module documentation states that the slim-disk-to-photon-trapping transition occurs when the mass accretion rate ratio crosses J(φ) in (0.11, 0.13), with the five regimes corresponding to configDim D = 5.
proof idea
The definition is a one-line wrapper that sets the five_regimes field to the result of accretionRegimeCount and the transition_threshold field to cert. It depends on the decidable proof of the regime count and the CanonicalCert supplied by the CanonicalJBand import.
why it matters
This definition closes the Lean formalization of the B12 astrophysical MHD model with zero sorry. It supplies the concrete certificate required to embed the J-cost prediction for the transition threshold into the Recognition Science framework. The construction directly realizes the five-regime count that the module equates with configDim D = 5 and thereby connects to the broader forcing chain and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.