Encyclopedia Verification Verification Quark Forward Pipeline

ARTICLE 5 claims 4 theorems 1 model

Verification Quark Forward Pipeline

A machine-checked pipeline computes all six quark masses from geometry and charge alone, with no measured mass as input.

Verify this page

The forward pipeline

The standard model of particle physics measures six quark masses and lists them in tables. The verification quark forward pipeline is a different kind of object: a single calculation that produces all six quark masses from a small set of counting numbers, the golden ratio, and the fine-structure constant. No measured quark mass enters any formula. The pipeline is a forward prediction, not a fit.

The calculation works in dimensionless ratios. Instead of absolute masses, which need a calibration seam, the pipeline outputs m_quark / m_electron, the mass of each quark relative to the electron. These ratios are seam-free and directly testable against experiment. The pipeline has five steps: a sector yardstick from cube geometry, an integer rung from generation torsion, a band correction from the charge-band map, a predicted mass, and finally the ratio to the electron mass.

In Recognition Science, the framework models particle masses on a phi-power ladder. The golden ratio phi is the unique self-similar scaling forced by the framework's cost theorem. The pipeline assigns each quark a yardstick, a rung on the ladder, and a charge-band correction. The yardstick comes from cube geometry: the up sector uses B_pow = -1 and r0 = 35, the down sector uses B_pow = 23 and r0 = -5. The rungs come from generation torsion: up, charm, top get 4, 15, 21, and down, strange, bottom get the same. The charge-band map gives Z = 276 for up-type quarks and Z = 24 for down-type quarks.

The machine-checked library of formal theorems proves structural facts about this pipeline. It proves that every predicted mass is positive. It proves that the charm-to-up mass ratio equals phi^11 and the bottom-to-strange ratio equals phi^6. It proves that all six quark predictions have derived residue coordinates, meaning each mass can be written as a residue mass relative to the electron. It also proves a non-circularity structure: the yardsticks come from geometry, the rungs from torsion, and the Z-values from charges, with no mass input anywhere.

The key equation for the predicted mass is m_i(μ*) = A_s × φ^(r_i - 8 + gap(Z_i)), where A_s is the sector yardstick, r_i is the integer rung, and gap(Z_i) = log_φ(1 + Z_i/φ) is the band correction. The pipeline equals a residue form, which connects it to the framework's core mass structure. What this establishes in plain language: the six quark masses are not six free parameters. They are six outputs of one geometric and arithmetic structure, and the structure is checked by a machine.

MODEL QuarkNonCircularity · IndisputableMonolith/Verification/QuarkForwardPipeline.lean
QuarkNonCircularity · IndisputableMonolith/Verification/QuarkForwardPipeline.lean:234 
/-- The forward pipeline is non-circular: no PDG quark mass enters any formula.
    This is a DESIGN ASSERTION verified by inspection of the definition chain:
    predict_mass → yardstick → B_pow/r0 → counting-layer integers
    predict_mass → gap_correction → Z → charge-band map
    predict_mass → rung → baseline + torsion → counting-layer integers -/
structure QuarkNonCircularity where
  /-- Yardsticks come from cube geometry (no mass input) -/
  yardsticks_geometric : B_pow .UpQuark = -1 ∧ r0 .UpQuark = 35 ∧
                         B_pow .DownQuark = 23 ∧ r0 .DownQuark = -5
  /-- Rungs come from generation torsion (no mass input) -/
  rungs_from_torsion : r_up "u" = 4 ∧ r_up "c" = 15 ∧ r_up "t" = 21 ∧
                       r_down "d" = 4 ∧ r_down "s" = 15 ∧ r_down "b" = 21
  /-- Z-values come from charges (no mass input) -/
  Z_from_charges : Z .UpQuark (2/3) = 276 ∧ Z .DownQuark (-1/3) = 24
THEOREM charm_to_up_eq_phi11 · IndisputableMonolith/Verification/QuarkForwardPipeline.lean
charm_to_up_eq_phi11 · IndisputableMonolith/Verification/QuarkForwardPipeline.lean:126 
/-- Corollary: charm/up = φ^11 (rung difference 15 − 4 = 11). -/
theorem charm_to_up_eq_phi11 :
    m_charm / m_up = phi ^ (11 : ℝ) := by
  have := charm_to_up_ratio_structural .UpQuark (r_up "u") (r_up "c") (Z .UpQuark (2/3))
  simp only [m_charm, m_up] at this ⊢
  rw [this]
  congr 1
  simp only [r_up, tau, Masses.Anchor.E_passive,
    Constants.AlphaDerivation.passive_field_edges,
    Constants.AlphaDerivation.cube_edges,
    Constants.AlphaDerivation.active_edges_per_tick,
    Constants.AlphaDerivation.D]
  push_cast; norm_num
