Rsbridge Anchor

The anchor scale

In particle physics, the twelve fermions (matter particles: six quarks, three leptons, three neutrinos) have masses that span five orders of magnitude. The anchor scale (a chosen reference energy where calculations are pinned) is where Recognition Science's bridge module does its work. It defines a single integer for each fermion, derived from its electric charge, and then a smooth function of that integer. The result is a number called the residue at the anchor.

The bridge assigns each fermion a charge index: up-type quarks get 4, down-type quarks get -2, charged leptons get -6, neutrinos get 0. From this it builds a value Z (for quarks, Z = 4 + q² + q⁴; for leptons, Z = q² + q⁴; for neutrinos, Z = 0). The display function F(Z) = ln(1 + Z/φ) / ln(φ), where φ is the golden ratio, turns this integer into a real number. For the down quark, F(24) ≈ 5.74; for the up quark, F(276) ≈ 10.69; for the electron, F(1332) ≈ 13.95. The module proves that two fermions with the same Z have the same residue, a definitional identity.

The physical claim, stated as an axiom in the framework's AnchorPolicy module, is that this closed-form residue equals the integral of the mass anomalous dimension (a quantum correction to mass) transported from the anchor scale to the physical mass. This equality is what the framework calls Single Anchor Phenomenology, checked numerically to a tolerance of about one part in a million. The module itself proves the algebraic identities; the numerical match to measured masses is an external verification, not a theorem.

In Recognition Science, the anchor scale is where the framework's particle ladder meets the Standard Model. The module defines the mass at the anchor for each fermion using a rung index (an integer step on the framework's ladder) and the residue. Its key proved theorem, anchor_ratio, states that for two fermions with the same Z, the ratio of their masses at the anchor is exactly a power of φ: massAtAnchor(f) / massAtAnchor(g) = exp((rung f - rung g) * ln φ). This means family mass ratios, like electron to muon, are pure φ-powers, with no other factor. The module also encodes three generations as a surjective map, and defines an admissible family as fermions sharing a Z value and a common rung residue class modulo 360, the joint sync scale of the framework's 8-beat and rung-45 cycles.

What this establishes is a precise, machine-checked dictionary between the framework's discrete ladder and the Standard Model's particle content. The bridge does not derive the fermion masses from nothing; it provides the formal scaffolding for a claim that the framework's structure, anchored at a single scale, reproduces the observed pattern of family mass ratios as golden-ratio powers. The proof of the algebraic identities is complete; the physical identification with measured masses remains a checked hypothesis.

theorem equalZ_residue (f g : Fermion) (hZ : ZOf f = ZOf g) :
  residueAtAnchor f = residueAtAnchor g := by
  simp [residueAtAnchor, hZ]

theorem anchor_ratio (f g : Fermion) (hZ : ZOf f = ZOf g) :
  massAtAnchor f / massAtAnchor g =
    Real.exp (((rung f : ℝ) - rung g) * Real.log (Constants.phi)) := by
  unfold massAtAnchor
  set Af := ((rung f : ℝ) - 8 + gap (ZOf f)) * Real.log (Constants.phi)
  set Ag := ((rung g : ℝ) - 8 + gap (ZOf g)) * Real.log (Constants.phi)
  -- Since M0=1, factor cancels directly
  calc
    (M0 * Real.exp Af) / (M0 * Real.exp Ag)
        = (Real.exp Af) / (Real.exp Ag) := by simpa [M0]
    _ = Real.exp (Af - Ag) := by
              simpa [Real.exp_sub] using (Real.exp_sub Af Ag).symm
    _ = Real.exp ((((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g)))
                   * Real.log (Constants.phi)) := by
              have : Af - Ag
                    = (((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g)))
                       * Real.log (Constants.phi) := by
                        simp [Af, Ag, sub_eq_add_neg, add_comm, add_left_comm, add_assoc,
                              mul_add, add_mul]
              have h' :
                ((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g))
                = (rung f : ℝ) - rung g + (gap (ZOf f) - gap (ZOf g)) := by ring
              simpa [this, h']
    _ = Real.exp (((rung f : ℝ) - rung g) * Real.log (Constants.phi)) := by
              simpa [hZ, sub_self, add_zero, add_comm, add_left_comm, add_assoc, mul_add,
                     add_right_comm, mul_comm, mul_left_comm, mul_assoc]

/-- Surjectivity of the generation index: there are exactly three generations. -/
theorem genOf_surjective : Function.Surjective genOf := by
  intro i
  have h : i.val = 0 ∨ i.val = 1 ∨ i.val = 2 := by
    fin_cases i <;> simp
  rcases h with h0 | h12
  · -- i = 0
    refine ⟨Fermion.e, ?_⟩
    apply Fin.ext
    simp [genOf, h0]
  · rcases h12 with h1 | h2
    · -- i = 1
      refine ⟨Fermion.mu, ?_⟩
      apply Fin.ext
      simp [genOf, h1]
    · -- i = 2
      refine ⟨Fermion.tau, ?_⟩
      apply Fin.ext
      simp [genOf, h2]

What this page does not claim

The module does not prove that the closed-form residue equals the integrated RG residue; that equality is an axiom checked numerically. The module does not derive the fermion masses from first principles; it defines a mass formula at the anchor scale. The module does not claim the anchor scale itself is derived within the framework.

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/RSBridge/Anchor.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: