module module moderate

`IndisputableMonolith.Physics.AnchorPolicy`

AnchorPolicy supplies the logarithmic definitions and anchor specifications that map fermion Z-values to mass gaps at the recognition scale. RS theorists and particle physicists cite it when verifying residue bounds after RG transport to the anchor. The module consists entirely of definitions and specifications that establish canonical anchors and stability conditions.

claimThe module defines $lnphi = ln(phi)$, the gap $F(Z) = ln(1 + Z/phi)/ln(phi)$, the anchor specification AnchorSpec, and canonical anchors for the electron, up quark, and down quark together with the stationary and stability conditions at those anchors.

background

The module sits inside the physics domain and imports the RS time quantum tau_0 = 1 tick from Constants, the RG transport formalism for experimental mass residues from RGTransport, and the core bridge objects (Fermion, ZOf, gap F, massAtAnchor) from RSBridge.Anchor. The gap function is the display map F(Z) = ln(1 + Z/phi)/ln(phi) that converts the integer charge index into a continuous rung on the phi-ladder. AnchorPolicy adds the policy layer that fixes the canonical locations and the identity axiom used by downstream residue certificates.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the display_identity_at_anchor axiom and the canonical anchors that ResidueData imports to produce the numerical audit certificates for experimental masses. It therefore closes the bridge between the RS forcing chain (T5 J-uniqueness, T6 phi fixed point) and the fermion mass ladder in the physics domain.

scope and limits

Does not compute numerical RG flows or residue values.
Does not prove the mass formula or phi-ladder spacing.
Does not address neutrinos or the full 12-fermion spectrum.
Does not derive alpha or other constants from the anchor.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.RSBridge.ResidueData module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Physics.RGTransport module_import
IndisputableMonolith.RSBridge.Anchor module_import

declarations in this module (19)

def lnphi L55
def F L59
theorem F_eq_gap L62
structure AnchorSpec L71
def canonicalAnchor L90
def canonicalZBands L103
theorem Z_electron L106
theorem Z_up L107
theorem Z_down L108
theorem f_residue L123
theorem stationary_at_anchor L145
theorem stability_bound_at_anchor L172
theorem display_identity_at_anchor L202
structure YukawaSpurion L213
def trivialYukawaSpurion L220
theorem mfv_compatible_at_anchor L235
def display_identity_at_anchor_hypothesis L257
theorem family_ratio_from_display L265
theorem muon_electron_ratio L274