module module high

`IndisputableMonolith.Physics.ElectronMass.Necessity`

Module Physics.ElectronMass.Necessity supplies interval bounds on the golden ratio φ together with Taylor error controls on exp and log at selected points. These close the numerical inequalities required for the electron mass residue in T9. Proofs rely on algebraic √5 comparisons imported from PhiBounds combined with power-function interval arithmetic.

claim$\phi = (1 + \sqrt{5})/2$ satisfies explicit rational interval bounds derived from $2.236^2 < 5 < 2.237^2$, together with error bounds on $\exp(10 \cdot \log x)$ and related terms at the points 481211 and 481212.

background

The module sits inside the T9 electron-mass layer of Recognition Science. It imports the RS time quantum $\tau_0 = 1$ tick, the geometric derivation of $\alpha^{-1}$ from the cubic ledger, and interval machinery for $\alpha^{-1}$ and $\phi$. PhiBounds supplies the core algebraic bounds on $\phi = (1 + \sqrt{5})/2$ via the inequality $2.236^2 = 4.999696 < 5 < 5.001956 = 2.237^2$. Pow supplies the identity $x^y = \exp(y \log x)$ for rigorous interval arithmetic on the phi-ladder exponents.

proof idea

The module consists of a sequence of lemmas. phi_bounds applies the √5 comparison directly. Subsequent lemmas (exp_taylor_10_at_481211, exp_error_10_at_481211, taylor_sum_eq_rational, etc.) expand the exponential to order 10, equate the partial sum to a rational, bound the remainder, and verify that the combined interval lies below the target threshold. All steps invoke the interval operations from Pow.

why it matters in Recognition Science

The bounds close the numerical side of the electron-mass necessity argument, feeding the parent module ElectronMass (T9) and LeptonGenerations.Necessity (T10). They also support MassResidueNoGo by confirming that the geometric band value gap(1332) ≈ 13.95 cannot be reproduced by a literal RG integral. The results rest on the T6 self-similar fixed point φ and the eight-tick octave structure.

scope and limits

Does not derive the electron mass formula itself.
Does not prove the full T9 theorem.
Limits to interval bounds at specific numeric points.
Does not address quark or neutrino sectors.
Does not replace the symbolic mass formula with numerics.

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Physics.ElectronMass module_import
IndisputableMonolith.Physics.LeptonGenerations.Necessity module_import
IndisputableMonolith.Physics.MassResidueNoGo module_import
IndisputableMonolith.Physics.NeutrinoSector module_import
IndisputableMonolith.Physics.QuarkMasses module_import
IndisputableMonolith.Physics.RecognitionCoupling module_import
IndisputableMonolith.RRF.Physics.LeptonGenerations.Necessity module_import
IndisputableMonolith.RRF.Physics.QuarkMasses module_import

depends on (10)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Constants.Alpha module_import
IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Numerics.Interval.AlphaBounds module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import
IndisputableMonolith.Numerics.Interval.Pow module_import
IndisputableMonolith.Physics.ElectronMass.Defs module_import
IndisputableMonolith.Physics.MassTopology module_import
IndisputableMonolith.RSBridge.Anchor module_import
IndisputableMonolith.RSBridge.GapProperties module_import

declarations in this module (45)

lemma phi_bounds L30
def exp_taylor_10_at_481211 L58
def exp_error_10_at_481211 L63
lemma exp_combined_lt_target L68
lemma taylor_sum_eq_rational L72
lemma error_term_eq_rational L80
lemma taylor_sum_lt_target L86
theorem log_lower_numerical L100
def exp_taylor_10_at_481212 L119
def exp_error_10_at_481212 L124
lemma exp_taylor_481212_gt_target L129
theorem log_upper_numerical L134
lemma log_phi_bounds L162
lemma alpha_bounds L175
lemma alpha_sq_bounds L198
lemma alpha_cube_bounds L209
lemma ledger_fraction_exact L225
lemma base_shift_bounds L229
lemma radiative_correction_bounds L234
lemma refined_shift_bounds L241
lemma electron_Z_value L251
def exp_67144_lt_824_hypothesis L256
def val_824_lt_exp_67145_hypothesis L259
lemma exp_six_upper L273
lemma exp_six_lower L284
def exp_taylor_10_at_7144 L298
def exp_error_10_at_7144 L303
lemma exp_07144_upper_q L307
lemma exp_07144_upper L311
def exp_taylor_10_at_7145 L334
def exp_error_10_at_7145 L339
lemma exp_07145_lower_q L343
lemma exp_07145_lower L347
theorem exp_67144_lt_824 L372
theorem val_824_lt_exp_67145 L385
theorem one_plus_1332_div_phi_lower L398
theorem log_824_lower L406
theorem one_plus_1332_div_phi_upper L413
theorem log_824_upper L421
lemma gap_1332_bounds L428
theorem structural_mass_bounds L471
def electron_residue_lower_hypothesis L547
def electron_residue_upper_hypothesis L550
def phi_pow_neg207063_lower_hypothesis L553
def phi_pow_neg20705_upper_hypothesis L556