pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Physics.MassResidueNoGo

show as:
view Lean formalization →

MassResidueNoGo supplies no-go lemmas that exclude small residual mass terms near gap value 1332 on the phi-ladder. Researchers proving forced particle masses from the unified chain would cite these bounds to close loopholes. The module structure consists of four direct inequality lemmas that compare the gap function against explicit numerical thresholds.

claim$F(1332) > 13.953$, $|F(1332) - x| > 10$ for relevant $x$, and no mass residue lies within micro-tolerance of $F(1332)$, where $F(Z) = $ ln$(1 + Z/φ)/$ln$(φ)$ is the gap function.

background

The module sits inside the physics layer that converts recognition constants into particle masses. RSBridge.Anchor supplies the core objects: the fermion species set, the charge-indexed map ZOf, the gap display function $F(Z)$, and the anchor mass scale. ElectronMass.Necessity shows that the electron mass itself is forced once T8 ledger quantization and the geometric constants are fixed. MassResidueNoGo operates downstream of these definitions to test whether any leftover residue can survive the tolerance constraints.

proof idea

The module contains four sibling lemmas. gap_1332_gt_13_953 and abs_sub_gap1332_gt_ten establish strict lower bounds by direct evaluation of the gap function. not_within_micro_tolerance and small_x_ne_gap1332 then apply absolute-value comparisons to rule out proximity within the micro-scale window. All steps rely on algebraic properties of the logarithm already proved in the Anchor module.

why it matters in Recognition Science

These lemmas close potential escape routes in the mass formula by showing that residues near gap 1332 cannot fit inside the required tolerance. They therefore reinforce the T9 necessity claim that the electron mass is uniquely determined once the forcing chain reaches T8. The results sit inside the broader program that derives all particle masses from the single functional equation via the phi-ladder and the eight-tick octave.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (4)