HawkingCert
plain-language theorem explainer
HawkingCert packages three assertions for the RS derivation of Hawking radiation: the inductive type of effects has cardinality exactly 5, the dimensionless factor 1/(8 phi^10) is positive, and phi^10 exceeds 100. Black-hole thermodynamics researchers working from the phi-ladder would cite the certificate to confirm the temperature formula T_H = phi^(-10)/(8M) in native units. The structure is assembled directly from the Fintype instance on the five-effect enumeration, the factor definition, and the phi inequality theorem.
Claim. A structure certifying that the set of Hawking effects has cardinality 5, that the dimensionless factor $1/(8 phi^{10})$ is positive, and that $phi^{10} > 100$.
background
In the Recognition Science treatment of strong-field physics the Hawking temperature is recovered as T_H = phi^(-10)/(8M) in native units, using the relation phi^10 = 55 phi + 34. The inductive type enumerates five canonical effects (thermal spectrum, information paradox, evaporation, page curve, remnant) and carries a Fintype instance. The factor is defined as 1/(8 phi^10) and the inequality phi^10 > 100 is established by successive power reductions to the Fibonacci identity.
proof idea
The structure is a direct record definition that bundles the three properties. Cardinality is taken from the Fintype instance on the inductive type, positivity follows from the definition of the factor, and the inequality is supplied by the upstream theorem proved via nlinarith on successive powers of phi.
why it matters
The certificate supplies the three fields required by the downstream hawkingCert instance, closing the Lean formalization of Hawking radiation in the RS module. It confirms the temperature formula and the five-effect count without axioms or sorrys, linking the phi fixed point to black-hole thermodynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.