phi_pow_neg962_upper_hypothesis
plain-language theorem explainer
The declaration encodes the inequality φ to the power -9.62 less than 0.0098 as a proposition supplying a numeric bound in the lepton ladder necessity module. Researchers closing mass predictions for the muon and tau from the Recognition Science forcing chain would reference this bound to seal the upper residue limit. It appears as a direct definition of the Prop with no internal derivation steps.
Claim. $φ^{-9.62} < 0.0098$, where $φ$ is the golden ratio.
background
The T10 Necessity module proves that muon and tau masses are forced from the electron structural mass (T9), step functions built from cube geometry (E_passive = 11, faces = 6, W = 17), the fine-structure constant α, and π, together with the golden ratio φ from T4. The lepton ladder is thereby determined without external axioms once the geometric constants are in place. This hypothesis supplies one of the φ-endpoint seam bounds needed to replace the original axioms in LeptonGenerations.lean.
proof idea
The declaration is a direct definition of the proposition as the stated real-number inequality. No lemmas or tactics are invoked inside the definition itself.
why it matters
The hypothesis is used by phi_pow_neg962_upper_proved and phi_pow_residue_mu_upper to close the upper bound on the muon residue term. It thereby advances the T10 goal of deriving the full lepton ladder from the eight-tick octave, D = 3, and the Recognition Composition Law. It touches the remaining task of converting all such numeric seam bounds into fully internal theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.