Physics Anchor Policy Family Ratio From Display

The family ratio theorem

The fermion mass spectrum, the set of masses for quarks and leptons, is one of the most precisely measured collections of numbers in physics and one of the least explained. The standard model of particle physics simply lists the masses as free parameters. The Recognition Science framework, a research program built around a machine-checked library of formal theorems, offers a different route: it derives a compact formula for ratios of fermion masses from a small set of assumptions.

The theorem, called family_ratio_from_display, states that the ratio of the masses of two fermions at a chosen anchor scale equals phi raised to the difference of their rung numbers, where phi is the golden ratio, approximately 1.618. The rung number is an integer assigned to each fermion in the framework. The theorem is proved in the framework's library, meaning its logical derivation has been verified step by step by a computer. It is not a numerical fit; it is a formal consequence of the framework's definitions and axioms.

The theorem's statement carries explicit conditions. It assumes a hypothesis called display_identity_at_anchor_hypothesis, which says that a certain residue function, representing the integrated effect of quantum corrections, equals a framework-defined function F of the fermion's Z charge. It also assumes an anchor specification with equal weight for all motifs. The proof itself is a direct application of a previously established lemma about anchor ratios. The theorem does not, by itself, assert that these hypotheses are true of the actual universe; it establishes a conditional implication: if the hypotheses hold, then the mass ratio formula follows.

The framework's library also contains a concrete instance: the ratio of the muon mass to the electron mass is derived as phi raised to the power 11. This is a specific, testable prediction. The derivation uses the same theorem with the rung numbers of the muon and electron, which are 13 and 2 respectively. The claim is not that this matches experiment to any stated precision; the pack provides no measured value for comparison. It is a formal derivation of a numerical value from the framework's assumptions, not an empirical verification.

/-- Family‑ratio at anchor: for fermions with equal Z, the mass ratio
    at the anchor is a pure φ-power determined by rung differences.

    This is a consequence of `display_identity_at_anchor` combined with
    the proven `RSBridge.anchor_ratio`. -/
theorem family_ratio_from_display (_f_residue : Fermion → ℝ → ℝ)
    (_h_disp : display_identity_at_anchor_hypothesis _f_residue)
    (_A : AnchorSpec) (_hA : _A.equalWeight)
    (f g : Fermion) (hZ : ZOf f = ZOf g) :
    massAtAnchor f / massAtAnchor g =
      Real.exp (((rung f : ℝ) - rung g) * Real.log phi) :=
  anchor_ratio f g hZ

/-- Family‑ratio at anchor: for fermions with equal Z, the mass ratio
    at the anchor is a pure φ-power determined by rung differences.

    This is a consequence of `display_identity_at_anchor` combined with
    the proven `RSBridge.anchor_ratio`. -/
theorem family_ratio_from_display (_f_residue : Fermion → ℝ → ℝ)
    (_h_disp : display_identity_at_anchor_hypothesis _f_residue)
    (_A : AnchorSpec) (_hA : _A.equalWeight)
    (f g : Fermion) (hZ : ZOf f = ZOf g) :
    massAtAnchor f / massAtAnchor g =
      Real.exp (((rung f : ℝ) - rung g) * Real.log phi) :=
  anchor_ratio f g hZ

/-- Family‑ratio at anchor: for fermions with equal Z, the mass ratio
    at the anchor is a pure φ-power determined by rung differences.

    This is a consequence of `display_identity_at_anchor` combined with
    the proven `RSBridge.anchor_ratio`. -/
theorem family_ratio_from_display (_f_residue : Fermion → ℝ → ℝ)
    (_h_disp : display_identity_at_anchor_hypothesis _f_residue)
    (_A : AnchorSpec) (_hA : _A.equalWeight)
    (f g : Fermion) (hZ : ZOf f = ZOf g) :
    massAtAnchor f / massAtAnchor g =
      Real.exp (((rung f : ℝ) - rung g) * Real.log phi) :=
  anchor_ratio f g hZ

/-- Instantiation for leptons: m_μ / m_e = φ^11. -/
theorem muon_electron_ratio (_f_residue : Fermion → ℝ → ℝ)
    (_h_disp : display_identity_at_anchor_hypothesis _f_residue) :
    massAtAnchor Fermion.mu / massAtAnchor Fermion.e =
      Real.exp ((11 : ℝ) * Real.log phi) := by
  have hZ : ZOf Fermion.mu = ZOf Fermion.e := by native_decide
  have h := anchor_ratio Fermion.mu Fermion.e hZ
  -- rung Fermion.mu = 13, rung Fermion.e = 2, so 13 - 2 = 11
  have hrung : (rung Fermion.mu : ℝ) - rung Fermion.e = 11 := by
    simp only [rung]
    norm_num
  simp only [hrung] at h
  exact h

What this page does not claim

The hypotheses of the theorem are asserted to be true of the actual universe. The theorem provides a numerical comparison to any measured fermion mass ratio. The theorem derives the absolute masses of fermions, only their ratios.

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/Physics/AnchorPolicy.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: