phi_pow_neg207063_lower_hypothesis
plain-language theorem explainer
This definition introduces a numerical hypothesis asserting that phi to the power of negative 20.7063 exceeds 4.705 times 10 to the minus 5. Researchers deriving the forced electron mass under T9 would cite this bound when checking phi-ladder numerics against the mass formula. The declaration is a direct one-line definition of the inequality as a proposition with no further reduction steps.
Claim. $phi^{-20.7063} > 4.705 times 10^{-5}$
background
The module develops T9 necessity, showing the electron mass formula is forced from T8 ledger quantization and geometric constants derived earlier. Phi is the self-similar fixed point from the forcing chain T6, satisfying the quadratic relation that yields the golden ratio. This hypothesis supplies a concrete lower bound on a high negative power of phi, supporting numerical verification steps in the phi-ladder mass formula yardstick times phi to the (rung minus 8 plus gap). The upstream CPM2D.Hypothesis structure bundles constants and functionals for projection-defect control in a GalerkinState model, entering here via module imports that anchor the broader physics context.
proof idea
The declaration is a definition that directly states the proposition as the given real-number inequality. No lemmas or tactics are applied; it functions as an abbrev-style hypothesis for downstream use inside the module.
why it matters
This hypothesis anchors a required numerical bound inside the T9 necessity argument for the electron mass, aligning with the phi fixed point from T6 and the eight-tick octave from T7. It fills a concrete step in the phi-ladder calculations that feed the mass formula. With no listed downstream uses, the definition closes a numerical scaffolding point in the electron-mass necessity chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.