electron_residue_lower_hypothesis
plain-language theorem explainer
The declaration states a hypothesis that the electron residue Δ exceeds -20.7063. Researchers closing the T9 necessity proof for the forced electron mass would cite this bound to establish the interval around the audited value near -20.70596. The definition is a direct Prop encoding of the lower bound with no computation.
Claim. Let $Δ = log_φ(m_obs / m_struct)$ be the electron residue. The hypothesis asserts $Δ > -20.7063$.
background
The T9 module proves the electron mass formula is forced from T8 ledger quantization and geometric constants. The residue Δ is defined as log_φ(m_obs / m_struct) with audited value -20.70596. Upstream results supply the electron_residue definition from ElectronMass.Defs and the Hypothesis structure from CPM2D for projection defects and energy control.
proof idea
This is a definition that directly encodes the lower bound hypothesis on electron_residue as a Prop. It serves as an interface for the interval bounds theorem.
why it matters
This hypothesis feeds the electron_mass_ledger_hypothesis theorem, which shows the residue matches (gap - refined_shift) within bounds and advances the T9 necessity claim. It closes part of the interval for the residue in the phi-ladder mass formula, linking to the eight-tick octave and D=3 in the RS framework. The note on current bounds limits precision to ~0.002 rather than the observed 1e-6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.