IndisputableMonolith.Verification.AnchorNonCircularityCert
Certificate layer for single-anchor non-circularity: SM one-loop beta coefficients depend only on gauge representations and charges, not on fermion masses. Stationarity and dispersion-minimum certificates package that structural independence for the RS mass ladder. Auditors of the anchor-scale mass framework cite it against circular-input objections. The module wires structural lemmas into named cert records rather than one deep theorem.
claimThe SM one-loop beta coefficients satisfy $\beta_0^{\mathrm{QCD}}=(11/3)C_A-(4/3)n_f T_F$ and $\beta_0^{\mathrm{QED}}=-(4/3)\sum_i Q_i^2$, depending only on group data (Casimirs, charges, active flavor count), not on fermion masses. RG transport from the single anchor $\mu_\star$ is therefore mass-independent at this order. Named certificates record stationarity bounds, a dispersion minimum, and $\beta$-mass-independence.
background
Recognition Science places fermion masses on a $\varphi$-ladder at a single anchor scale $\mu_\star$, with species indexed by $Z$ and display gap $F(Z)=\ln(1+Z/\varphi)/\ln\varphi$ (from the RSBridge anchor). Empirical residues are then compared after RG transport to a common scale. Colleagues' circularity worry is that running might smuggle the predicted masses back into the beta functions that define the transport.
Upstream, AnchorPolicy isolates the single-anchor phenomenology and stability/flavor hypotheses; RGTransport formalizes the map that defines the empirical residue $f^{\mathrm{exp}}$; Constants supplies the RS tick and $\varphi$. This verification module answers the circularity charge at the structural level: one-loop $\beta_0$ is fixed by gauge group factors alone.
QCD uses $C_A=N_c=3$, $T_F=1/2$, and $n_f$ active flavors; QED sums squared charges. Neither formula takes fermion mass as an input, so the transport kernel cannot depend on the ladder masses being certified.
proof idea
Definition-and-certificate module, not a single end-to-end proof. It records the SM beta structure (QCD/QED $\beta_0$ from Casimirs and charges), a canonical instance, and lemmas that $\beta$ is mass-independent and that stationarity is structural. Derived quantities such as $\lambda$ from $\varphi$ and positivity of $\mu_\star$ support the cert bundles. StationarityCert, DispersionMinCert, and NonCircularityCert package those facts as auditable records (certified bounds, certified dispersion minimum, mass-independence flag). Argument shape: spell the group-theoretic formulae, prove independence of mass parameters, then wrap into named certificates.
why it matters in Recognition Science
Closes the non-circularity audit for single-anchor phenomenology: masses at $\mu_\star$ via $F(Z)$ and the $\varphi$-ladder must not be inputs to the RG map that defines residues. Feeds the Verification domain's claim that anchor policy plus RG transport is structurally honest. No downstream Lean dependents are wired yet in the graph; the module is an interface for external review and for later mass-framework theorems that assume a certified anchor. Ties to AnchorPolicy's stated colleague concerns (radiative stability, flavor compatibility) by making mass-independence of $\beta$ an explicit, checkable object rather than prose.
scope and limits
- Does not derive two-loop or higher beta functions or threshold matching.
- Does not prove numerical mass predictions or fit residues to data.
- Does not discharge radiative-stability hypotheses left open in AnchorPolicy.
- Does not treat beyond-SM gauge groups or non-canonical flavor assignments.
- Does not assert used_by theorems; the export graph currently lists none.
depends on (4)
declarations in this module (18)
-
structure
SMBetaStructure -
def
canonicalSMBeta -
theorem
stationarity_structural -
theorem
beta_is_mass_independent -
theorem
lambda_from_phi -
theorem
muStar_positive -
structure
StationarityCert -
def
certified_stationarity_bounds -
structure
DispersionMinCert -
def
certified_dispersion_minimum -
structure
NonCircularityCert -
def
is_mass_independent -
def
is_parameter_free -
def
canonical_anchor_cert -
theorem
anchor_mass_independent -
theorem
anchor_parameter_free -
theorem
anchor_value -
theorem
anchor_scale_certified