hawkingEffectCount
plain-language theorem explainer
The theorem establishes that the inductive enumeration of Hawking radiation effects in Recognition Science contains exactly five members. Physicists deriving black hole thermodynamics from the RS temperature formula would cite this cardinality to confirm the configuration dimension. The proof is a one-line decision procedure that evaluates the derived Fintype instance of the inductive definition.
Claim. The set of Hawking effects has cardinality five: $|$ {thermal spectrum, information paradox, evaporation, Page curve, remnant} $| = 5$.
background
In the Hawking Radiation from RS module the temperature takes the native-unit form T_H = φ^{-10}/(8M), obtained by substituting the RS constants ħ = φ^{-5}, G = φ^5/π into the classical expression. The module associates five canonical effects with this temperature: thermal spectrum, information paradox, black hole evaporation, Page curve, and remnant. These effects are collected in the inductive type HawkingEffect, which derives DecidableEq, Repr, BEq and Fintype instances directly from its five constructors. The upstream temperature definition states that temperature is the inverse of the Lagrange multiplier β and equals the derivative of average energy with respect to entropy.
proof idea
The proof is a term-mode application of the decide tactic. The tactic succeeds because the inductive type HawkingEffect carries a derived Fintype instance whose cardinality is computed by enumerating the five constructors.
why it matters
The result supplies the five_effects component of the hawkingCert certificate, which also records positivity of the temperature factor and largeness of φ^{10}. It completes the enumeration step in the A4 strong-field derivation, confirming that the configuration dimension for Hawking phenomena equals five. The module documentation links the count to the RS temperature formula T_H M = φ^{-10}/8 and notes the absence of sorrys or axioms. It touches the open question of whether each of the five effects receives a full dynamical derivation from J-uniqueness and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.