Masses Baseline Derivation Lepton Baseline Matches Anchor

The lepton baseline

The lepton baseline is the number 2. In the Recognition Science framework, particle masses sit on a ladder of integers, and this baseline is the starting rung for the electron, muon, and tau. The framework derives that starting value from the combinatorics of a three-dimensional cube, the same object that yields the quark baseline 4 and the neutrino baseline -54. The theorem lepton_baseline_matches_anchor states that this derived value equals the framework's assigned anchor for the electron family: the integer 2.

The derivation is short. A cube has 8 vertices, 12 edges, and 6 faces. The framework defines the lepton baseline as the number of active edges per tick plus one. At three dimensions, that count is 1, so the baseline becomes 2. The machine-checked library of formal theorems proves this equality directly, with no free parameters and no experimental input. The number 2 is not fitted to data; it falls out of the cube's structure.

What the theorem does not claim is just as important. It does not claim that any measured lepton mass equals 2. Masses in the framework are scaled by a phi-power ladder, so the baseline 2 is a structural index, not a physical mass in kilograms. The theorem also does not claim that the electron family is the only family with this baseline; it merely fixes the starting point. Finally, the theorem does not assert that the cube geometry is the unique source of this number; it shows that, within the framework's definitions, the cube produces it.

The consequence is that the lepton ladder has a definite foot. Once the baseline is fixed, the framework's generation ordering places the electron, muon, and tau at rungs 2, 13, and 19. A reader can now see why the lepton family starts where it does, at least within this account, and can check the derivation against the cube's own arithmetic.

/-- Consistency: matches the hardcoded value in Anchor.lean. -/
theorem lepton_baseline_matches_anchor :
    (lepton_baseline : ℤ) = Integers.r_lepton "e" := by
  simp [lepton_baseline, active_edges_per_tick, Integers.r_lepton]

/-- **B-11 DERIVED**: The lepton baseline rung from cube geometry. -/
def lepton_baseline : ℕ := active_edges_per_tick + 1

theorem lepton_baseline_eq : lepton_baseline = 2 := by
  unfold lepton_baseline active_edges_per_tick
  norm_num

/-- Lepton rungs: r_e, r_μ, r_τ -/
theorem lepton_rungs :
    lepton_baseline = 2 ∧
    lepton_baseline + passive_field_edges D = 13 ∧
    lepton_baseline + wallpaper_groups = 19 := by
  unfold lepton_baseline
  constructor
  · native_decide
  constructor
  · native_decide
  · native_decide

What this page does not claim

The theorem does not claim that any measured lepton mass equals the integer 2. The theorem does not claim that the cube is the only possible source of the baseline value. The theorem does not claim that the lepton family is the only family with this baseline.

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/BaselineDerivation.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: