pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Masses.RSBridge.Anchor

show as:
view Lean formalization →

The module supplies the closed-form anchor display function F(Z) = ln(1 + Z/φ)/ln(φ) for the integrated renormalization-group residue at the anchor scale μ⋆. Mass derivations in the Recognition Science framework cite this when equating the residue to the gap function for charged fermions. It is a definition module that states the explicit formula together with its basic properties such as F(0) = 0 and monotonicity for Z > -φ.

claim$F(Z) = ln(1 + Z/φ)/ln(φ)$ with the property that the integrated mass anomalous dimension at the anchor equals $F(Z_i)$ for each species $i$, where $F(0) = 0$ and $F(Z) ≈ log_φ(Z)$ for large $Z$.

background

Recognition Science derives masses on a phi-ladder with a residue term supplied by the gap function. This module introduces the display function F as the closed form claimed to match the integrated RG residue at the anchor scale μ⋆. Upstream the time quantum τ₀ = 1 tick from Constants fixes the native units 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 formula used by GapFunctionForcing to close the affine-log family and by QuarkAnchorDerivation to obtain RS-native heavy-quark masses without PDG input. It bridges the geometric phi-ladder to the perturbative RG side as described in the CouplingLaw module.

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)