pith. sign in
module module high

IndisputableMonolith.RSBridge.Anchor

show as:
view Lean formalization →

RSBridge.Anchor supplies the closed-form display function F(Z) = ln(1 + Z/φ)/ln(φ) together with supporting definitions for sectors, ZOf, gap, and residueAtAnchor. Mass-spectrum and RG-policy authors cite it to equate the integrated anomalous-dimension residue at the anchor scale μ⋆ with gap(ZOf i). The module is purely definitional; it states the claimed equality and lists monotonicity and asymptotic properties without Lean proofs.

claim$F(Z) = \frac{\ln(1 + Z/\phi)}{\ln \phi}$, with $F(0) = 0$, $F$ strictly increasing for $Z > -\phi$, and $F(Z) \sim \log_\phi Z$ for large $Z$. The module asserts that the RG residue at the anchor satisfies $f_i(\mu_\star) = \mathrm{gap}(ZOf i)$ for charged fermions with canonical values $F(24) \approx 5.74$, $F(276) \approx 10.69$, $F(1332) \approx 13.95$.

background

The module imports Constants (where $\tau_0 = 1$ tick) and Mathlib. It introduces the display function as the explicit closed form that the integrated RG residue is claimed to equal at the single anchor scale $\mu_\star$. Sibling definitions include Sector and Fermion types, sectorOf, tildeQ, ZOf (the effective charge label), gap (the phi-ladder rung offset), residueAtAnchor, and anchorEquality. These objects encode the mapping from fermion labels to the phi-ladder mass formula used throughout the mass framework.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the explicit residue function required by AnchorPolicy, AnchorPolicyModel, AnchorPolicyCertified, ElectronMass.Defs, ElectronMass.Necessity, Hadrons, AnomalousMoments, and RungConstructor.Proofs. It closes the interface between the phi-ladder (T5–T8) and the single-anchor RG policy by giving the closed form that downstream modules treat as the target of the equality $f_i(\mu_\star) = \mathrm{gap}(ZOf i)$.

scope and limits

used by (22)

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)