bHThermoCount
plain-language theorem explainer
The declaration establishes that black hole thermodynamics in the Recognition Science setting is characterized by exactly five quantities. Researchers examining the four laws of black hole mechanics and their thermodynamic parallels would reference this count to fix the configuration dimension. The proof is a direct cardinality computation on the enumerated inductive type via the decide tactic.
Claim. The finite type of black hole thermodynamic quantities (temperature, entropy, mass, angular momentum, charge) has cardinality 5.
background
The module on Black Hole Thermodynamics from RS states that the four laws mirror ordinary thermodynamics and that black hole entropy takes the form S = A π / (4 φ^5) in RS units. The inductive type enumerates the five canonical quantities as temperature, entropy, mass, angular momentum, and charge, each equipped with DecidableEq, Repr, BEq, and Fintype instances. This count is identified with configDim D = 5, while the four laws are written as 2^2 = 2^(D-1). The upstream definition supplies the finite-type structure required for the cardinality statement.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the Fintype.card expression for the inductive type.
why it matters
The result populates the five_quantities field inside bHThermoCert, which certifies the full correspondence between black hole thermodynamics and standard thermodynamics. It supplies the numerical anchor for the module claim that five quantities align with configDim D = 5 and that the four laws equal 2^2. The declaration therefore closes the counting step that feeds the certification object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.