THEOREM bottom_to_strange_eq_phi6 · IndisputableMonolith/Verification/QuarkForwardPipeline.lean
bottom_to_strange_eq_phi6 · IndisputableMonolith/Verification/QuarkForwardPipeline.lean:140 
/-- Corollary: bottom/strange = φ^6 (rung difference 21 − 15 = 6). -/
theorem bottom_to_strange_eq_phi6 :
    m_bottom / m_strange = phi ^ (6 : ℝ) := by
  have := charm_to_up_ratio_structural .DownQuark (r_down "s") (r_down "b") (Z .DownQuark (-1/3))
  simp only [m_bottom, m_strange] at this ⊢
  rw [this]
  congr 1
  simp only [r_down, tau, Masses.Anchor.W,
    Constants.AlphaDerivation.wallpaper_groups,
    Masses.Anchor.E_passive,
    Constants.AlphaDerivation.passive_field_edges,
    Constants.AlphaDerivation.cube_edges,
    Constants.AlphaDerivation.active_edges_per_tick,
    Constants.AlphaDerivation.D]
  push_cast; norm_num
THEOREM m_up_pos · IndisputableMonolith/Verification/QuarkForwardPipeline.lean
m_up_pos · IndisputableMonolith/Verification/QuarkForwardPipeline.lean:85 
theorem m_up_pos : 0 < m_up := predict_mass_pos _ _ _
THEOREM all_quark_predictions_have_derived_residue_coordinates · IndisputableMonolith/Verification/QuarkForwardPipeline.lean
all_quark_predictions_have_derived_residue_coordinates · IndisputableMonolith/Verification/QuarkForwardPipeline.lean:195 
/-- A single canonical forward pipeline generates all six quarks; the quarter/residue
    convention is derived as a coordinate representation from that same pipeline. -/
theorem all_quark_predictions_have_derived_residue_coordinates :
    ∃ R_u R_c R_t R_d R_s R_b : ℝ,
      m_up = residueMass m_electron R_u ∧
      m_charm = residueMass m_electron R_c ∧
      m_top = residueMass m_electron R_t ∧
      m_down = residueMass m_electron R_d ∧
      m_strange = residueMass m_electron R_s ∧
      m_bottom = residueMass m_electron R_b := by
  refine ⟨residue_from_pipeline .UpQuark (r_up "u") (Z .UpQuark (2/3)),
    residue_from_pipeline .UpQuark (r_up "c") (Z .UpQuark (2/3)),
    residue_from_pipeline .UpQuark (r_up "t") (Z .UpQuark (2/3)),
    residue_from_pipeline .DownQuark (r_down "d") (Z .DownQuark (-1/3)),
    residue_from_pipeline .DownQuark (r_down "s") (Z .DownQuark (-1/3)),
    residue_from_pipeline .DownQuark (r_down "b") (Z .DownQuark (-1/3)), ?_⟩
  repeat' constructor
  · simpa [m_up] using pipeline_equals_residue_form .UpQuark (r_up "u") (Z .UpQuark (2/3))
  · simpa [m_charm] using pipeline_equals_residue_form .UpQuark (r_up "c") (Z .UpQuark (2/3))
  · simpa [m_top] using pipeline_equals_residue_form .UpQuark (r_up "t") (Z .UpQuark (2/3))
  · simpa [m_down] using pipeline_equals_residue_form .DownQuark (r_down "d") (Z .DownQuark (-1/3))
  · simpa [m_strange] using pipeline_equals_residue_form .DownQuark (r_down "s") (Z .DownQuark (-1/3))
  · simpa [m_bottom] using pipeline_equals_residue_form .DownQuark (r_down "b") (Z .DownQuark (-1/3)
    )

What this page does not claim

The pipeline does not prove that the predicted masses match measured quark masses. The fine-structure constant alpha is identified from the counting layer, not derived as a coupling. The physical bridge from recognition events to quark sectors remains open.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND