lepton_yardstick_explicit
This definition supplies the explicit numerical form of the lepton yardstick as 2 to the power -22 times phi to the -5 times phi to the 62. Researchers deriving lepton masses from the Recognition Science ladder cite it to confirm numerical compatibility with the general sector formula. The definition is a direct substitution of the lepton-specific exponents B_pow = -22, r0 = 62 and coherence factor phi^{-5}.
claimThe explicit lepton yardstick is defined as $2^{-22} phi^{-5} phi^{62}$.
background
The sector yardstick is given by $A_s = 2^{B_{pow}(s)} E_{coh} phi^{r_0(s)}$, where $B_{pow}$ is the binary exponent fixed by passive edge count, $E_{coh}$ is the coherence factor, and $r_0$ is the rung offset on the phi-ladder. For leptons the module derives $B_{pow} = -22$ from the 11 passive edges of the 3-cube and $r_0 = 62$ from four wallpaper tilings offset by the octave baseline rung 2. The coherence factor is taken as $phi^{-5}$ from the Recognition Science constants. This module isolates definitions to break import cycles in the T9 electron-mass chain.
proof idea
One-line definition that substitutes the lepton exponents directly into the general yardstick expression from the Anchor module.
why it matters in Recognition Science
The definition feeds the equality theorem lepton_yardstick_eq_explicit that closes the derived-versus-explicit check for the lepton sector. It supports the T9 chain step that obtains all lepton constants from D = 3 cube geometry, the 11 passive edges, the 17 wallpaper groups, and the 8-tick octave structure rather than free parameters.
scope and limits
- Does not derive the exponents B_pow or r0 from first principles.
- Does not evaluate the numerical value of the yardstick.
- Does not apply to non-lepton sectors.
- Does not address mass formulas beyond the yardstick itself.
formal statement (Lean)
151noncomputable def lepton_yardstick_explicit : ℝ :=
proof body
Definition body.
152 (2 : ℝ) ^ (-22 : ℤ) * phi ^ (-5 : ℤ) * phi ^ (62 : ℤ)
153
154/-- PROOF: The derived yardstick equals the explicit form. -/