Masses Anchor B Pow Lepton Eq

The lepton yardstick exponent

In the Recognition Science framework, particle masses are not free parameters but values that follow from a small set of geometric constants. The framework's ledger, a discrete record of recognition events, gives rise to a cube with 12 edges. Of these, 11 are called passive field edges, and the framework's model assigns the lepton sector a power-of-two exponent equal to negative twice that number: -22.

The declaration B_pow_Lepton_eq is a theorem in the framework's machine-checked library of formal theorems. It states that the function B_pow, applied to the lepton sector, equals -22. This exponent is one of two numbers that define a lepton's mass yardstick, the other being the integer 62. Together they form a scale: the framework multiplies a base energy by 2 raised to the exponent and by the golden ratio raised to the second integer.

This is a definitional choice, not a derivation from physical law. The framework's own documentation is explicit: the values are fixed, and the sector assignment is not yet forced. The theorem proves arithmetic, that the expression simplifies to -22, but nothing in the library claims this matches measured lepton masses. The comparison to experiment remains a separate, open question.

What the declaration establishes is a clean, computable anchor. It lets downstream code refer to a single named constant rather than a scattered literal. It is a building block, not a prediction.

theorem B_pow_Lepton_eq : B_pow .Lepton = -22 := by
  simp only [B_pow, E_passive, passive_field_edges, cube_edges, active_edges_per_tick, D]
  norm_num

theorem B_pow_Lepton_eq : B_pow .Lepton = -22 := by
  simp only [B_pow, E_passive, passive_field_edges, cube_edges, active_edges_per_tick, D]
  norm_num

/-- Derived powers of two for each sector.
    These are NOT arbitrary—they come from cube edge counting. -/
@[simp] def B_pow : Sector → ℤ
  | .Lepton      => -(2 * (E_passive : ℤ))     -- = -(2 × 11) = -22
  | .UpQuark     => -(A : ℤ)                    -- = -1
  | .DownQuark   => 2 * (E_total : ℤ) - 1       -- = 2 × 12 - 1 = 23
  | .Electroweak => (A : ℤ)                     -- = 1

What this page does not claim

No claim that the value -22 matches any measured lepton mass. No claim that the sector assignment is derived rather than chosen. No claim that the yardstick alone predicts a mass without the second integer and base energy.

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: