Verification Quark Sector Audit

The unresolved quark sector

In particle physics, quarks come in six flavors, from the light up quark to the heavy top quark. A complete theory of particle masses should predict all six from a single set of rules. The Recognition Science framework attempts this, but its own verification module, the quark sector audit, documents a specific unresolved problem: two different coordinate conventions for quark masses coexist, and they are not mathematically equivalent.

The first convention, called Integer Rungs, is the core model. It is parameter-free, derived from cube geometry, and uses the formula m = yardstick(Sector) × φ^(r − 8 + gap(Z)), with rungs at 4, 15, and 21 for both up-type and down-type quarks. The second convention, called Quarter-Ladder, is a hypothesis module. It uses the formula m = electron_structural_mass × φ^R, where R takes quarter-integer values like 23/4 for the top quark and −71/4 for the up quark. This second convention explicitly uses measured PDG mass targets as inputs, so it is not parameter-free.

The audit proves these two conventions cannot be the same. A formal theorem, different_rung_types, shows that the quarter-integer 23/4 cannot equal any integer rung. The generation spacings also differ completely: Convention A has spacings of 11 and 6, while Convention B has spacings of 7.75, 2.5, and 5.5. The module defines a structure, UnifiedQuarkSector, listing what a unified sector would require: one coordinate convention, a forward prediction pipeline with no PDG targets in the loop, and the same structural footing as the lepton chain. No such reconciliation proof currently exists.

In plain language, the audit establishes a negative result. The quark sector is not yet a complete forward pipeline. Convention A gives only skeleton masses with 10% to order-of-magnitude errors without the gap(Z) term. Convention B achieves under 2% error for heavy quarks but only by fitting to measured values. Neither alone predicts all six quark masses from first principles. The theorem quark_problem_blocks_full_verdict states formally that the current status string is not "RESOLVED". This means the mass framework cannot claim to be fully correct for all fermions until the two conventions are reconciled into one.

/-- Convention B residues (from Physics/QuarkMasses.lean) -/
structure ConventionB_Residues where
  top     : ℚ := 23/4      -- 5.75
  bottom  : ℚ := -8/4      -- -2.0
  charm   : ℚ := -18/4     -- -4.5
  strange : ℚ := -40/4     -- -10.0
  down    : ℚ := -64/4     -- -16.0
  up      : ℚ := -71/4     -- -17.75

/-! The conventions use different reference masses. -/
-- Convention A: sector-specific yardsticks (different for up-type vs down-type)
-- Convention B: single electron_structural_mass base for all quarks

/-! The conventions use different rung types.
    Convention B requires quarter-integers (e.g., 23/4), which are not integers.
    Convention A uses only integers. -/
theorem different_rung_types :
    ¬(∀ (r : ℚ), ∃ (n : ℤ), r = ↑n) := by
  push_neg
  refine ⟨23/4, fun n => ?_⟩
  intro h
  have : (23 : ℚ) / 4 = ↑n := h
  have : (4 : ℚ) * ↑n = 23 := by linarith
  have : (4 : ℤ) * n = 23 := by exact_mod_cast this
  omega

/-- The quark sector problem means the mass framework verdict cannot be "fully correct." -/
theorem quark_problem_blocks_full_verdict :
    ¬(currentStatus = "RESOLVED") := by
  simp [currentStatus]

What this page does not claim

This module does not claim the quark sector is correct or resolved. This module does not claim the two conventions are equivalent. This module does not provide a unified quark mass formula.

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/Verification/QuarkSectorAudit.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: