Pith. sign in
module module high

IndisputableMonolith.Physics.ElectronMass.BaselineDerivation

show as:
view Lean formalization →

Defines the lepton baseline rung as one above the active edge count: a charged state needs at least one edge (A = 1), so the minimal stable state sits at A + 1 = 2. Electron-mass workers cite it to pin the phi-ladder starting rung before gap and yardstick factors. The module equates that baseline to the electron rung via short algebraic identities on the cube-geometry edge count.

claimThe lepton baseline rung is $A+1$, where the active edge count is $A=1$. Thus the minimal stable charged lepton state sits at rung $2$. The module records $A=1$, the equality of the baseline with that value, and the match of the baseline to the derived electron rung on the $\varphi$-ladder.

background

Recognition Science places lepton masses on a $\varphi$-ladder: mass equals a yardstick times $\varphi$ raised to (rung $- 8 +$ gap$(Z)$). The electron is the lightest charged lepton, so its rung is the sector baseline before gap corrections.

Upstream Physics.ElectronMass.Defs isolates T9 electron-mass definitions and states that lepton sector constants come from cube geometry, not free parameters. Constants supplies the RS tick $\tau_0$; AlphaDerivation supplies the cubic-ledger seed assembly used elsewhere in the coupling sector.

The module doc fixes the combinatorial reading: a charged state must traverse at least one edge (the active edge $A=1$). The minimal stable state is therefore one rung above that edge count.

proof idea

Definition-plus-equality layer, not a deep proof stack. active_edges_eq_one fixes $A=1$ from the charged-edge requirement. lepton_baseline and lepton_baseline_eq set the baseline to $A+1=2$ and record the numeral equality. baseline_matches_electron_rung and electron_rung_derived identify that baseline with the electron's derived rung on the ladder. Argument shape is short rewriting against the Defs imports, not an inductive or analytic construction.

why it matters in Recognition Science

Closes the first combinatorial step of the T9 electron-mass chain: without a forced baseline rung, the $\varphi$-ladder mass formula has no integer starting point for the electron. Downstream mass theorems (outside this module's direct used_by list) consume the baseline when they assemble yardstick $\times\varphi^{(\mathrm{rung}-8+\mathrm{gap})}$.

In the broader forcing picture this sits after T5–T8 (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) and uses cube-edge counting consistent with the ledger geometry that also seeds the alpha construction. It does not itself produce a numerical MeV value; it only locks the rung offset that those later steps dress with gap and yardstick.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (5)