electron_residue_upper_hypothesis
plain-language theorem explainer
This definition packages the upper numerical bound hypothesis on the electron residue Δ = log_φ(m_obs / m_struct) as Δ < -20.7057. Researchers closing the T9 necessity argument for the forced electron mass would cite it to complete interval bounds on the residue. It is introduced by direct definition of the inequality to feed the residue bounds theorem without further computation.
Claim. Let $Δ := log_φ(m_{obs}/m_{struct})$ denote the electron residue. The hypothesis asserts the statement $Δ < -20.7057$.
background
The T9 Necessity module proves that the electron mass formula is forced from T8 ledger quantization and geometric constants derived earlier in the chain. The residue Δ is defined upstream as the base-phi logarithm of the ratio between observed electron mass in MeV and structural mass on the phi-ladder, with audited value -20.70596. The module also imports a hypothesis bundle from classical fluid models that encodes projection defects and energy controls for the physical embedding.
proof idea
This is a direct definition that sets the proposition equal to the strict inequality on the precomputed electron residue. It references the residue definition from the ElectronMass.Defs module with no additional lemmas or reductions applied.
why it matters
The hypothesis supplies the upper endpoint for the residue interval in the T9 theorem electron_mass_ledger_hypothesis, which shows the residue matches (gap - refined_shift) within 0.002. It completes numerical closure for the claim that the electron mass is determined by the phi-ladder and eight-tick octave from T0-T8. An open question is tightening the bounds to 1e-6 precision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.