Verification Quark Coordinate Unification

One mass law, two coordinate systems

In the Recognition Science framework, particle masses are not arbitrary numbers. They sit on a ladder of powers of the golden ratio φ, about 1.618. The framework's library, a machine-checked collection of formal theorems, expresses this in two ways. The core form writes a mass as a sector scale multiplied by φ raised to an integer-rung exponent: m = A_sector · φ^(r − 8 + gap). The residue form writes the same mass relative to a reference mass: m = m_ref · φ^R. A reader might wonder whether these are two different physical laws. The answer is that they are not.

The two forms are connected by an explicit coordinate change. Given a sector scale, a rung, a gap, and a reference mass, the residue coordinate is R = log_φ(A_sector / m_ref) + (r − 8 + gap). The framework proves, as a formal theorem, that plugging this R into the residue form reproduces the core mass exactly, provided both the sector scale and the reference mass are positive. The reverse direction also holds: starting from a residue coordinate and a reference mass, one can recover a sector scale that makes the core form equal the residue form. A third theorem shows that the residue coordinate can be recovered from a residue-form mass by taking the logarithm base φ of the mass divided by the reference mass.

The structural conclusion is stated as a theorem: once a positive reference mass is fixed, for any positive sector scale, rung, and gap, there exists a residue coordinate R such that the core mass equals the residue mass. This is not a new physical assumption. It is a reparameterization of the same multiplicative φ-ladder. The choice between the two conventions is a matter of bookkeeping, not a choice between competing theories.

The practical consequence is that any result proved in one coordinate system carries over to the other without re-derivation. A physicist or mathematician working with quark mass tables can translate between the integer-rung picture and the reference-mass picture freely, knowing the translation is exact and machine-checked. The framework does not itself compare these masses to measured PDG values; that comparison is a separate empirical check. What it establishes is internal consistency: the two coordinate languages say the same thing.

/-- Core mass law shape (sector yardstick form). -/
def coreMass (A_sector : ℝ) (r : ℤ) (gap : ℝ) : ℝ :=
  A_sector * phi ^ (coreExponent r gap)

/-- Residue/quarter coordinate mass law shape (reference mass form). -/
def residueMass (m_ref : ℝ) (R : ℝ) : ℝ :=
  m_ref * phi ^ R

/-- Core form equals residue form under the explicit coordinate transform. -/
theorem core_eq_residue_of_positive
    {A_sector m_ref : ℝ} {r : ℤ} {gap : ℝ}
    (hA : 0 < A_sector) (hm : 0 < m_ref) :
    coreMass A_sector r gap = residueMass m_ref (residueFromCore A_sector m_ref r gap) := by
  unfold coreMass residueMass residueFromCore coreExponent
  have hratio : 0 < A_sector / m_ref := div_pos hA hm
  have hpow : A_sector / m_ref = phi ^ (Real.logb phi (A_sector / m_ref)) :=
    (Real.rpow_logb phi_pos phi_ne_one hratio).symm
  calc
    A_sector * phi ^ ((r : ℝ) - 8 + gap)
        = (m_ref * (A_sector / m_ref)) * phi ^ ((r : ℝ) - 8 + gap) := by
            field_simp [hm.ne']
    _ = m_ref * ((A_sector / m_ref) * phi ^ ((r : ℝ) - 8 + gap)) := by ring
    _ = m_ref * (phi ^ (Real.logb phi (A_sector / m_ref)) * phi ^ ((r : ℝ) - 8 + gap)) := by
          congr 1
          exact congrArg (fun t => t * phi ^ ((r : ℝ) - 8 + gap)) hpow
    _ = m_ref * phi ^ (Real.logb phi (A_sector / m_ref) + ((r : ℝ) - 8 + gap)) := by
          rw [← Real.rpow_add phi_pos]

/-- Recover residue coordinate from a residue-form mass exactly. -/
theorem recover_residue_coordinate
    {m_ref : ℝ} {R : ℝ}
    (hm : 0 < m_ref) :
    Real.logb phi (residueMass m_ref R / m_ref) = R := by
  unfold residueMass
  have hdiv : (m_ref * phi ^ R) / m_ref = phi ^ R := by
    field_simp [hm.ne']
  rw [hdiv]
  exact Real.logb_rpow phi_pos phi_ne_one

/-- Structural interpretation: once a positive reference mass is fixed,
the two coordinate systems are equivalent (up to explicit transforms). -/
theorem coordinate_systems_equivalent :
    ∀ {A_sector m_ref : ℝ} {r : ℤ} {gap : ℝ},
      0 < A_sector → 0 < m_ref →
      ∃ R : ℝ,
        coreMass A_sector r gap = residueMass m_ref R := by
  intro A_sector m_ref r gap hA hm
  refine ⟨residueFromCore A_sector m_ref r gap, ?_⟩
  exact core_eq_residue_of_positive hA hm

What this page does not claim

This framework does not compare quark masses to experimental measurements. This framework does not derive the value of φ or the existence of the mass ladder; it assumes the ladder and proves the coordinate equivalence. This framework does not assign specific values to sector scales or reference masses.

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