blackHoleClassCount
plain-language theorem explainer
The theorem asserts that the finite type of black hole classes has cardinality exactly five. A physicist working on strong-field gravitational solutions in Recognition Science units would cite this when confirming the configuration dimension for the A4 sector. The proof is a one-line decision procedure that evaluates the automatically derived Fintype instance on the inductive definition.
Claim. The set of black hole classes has cardinality five: $Fintype.card(BlackHoleClass) = 5$, where BlackHoleClass is the inductive type with constructors stellar, intermediate, supermassive, primordial, and Planck-scale.
background
The module derives the Schwarzschild radius in RS-native units with $G = φ^5/π$ and $ℏ = φ^{-5}$, so that $r_s = 2φ^5 M / π$. BlackHoleClass is defined as an inductive type whose five constructors label the canonical classes. The module states that this count equals the configuration dimension D = 5 in the strong-field sector.
proof idea
The proof is a term-mode one-liner that invokes the decide tactic. This tactic computes the cardinality directly from the Fintype instance generated by the five constructors of BlackHoleClass.
why it matters
It supplies the five_classes field inside the schwarzchildCert definition that certifies the overall radius result. The module documentation identifies the count as implementing configDim D = 5. In the Recognition framework it supports the strong-field limit consistent with the constants $c=1$, $ℏ=φ^{-5}$, $G=φ^5/π$ and the phi-ladder classification of mass scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.