phi10_large
plain-language theorem explainer
The golden ratio satisfies φ¹⁰ > 100. Researchers deriving Hawking radiation temperatures in Recognition Science units cite this bound to establish positivity of the temperature-mass product. The proof reduces higher powers of φ from the base identity φ² = φ + 1 and closes the inequality with a numerical lower bound via linear arithmetic.
Claim. Let $φ = (1 + √5)/2$ be the golden ratio. Then $φ^{10} > 100$.
background
In Recognition Science the golden ratio φ obeys the defining relation φ² = φ + 1, which generates the Fibonacci recurrence for all higher powers: φ^n = F_n φ + F_{n-1}. The module HawkingRadiationFromRS works in RS-native units where ħ = φ^{-5} and G = φ^5/π, yielding the Hawking temperature T_H = φ^{-10}/(8M). Positivity of the product T_H M therefore reduces to the numerical claim φ^{10} > 100. Upstream lemmas supply the square identity and the tighter bound φ > 1.61.
proof idea
The tactic proof recalls phi_sq_eq to obtain φ² = φ + 1, then uses nlinarith to derive the explicit linear forms for φ³, φ⁴ and φ⁵. It rewrites φ^{10} as (φ^5)² by ring and finishes with nlinarith applied to the list containing phi_gt_onePointSixOne.
why it matters
The bound supplies the missing positivity field inside HawkingCert, the structure that certifies the five canonical Hawking effects (thermal spectrum, information paradox, evaporation, Page curve, remnant) in the RS setting. It directly supports the temperature formula derived from the constants ħ = φ^{-5} and G = φ^5/π, closing one concrete link between the phi-ladder and observable black-hole physics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.