HawkingEffect
plain-language theorem explainer
Recognition Science associates Hawking radiation with exactly five effects in its strong-field A4 sector. A physicist deriving the Page curve or remnant mass in phi-ladder units would cite this enumeration to fix the configuration dimension at five. The inductive definition lists thermal spectrum, information paradox, evaporation, page curve, and remnant without further axioms or reductions.
Claim. The inductive type enumerating Hawking radiation effects consists of five constructors: thermal spectrum, information paradox, black-hole evaporation, Page curve, and remnant state.
background
In the Hawking radiation module the temperature takes the RS-native form T_H = phi^(-10)/(8M) after substituting hbar = phi^(-5) and G = phi^5/pi. The five effects are presented as exhausting configuration dimension D = 5. This rests on the phi^10 = 55 phi + 34 identity proved upstream in WeakNuclearForceFromRS.lean and on the general phi-ladder mass formula.
proof idea
The declaration is an inductive definition that introduces five distinct constructors. No lemmas or tactics are invoked; the structure itself supplies the finite enumeration required by the downstream cardinality statement.
why it matters
This definition supplies the finite set whose cardinality is asserted to be five in HawkingCert and proved by decide in hawkingEffectCount. It realizes the claim that Hawking radiation in RS units comprises exactly five canonical effects, linking the temperature factor positivity and phi^10 largeness checks to the eight-tick octave and dimensional forcing steps of the unified chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.