AccretionDiskCert
plain-language theorem explainer
The structure packages a certificate asserting exactly five accretion regimes around compact objects together with the canonical J-band certificate fixing the transition threshold. Astrophysicists modeling black-hole and neutron-star disks would cite it when mapping the J-cost to the slim-disk to photon-trapping boundary. It is introduced as a structure definition that directly assembles the Fintype cardinality of the regime enumeration with the six-clause canonical certificate.
Claim. Let $R$ be the inductive set of accretion regimes. The certificate consists of the assertion that the cardinality of $R$ equals five together with a canonical certificate $C$ satisfying $J(1)=0$, $J(x)=J(1/x)$ for $x≠0$, $J(φ)>0$, $0.11<J(φ)<0.13$, and $J(1/φ^2)>0$.
background
In the Recognition Science treatment of astrophysical accretion the J-cost function governs transitions between regimes. The inductive type enumerates five regimes: sub-Eddington thin, thick, slim, photon-trapped, and super-critical. The canonical certificate encodes the key J-cost properties: it vanishes at unity, is reciprocal, is positive at the golden ratio, lies in the narrow band (0.11, 0.13) there, and is positive at the reciprocal square of the golden ratio.
proof idea
The declaration is a structure definition that bundles two fields: the Fintype cardinality of the regime enumeration equaling five, and an instance of the canonical J-band certificate. No proof tactics are required; the definition simply declares the fields that must be supplied by any inhabitant.
why it matters
This structure supplies the certificate used by the downstream accretion-disk certificate definition to witness the five-regime structure and the J-band transition threshold. It fills the astrophysical application of the J-uniqueness and phi fixed-point results from the forcing chain. In the Recognition framework it connects the J-cost to observable accretion states, with the phi-band interval (0.11, 0.13) providing the quantitative prediction for the Eddington ratio at transition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.