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

IndisputableMonolith.RSBridge.Anchor

show as:
view Lean formalization →

RSBridge.Anchor defines the closed-form display function F(Z) = ln(1 + Z/φ)/ln(φ) as the integrated RG residue at the anchor scale μ⋆. Mass and flavor modelers cite it to equate f_i(μ⋆) with gap(ZOf i) on the phi-ladder. The module supplies only definitions and listed properties with no proofs or derivations.

claimThe display function is $F(Z) = {ln(1 + Z/φ)}/{ln φ}$ for $Z > -φ$, satisfying $F(0) = 0$, monotonic increase, and $F(Z) ≈ log_φ(Z)$ at large $Z$.

background

Recognition Science places all masses on a phi-ladder whose rungs are set by the J-cost function and the eight-tick octave. The anchor scale μ⋆ is the fixed point where the integrated mass anomalous dimension equals the residue gap(ZOf i). Constants supplies the RS time quantum τ₀ = 1 tick and the self-similar fixed point φ. The module isolates the explicit closed form that downstream RG policy modules treat as the target value for the residue.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Anchor supplies the explicit F(Z) that AnchorPolicy, AnchorPolicyModel, and RungConstructor.Proofs import to close the single-anchor residue claim. It directly supports the lepton mass table and the universal RS correction to anomalous moments. The definition fills the T5–T6 step that equates the RG integral to the phi-ladder gap at μ⋆.

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)