Masses Baseline Derivation Quark Baseline Matches Anchor Up

The quark baseline

In the Recognition Science framework, particle masses are not inserted by hand; they are arranged on a ladder of integers called rungs, where each rung is a baseline number from which a particle's mass is built. The declaration quark_baseline_matches_anchor_up is a machine-checked theorem stating that the baseline for the up quark, computed from the combinatorics of a three-dimensional cube, equals the number 4. The proof is a direct calculation: the baseline is defined as the number of edges per face of a cube, which is 4, and the anchor for the up quark is also defined to be 4. The theorem simply confirms that these two definitions agree.

The number 4 itself comes from the cube. A cube has 4 edges meeting at each face, and the framework sets the quark baseline to this count. The derivation is not a measurement and not a fit; it is a definitional choice that the framework then proves is consistent with its own anchor table. The theorem quark_baseline_matches_anchor_up is one of several such consistency checks in the file BaselineDerivation.lean, which also proves the down quark baseline matches its anchor, the lepton baseline is 2, and the neutrino baseline is −54. These results upgrade what were previously assumed boundary values into derived, machine-checked statements.

What the theorem does not claim is that the number 4 is a physical prediction about the up quark's mass in kilograms or electronvolts. The baseline is an integer on an internal ladder; converting that ladder to measured particle masses requires additional scaling steps that are not part of this declaration. The theorem also does not claim that the up quark's mass is 4 times anything observable. It only establishes an internal consistency: the framework's own geometric derivation produces the same number that its anchor table assigns to the up quark.

In plain terms, this is a bookkeeping check. The framework keeps a ledger of recognition events, and the cost of recognition forces a specific mathematical structure. Within that structure, the baseline for the up quark turns out to be 4, and the theorem verifies that the derivation and the anchor agree. It is a small but necessary step: before the framework can compare its mass ladder to real particle data, it must first show that its internal numbers are coherent.

/-- Consistency: matches the hardcoded value in Anchor.lean. -/
theorem quark_baseline_matches_anchor_up :
    (quark_baseline : ℤ) = Integers.r_up "u" := by
  simp [quark_baseline, edges_per_face, D, Integers.r_up]

theorem quark_baseline_eq : quark_baseline = 4 := by
  unfold quark_baseline
  exact edges_per_face_at_D3

theorem quark_baseline_matches_anchor_down :
    (quark_baseline : ℤ) = Integers.r_down "d" := by
  simp [quark_baseline, edges_per_face, D, Integers.r_down]

theorem lepton_baseline_eq : lepton_baseline = 2 := by
  unfold lepton_baseline active_edges_per_tick
  norm_num

theorem neutrino_baseline_eq : neutrino_baseline_int = -54 := by
  unfold neutrino_baseline_int
  rw [total_geometric_at_D3]
  norm_num

What this page does not claim

The theorem does not predict a measured mass for the up quark in physical units. The theorem does not claim that the number 4 is derived from any experimental data. The theorem does not establish that the up quark's mass is 4 times any observable quantity.

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