pith. machine review for the scientific record. sign in
def definition def or abbrev high

predicted_electron_mass

show as:
view Lean formalization →

The definition supplies the T9 electron mass in RS-native units as the product of the pre-derived structural mass and a phi-powered correction from the gap function at 1332 minus the refined shift. Researchers deriving lepton masses from cube geometry and the phi-ladder would cite it as the explicit formula closing the sector constants. It is a direct one-line definition that composes the structural mass with the gap adjustment.

claimThe predicted electron mass equals the electron structural mass multiplied by $phi$ raised to the power $(g(1332) - s)$, where the structural mass is $2^{-22} phi^{51}$ from the lepton sector geometry and $g$ denotes the gap function.

background

The module isolates definitions for the T9 electron mass to avoid import cycles. It builds on D=3 forcing eight spatial dimensions via the 3-cube, which yields 12 total edges, one active edge per tick, and 11 passive field edges that set the binary exponent B_pow(Lepton) = -22. The rung offset r0(Lepton) = 62 follows from four wallpaper tilings (17 groups each) offset by the baseline rung 2 and the eight-tick octave period. The gap function, drawn from AnchorPolicy, returns the real exponent (log(1 + Z/phi))/log(phi) for a given sector and name; Mass is simply the type alias for real numbers.

proof idea

This is a one-line definition that multiplies the electron structural mass by phi raised to the difference between the gap evaluated at 1332 and the refined shift.

why it matters in Recognition Science

The definition implements the T9 electron mass formula and is used by the RRF.Physics.ElectronMass.Defs.predicted_electron_mass. It completes the chain from cube geometry (D=3), passive-edge count 11, wallpaper groups 17, and the eight-tick octave (T7) to a concrete value on the phi-ladder. It touches the open question of whether the resulting mass lies inside the alpha inverse band (137.030, 137.039).

scope and limits

formal statement (Lean)

 185noncomputable def predicted_electron_mass : ℝ :=

proof body

Definition body.

 186  electron_structural_mass * phi ^ (gap 1332 - refined_shift)
 187
 188/-! ## Main Theorems -/
 189
 190/-- Theorem: The Structural Mass is well-defined and forced by geometry.
 191
 192    m_struct = 2^(-22) * φ^(-5) * φ^62 * φ^(2-8)
 193             = 2^(-22) * φ^(62 - 5 + 2 - 8)
 194             = 2^(-22) * φ^51
 195
 196    Proof: Direct computation shows φ^(-5) * φ^62 * φ^(-6) = φ^51. -/

used by (1)

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

depends on (14)

Lean names referenced from this declaration's body.