Masses Baseline Derivation Color Offset Eq Quark Baseline

The color offset identity

The declaration color_offset_eq_quark_baseline states that two quantities in the Recognition Science mass framework are equal: the color offset and the quark baseline. Both are defined as the number of edges per face of a cube, which at dimension 3 equals 4. The theorem is proved by definitional equality, meaning the two names refer to the same underlying value by construction.

In plain terms, the framework models particle masses as integers on a ladder derived from the geometry of a 3-dimensional cube. The quark baseline is the starting integer for quark masses, set at 4. The color offset is a separate structural quantity, also derived from the cube's face-edge count, that the framework uses to account for color charge. The identity says these two numbers coincide: the offset that distinguishes quark colors is the same as the baseline from which quark masses are built.

The framework's machine-checked library of formal theorems proves this equality directly. It also proves that both quantities equal 4, and that the quark baseline matches the framework's anchor values for the up and down quarks. These are structural identities within the framework's model; they are not measurements of physical quark masses.

What the declaration does not claim is that physical quark masses are 4 in any conventional unit, or that the color offset has been observed in experiment. The value 4 is a baseline integer in a theoretical ladder, not a measured mass. The framework compares its ladder against measured particle data separately, as an empirical check, not as part of this theorem.

/-- Color offset equals quark baseline (same geometric origin). -/
theorem color_offset_eq_quark_baseline : color_offset = quark_baseline := rfl

theorem color_offset_eq : color_offset = 4 := by
  exact edges_per_face_at_D3

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

/-- Color offset equals quark baseline (same geometric origin). -/
theorem color_offset_eq_quark_baseline : color_offset = quark_baseline := rfl

What this page does not claim

Physical quark masses are 4 in any conventional unit. The color offset has been observed in experiment. The equality is a measurement rather than a structural identity within the model.

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: