Physics Anchor Policy

The Anchor Policy

In particle physics, a mass is not a single number: it changes with the energy at which it is measured, a running set by quantum corrections. To compare two masses, one must choose a common energy, called the renormalization scale. Physics anchor policy is the Recognition Science (RS) rule for making that choice: it declares a specific scale, called mu-star, where the framework's geometric charge for a fermion maps directly onto its physical mass residue. The policy is a definitional choice, a scaffold for building a mass model, not a derived law.

The module that implements this policy is a formal, machine-checked library. It defines the display function F(Z), which takes an integer geometric charge Z and returns the mass residue, and it records the canonical anchor scale at 182.201 in the framework's units. It also fixes the three lowest fermion charges: the down quark at 24, the up quark at 276, and the electron at 1332. These are not derived from first principles; they are stated as definitions, with the proofs being mere computation from the chosen values.

The policy's content is a hypothesis about how the running of masses behaves. The module states that the integrated renormalization-group residue for a fermion equals the display function of its geometric charge. This identity is not proved from physics; it is assumed, so that downstream calculations can rely on a clean interface. The actual numerical transport of masses from low to high energy is done by external tools, not by the library. The module also includes a stability condition: it proves that if the second derivative of the residue is bounded, then the anchor scale is a stable point, meaning small shifts in the scale do not change the residue much.

Within the framework, this policy yields a specific prediction for mass ratios. The library proves that the ratio of the muon mass to the electron mass at the anchor scale equals the exponential of 11 times the natural log of the golden ratio, a number that evaluates to about 199.7. This is a theorem, but it rests entirely on the hypothesis that the display identity holds. The policy also addresses flavor structure: it shows that if the residue depends only on the geometric charge, then the leading mass terms are flavor-blind, with any corrections suppressed by Yukawa couplings. This is a consistency check, not a derivation of the Yukawa couplings themselves.

The anchor policy is best understood as a bridge. It takes the abstract geometric charges of the framework and connects them to the familiar language of particle masses, but it does so by assuming the key link rather than proving it. The value of the module is that it makes that assumption explicit and auditable, so that the rest of the framework can be built on a precise, checkable foundation. What a reader can take away is a clear picture of where the framework's assumptions live, and what would have to be true for its mass predictions to hold.

/-- The canonical anchor from Source-Super and the mass papers.

**CONVENTION STATUS** (P1.5 Policy Knob Audit):
- `muStar := 182.201 GeV` is a **declared convention**, NOT a fit parameter.
  It is determined by the BLM/PMS stationarity condition at the top-quark pole.
  The specific numerical value emerges from the RS structure, not from fitting
  to experimental data.
- `lambda := ln φ` is **derived** from the φ-ladder structure.
- `kappa := φ` is **derived** from the golden ratio.

These values are NOT adjusted to improve agreement with experiment.
They are fixed by the RS structure and then compared to experiment. -/
noncomputable def canonicalAnchor : AnchorSpec where
  muStar := 182.201
  muStar_pos := by norm_num
  lambda := Real.log phi
  kappa := phi
  equalWeight := True  -- Placeholder; the actual condition is checked numerically

/-- 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

/-- Hypothesis: f_residue matches the display function F(Z) = gap(Z). -/
def display_identity_at_anchor_hypothesis (f_residue : Fermion → ℝ → ℝ) : Prop :=
  ∀ f μ, f_residue f μ = F (ZOf f)

/-- **STABILITY BOUND THEOREM**

    The second derivative of the RG residue is bounded at the anchor.

    **Proof Structure**:
    1. The second derivative $\delta^2 f / \delta (\ln \mu)^2$ is proportional to $d\gamma/d\ln \mu$.
    2. In the perturbative regime near $\mu_{\star}$, the beta functions are small and smooth.
    3. A bounded second derivative ensures that the anchor is not a singular point.
    4. This provides the stability guarantee for the Single Anchor RG Policy.

    **STATUS**: HYPOTHESIS (higher-order stability) -/
theorem stability_bound_at_anchor (f_residue : Fermion → ℝ → ℝ)
    (h_bounded : ∀ f, |deriv (deriv (fun t => f_residue f (Real.exp t))) (Real.log muStar)| < 1) :
    ∀ (A : AnchorSpec), A.equalWeight →
      (A.muStar = muStar) →  -- Anchor alignment
      ∃ (ε : ℝ), 0 < ε ∧ ∀ (f : Fermion),
        |deriv (deriv (fun t => f_residue f (Real.exp t))) (Real.log A.muStar)| < ε := by
  -- Follows from the smoothness of RG flow in the vicinity of the anchor.
  -- REDUCTION: Perturbative unitarity ensures derivatives of anomalous dimensions are bounded.
  intro A _hA hA_eq
  -- The second derivative is bounded by 1 at muStar by hypothesis.
  -- Since A.muStar = muStar, the bound transfers directly.
  use 1
  constructor
  · norm_num
  · intro f
    rw [hA_eq]
    exact h_bounded f

What this page does not claim

The anchor scale mu-star is not derived from the framework's axioms. The mass ratios are not measured predictions; they follow only if the display identity hypothesis holds. The Yukawa spurion structure is not a derivation of the Yukawa couplings themselves.

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: