anchor_ratio
Family mass ratios at the anchor scale reduce to pure powers of phi for any two fermions sharing the same Z-value. Researchers deriving quark or lepton hierarchies from the recognition framework cite this to obtain explicit expressions such as the top-to-charm ratio. The proof is a direct algebraic reduction that cancels the base mass M0 and the gap terms once the equal-Z hypothesis is applied.
claimFor fermions $f$ and $g$ with $Z(f)=Z(g)$, the ratio of their anchor masses satisfies $m_*(f)/m_*(g)=e^{(r(f)-r(g))ln phi}$, where $m_*$ is the mass at the anchor scale, $r$ the rung index, and $phi$ the golden ratio.
background
The RSBridge.Anchor module supplies the bridge from the recognition framework to the twelve Standard Model fermions. Fermion is the inductive type listing d,s,b,u,c,t,e,mu,tau,nu1,nu2,nu3. ZOf(f) returns the integer charge index Z = q̃² + q̃⁴ (+4 for quarks). The gap function is the closed-form display F(Z) = ln(1+Z/phi)/ln(phi), claimed to equal the integrated RG residue at the anchor scale μ⋆. massAtAnchor(f) is defined as M0 * exp(((rung f)-8 + gap(ZOf f)) * ln phi) with M0=1 in native units. The module imports rung from Compat.Constants and gap from Gap45.Derivation; upstream arithmetic lemmas (add_assoc, add_comm, mul_add) from ArithmeticFromLogic are used for the exponent algebra.
proof idea
The tactic proof unfolds massAtAnchor, sets the exponents Af and Ag, then applies a calc block. It first cancels the common M0 factor by simpa, rewrites the ratio of exponentials as exp(Af-Ag) via Real.exp_sub, expands the difference of exponents with ring and simp using add_assoc, add_comm, mul_add, and finally substitutes the equal-Z hypothesis to drop the gap difference, leaving only the rung difference times ln phi.
why it matters in Recognition Science
This theorem supplies the anchor-side ratios used by QuarkAbsoluteBridgeScoreCard (bottom-strange, top-charm, charm-up, strange-down) and by AnchorPolicy (family_ratio_from_display, muon_electron_ratio). It realizes the Recognition Science mass formula on the phi-ladder: yardstick * phi^(rung-8+gap(Z)). The result supports the Single Anchor Phenomenology claim that gap(Z) matches the RG residue at μ⋆ and closes the step from the forcing chain (T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave) to concrete fermion predictions.
scope and limits
- Does not apply when ZOf f differs from ZOf g.
- Does not assign numerical rung values to individual fermions.
- Does not derive or prove the gap function.
- Does not address the physical location of the anchor scale μ⋆.
Lean usage
have hZ : ZOf .t = ZOf .c := by decide; have h := anchor_ratio .t .c hZformal statement (Lean)
107theorem anchor_ratio (f g : Fermion) (hZ : ZOf f = ZOf g) :
108 massAtAnchor f / massAtAnchor g =
109 Real.exp (((rung f : ℝ) - rung g) * Real.log (Constants.phi)) := by
proof body
Tactic-mode proof.
110 unfold massAtAnchor
111 set Af := ((rung f : ℝ) - 8 + gap (ZOf f)) * Real.log (Constants.phi)
112 set Ag := ((rung g : ℝ) - 8 + gap (ZOf g)) * Real.log (Constants.phi)
113 -- Since M0=1, factor cancels directly
114 calc
115 (M0 * Real.exp Af) / (M0 * Real.exp Ag)
116 = (Real.exp Af) / (Real.exp Ag) := by simpa [M0]
117 _ = Real.exp (Af - Ag) := by
118 simpa [Real.exp_sub] using (Real.exp_sub Af Ag).symm
119 _ = Real.exp ((((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g)))
120 * Real.log (Constants.phi)) := by
121 have : Af - Ag
122 = (((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g)))
123 * Real.log (Constants.phi) := by
124 simp [Af, Ag, sub_eq_add_neg, add_comm, add_left_comm, add_assoc,
125 mul_add, add_mul]
126 have h' :
127 ((rung f : ℝ) - 8 + gap (ZOf f)) - ((rung g : ℝ) - 8 + gap (ZOf g))
128 = (rung f : ℝ) - rung g + (gap (ZOf f) - gap (ZOf g)) := by ring
129 simpa [this, h']
130 _ = Real.exp (((rung f : ℝ) - rung g) * Real.log (Constants.phi)) := by
131 simpa [hZ, sub_self, add_zero, add_comm, add_left_comm, add_assoc, mul_add,
132 add_right_comm, mul_comm, mul_left_comm, mul_assoc]
133