pith. sign in
module module high

IndisputableMonolith.Physics.ElectronMass.Defs

show as:
view Lean formalization →

This module supplies the octave period (2^D = 8 for D = 3) together with ledger factors, secondary counts, and coherence exponents required for the electron mass derivation. It is imported by the main ElectronMass theorem, the baseline rung derivation, and all lepton generation modules. The module contains only definitions and equations with no proofs.

claimThe module exports the octave period $2^D = 8$ ($D=3$), the bilateral ledger factor, $N_{sec}$, lepton charge index $B$, electron baseline rung $r_e = 2$, lepton reference scale $R_0$, and coherence exponent derived from the cubic ledger geometry.

background

The module lives inside the T9 electron-mass block and imports the RS time quantum from Constants, the golden-ratio identity from PhiSupport, the refined ledger fraction delta from MassTopology, and the Z-map plus gap function from RSBridge.Anchor. Its central object is the octave period forced by T6 and T8, which sets the eight-tick cycle on the phi-ladder. These definitions convert the abstract anchor scale into concrete rung and coherence numbers used by the mass formula.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed the T9 electron-mass theorem and its necessity proof, as well as the T10 lepton-generation modules. They supply the octave period required by the eight-tick structure (T7) and close the bridge from RSBridge.Anchor to the concrete mass ladder. Downstream necessity results cite these constants to show the electron rung is geometrically forced rather than free.

scope and limits

used by (7)

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

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (27)