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

IndisputableMonolith.Physics.AnchorPolicyModel

show as:
view Lean formalization →

This module supplies a computable definition for the RG residue in Recognition Science, fixing it constant across scales and identical to the display gap(Z). Model builders working with single-anchor mass formulas at the RS-native scale cite it to replace external inputs with an internal closed form. The module is purely definitional, implementing the residue directly from the imported Z-map and gap function without additional axioms.

claim$f_ {residue}(Z) = F(Z)$ where $F(Z) = ln(1 + Z/φ)/ln(φ)$ is held constant in the renormalization scale, serving as the single-anchor residue model.

background

The module imports the RS time quantum τ₀ = 1 tick from Constants and the core bridge from RSBridge.Anchor. The latter defines the 12 Standard Model fermions, the charge-indexed integer Z_i = q̃² + q̃⁴ (+4 for quarks), and the display function gap(F) = ln(1 + Z/φ)/ln(φ). It also supplies massAtAnchor at the anchor scale μ⋆. The present module encodes the RG residue as a definition rather than a phenomenological axiom, making the single-anchor closed form directly computable.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the residue term required by downstream mass formulas that combine the yardstick with the phi-ladder rung and gap(Z). It closes the single-anchor model by turning the gap function into an explicit, scale-independent definition that can be referenced by any physics construction using the imported Anchor primitives.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (5)