Masses Anchor B Pow Down Quark Eq

The down quark yardstick

In the Recognition Science framework, particle masses are built from a small set of integer exponents. The declaration B_pow_DownQuark_eq proves that the exponent assigned to the down quark sector is exactly 23. This exponent is not a free parameter; it is computed from a cube geometry. A cube has 12 edges, and the formula is 2 × 12 − 1, which equals 23. The proof is a direct arithmetic check in the framework's machine-checked library of formal theorems.

This exponent appears in a yardstick, a scale used to construct mass values. The yardstick for a sector is 2 raised to the exponent, multiplied by a base energy and by the golden ratio raised to a second integer. For the down quark, the second integer is −5. The yardstick is a definitional choice, not a derived physical law. The framework's documentation states plainly that the sector assignment is not yet forced and that no proofs claim experimental agreement.

What the declaration does not claim is just as important. It does not claim that the down quark mass has been measured or predicted. It does not claim that 23 is the only possible value. The theorem only verifies that the definition of B_pow for the down quark sector evaluates to 23. It is arithmetic consistency, not physics discovery. The framework's own status notes say the sector assignment is not yet forced, meaning the choice of which sector gets which exponent is not derived from first principles.

The practical consequence is narrow but real: downstream calculations can rely on this value without re-deriving it. Any module that imports this definition knows the down quark exponent is 23, and the machine-checked proof guarantees the arithmetic. The larger question of whether these exponents correspond to measured particle masses remains open. The framework treats that comparison as an empirical check, not as a theorem.

theorem B_pow_DownQuark_eq : B_pow .DownQuark = 23 := by
  simp only [B_pow, E_total, cube_edges, D]
  norm_num

theorem B_pow_DownQuark_eq : B_pow .DownQuark = 23 := by
  simp only [B_pow, E_total, cube_edges, D]
  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 down quark mass has been measured or predicted. The exponent 23 is uniquely forced by the framework's axioms. The sector assignment is derived from physical principles.

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: