Masses Anchor R0 Down Quark Eq

A fixed number for the down quark

The down quark is one of the six quarks that make up protons and neutrons. In the Recognition Science framework, each particle sector carries two integers used to build a mass scale: a power B_pow and a starting rung r0, a discrete step on a ladder of values. The declaration r0_DownQuark_eq states that the down quark's starting rung is -5. The number comes from a short arithmetic identity: the framework defines r0 for the down quark as the total edges of a three-dimensional cube (12) minus the number of wallpaper groups (17), which equals -5.

The proof is a simple calculation, not a deep result. The machine-checked library of formal theorems verifies that the definition of r0 for the down quark reduces to -5 by ordinary arithmetic. It does not derive -5 from first principles, and it does not claim that this number matches any measured mass. The value is fixed by a definitional choice, and the framework's own documentation states that the sector assignment is not yet forced. The constant sits in the Model layer, meaning it is a chosen input, not a proved output.

What the declaration does establish is a precise, reproducible anchor. Anyone can compute the down quark's rung from the cube geometry and the wallpaper constant, and the result is exactly -5, no more and no less. This integer feeds into a larger yardstick formula that combines a power of two, a coherence energy, and a power of the golden ratio. The framework uses these yardsticks to build mass scales for all charged fermions and bosons, with the down quark's rung being one fixed point in that scheme.

The honest limit is clear: the declaration proves an arithmetic equality, not a physical law. It does not predict the down quark's mass, does not show that -5 is the only possible value, and does not claim experimental agreement. The framework's own status note says no proofs claim experimental agreement. The value -5 is a definitional anchor in a model, useful for internal consistency but not yet a derived prediction about nature.

theorem r0_DownQuark_eq : r0 .DownQuark = -5 := by
  simp only [r0, E_total, cube_edges, D, W, wallpaper_groups]
  norm_num

/-- Derived φ-exponent offsets per sector.
    These are NOT arbitrary—they come from wallpaper + cube geometry. -/
@[simp] def r0 : Sector → ℤ
  | .Lepton      => 4 * (W : ℤ) - 6             -- = 4 × 17 - (8 - 2) = 62
  | .UpQuark     => 2 * (W : ℤ) + (A : ℤ)       -- = 2 × 17 + 1 = 35
  | .DownQuark   => (E_total : ℤ) - (W : ℤ)     -- = 12 - 17 = -5
  | .Electroweak => 3 * (W : ℤ) + 4             -- = 3 × 17 + 4 = 55

What this page does not claim

This answer does not claim that -5 is derived from first principles. This answer does not claim that the down quark's mass is predicted or measured by this declaration. This answer does not claim that the sector assignment is forced rather than chosen.

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: