pith. sign in
module module high

IndisputableMonolith.RSBridge.Anchor

show as:
view Lean formalization →

The RSBridge.Anchor module supplies the closed-form display function F(Z) = ln(1 + Z/φ)/ln(φ) together with the auxiliary maps ZOf, gap and residueAtAnchor that equate the integrated RG residue to the phi-ladder label at the single anchor scale μ⋆. Mass-ladder and flavor-structure authors cite it when they need an explicit, auditable replacement for the Standard-Model residue. The module is purely definitional; it contains no theorems or proofs.

claim$F(Z) = {ln(1 + Z/φ)}/{ln φ}$ with the asserted equality $f_i(μ⋆) = gap(ZOf i)$ for each fermion sector i, where F(0) = 0, F is strictly increasing for Z > -φ, and F(Z) ∼ log_φ(Z) for large Z.

background

The module lives in the RSBridge domain and depends only on the RS time quantum τ₀ = 1 tick from Constants. It introduces the single-anchor scale μ⋆ and the display function F that is claimed to equal the integrated mass anomalous dimension at that scale. Auxiliary definitions include Sector and Fermion, the map sectorOf, the effective label tildeQ, ZOf (the rung or charge-squared label), gap (the phi-ladder defect), residueAtAnchor, anchorEquality and equalZ_residue.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

AnchorPolicy, AnchorPolicyCertified and AnchorPolicyModel import the module to obtain an explicit, Lean-native stand-in for the RG residue, removing the need for an opaque axiom. RungConstructor.Proofs and ElectronMass.Defs use the same F and ZOf to reproduce the charged-lepton table and the cube-geometry derivation of lepton constants. AnomalousMoments relies on the universal Z = 1332 value for the RS correction to (g-2).

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)