phi_pow_neg20705_upper_hypothesis
plain-language theorem explainer
This definition encodes the numerical hypothesis φ^{-20.705} < 4.709 × 10^{-5} for use in the T9 electron mass necessity argument. Researchers deriving particle masses from the Recognition Science forcing chain would cite it when closing the numerical gap between the phi-ladder and the observed electron mass. The declaration is a direct one-line definition of the inequality with no lemmas or reductions.
Claim. The hypothesis asserts that φ^{-20.705} < 4.709 × 10^{-5}, where φ is the golden ratio fixed point of the Recognition Science forcing chain.
background
Module T9 proves the electron mass formula is forced from T8 ledger quantization together with geometric constants obtained earlier. The hypothesis supplies a concrete upper bound on a high negative power of φ, drawn from interval estimates in sibling definitions such as phi_bounds and the Taylor expansions exp_taylor_10_at_481211. Local notation follows the phi-ladder mass formula yardstick · φ^{rung-8+gap(Z)} with constants c=1, ħ=φ^{-5}.
proof idea
The declaration is a direct definition of the Prop as the stated real-number inequality. No lemmas are invoked and no tactics are applied.
why it matters
The hypothesis closes a numerical step inside the T9 necessity proof that the electron mass is forced from T8 and prior constants. It supports the phi-ladder rung assignment for the electron and keeps the result inside the alpha^{-1} band (137.030, 137.039). No downstream theorems are recorded yet, leaving the bound as an open numerical interface for the full mass derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.