pith. sign in
module module high

IndisputableMonolith.Masses.RSBridge.Anchor

show as:
view Lean formalization →

The Anchor module supplies the closed-form display function F(Z) = ln(1 + Z/φ)/ln(φ) that equates the integrated mass anomalous dimension to the gap at the anchor scale μ⋆. Mass derivations for quarks and leptons cite this expression to close the RSBridge residue. The module records monotonicity, the boundary F(0) = 0, the large-Z asymptotic log_φ(Z), and canonical numerical values for charged fermions without introducing new derivations.

claim$F(Z) = ln(1 + Z/φ) / ln(φ)$. It satisfies $F(0) = 0$, is monotonically increasing for $Z > -φ$, and obeys $F(Z) ≈ log_φ(Z)$ for large $Z$. Canonical values are $F(24) ≈ 5.74$ (down quarks), $F(276) ≈ 10.69$ (up quarks), and $F(1332) ≈ 13.95$ (leptons).

background

This module belongs to the Masses domain and imports only the RS time quantum τ₀ = 1 tick from Constants. It introduces the anchor display function F(Z) as the candidate closed form for the integrated RG residue at scale μ⋆, with the explicit claim that the integrated mass anomalous dimension f_i(μ⋆) equals gap(ZOf i) for each fermion species i. The function is defined on Z > -φ and positioned as the bridge that converts the geometric φ-ladder into a perturbative residue.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the explicit gap expression used in the RSBridge mass formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap(ZOf f)) * log φ). It feeds GapFunctionForcing for affine-log family closure, QuarkAnchorDerivation for RS-native heavy-quark masses, QuarkSchemeReconciliation for RGE matching, QuarkScoreCard for theorem-grade tracking, RungConstructor.Basic for species definitions, and CouplingLaw for the geometric-to-perturbative unification. It directly fills the Tier 1.1 closure step that equates the residue to F(Z).

scope and limits

used by (6)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (19)