Masses Anchor R Lepton Values

The lepton rung numbers

The electron, muon, and tau are the three charged leptons, the family of lightweight particles that includes the electron that orbits atomic nuclei. In the Recognition Science framework, each particle species receives a small set of integer labels, called rung numbers, that help fix its mass scale. The declaration r_lepton_values pins down three of those labels: the electron gets 2, the muon gets 13, and the tau gets 19. These numbers are not arbitrary; they come from a simple arithmetic pattern built on two geometric constants, 11 and 17, which the framework derives from the edges of a cube and the count of wallpaper groups.

The pattern works like this. The electron, the lightest lepton, starts with the rung number 2. The muon adds 11 to reach 13, and the tau adds 17 to reach 19. Here 11 is the number of passive edges in a cube, the edges that do not carry a transition in a single tick of the framework's recognition cycle. And 17 is the number of wallpaper groups, the 17 distinct ways a pattern can repeat in two dimensions. The declaration r_lepton_values is a theorem in the framework's machine-checked library of formal theorems, but it only proves the arithmetic: that the function named r_lepton returns 2, 13, and 19 for the three species. It does not prove that these numbers produce the measured masses.

In Recognition Science, the rung numbers feed into a larger formula for a mass yardstick. That formula multiplies a base energy by powers of two and powers of the golden ratio, with the rung number appearing in the exponent. The framework's model layer defines this yardstick and the rung numbers as a model, a definitional choice about how to organize the constants, not as a forced result. The docstring for the module is explicit: everything there lives in the Model layer, and no proofs claim experimental agreement. The framework does not yet force which sector, lepton or quark, owns which expression; that assignment remains open.

What the declaration establishes, then, is narrow but real. It shows that three rung numbers, 2, 13, and 19, follow from a consistent arithmetic scheme involving 11 and 17. It gives the framework a concrete, checkable starting point for lepton masses. It does not claim that the electron, muon, and tau masses match measurements, and it does not claim that the framework has derived those masses from first principles. The numbers are a labeled anchor, a place where the model can be compared against experiment later, not a finished prediction.

/-- Verify r_lepton values. -/
theorem r_lepton_values : r_lepton "e" = 2 ∧ r_lepton "mu" = 13 ∧ r_lepton "tau" = 19 := by
  simp only [r_lepton, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  norm_num

/-- Verify r_lepton values. -/
theorem r_lepton_values : r_lepton "e" = 2 ∧ r_lepton "mu" = 13 ∧ r_lepton "tau" = 19 := by
  simp only [r_lepton, tau, Anchor.E_passive, Anchor.W, passive_field_edges,
             cube_edges, active_edges_per_tick, D, wallpaper_groups]
  norm_num

/-- Sector yardstick `A_s = 2^{B_pow} * E_coh * φ^{r0}`. -/
@[simp] noncomputable def yardstick (s : Sector) : ℝ :=
  (2 : ℝ) ^ (B_pow s) * E_coh * Constants.phi ^ (r0 s)

What this page does not claim

The declaration does not prove that the electron, muon, and tau masses match measured values. The declaration does not force the assignment of rung expressions to particle sectors. The declaration does not derive the rung numbers from the framework's core forcing theorems.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Masses/Anchor.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: