canonicalAnchorSpec
plain-language theorem explainer
canonicalAnchorSpec sets the canonical anchor specification by direct reference to the canonical anchor object from AnchorPolicy. Researchers auditing residue certificates for fermion masses cite it to ground verification of the display identity at the anchor scale. The definition is a one-line alias that imports the anchor without additional computation.
Claim. The canonical anchor specification is the canonical anchor object supplied by the anchor policy.
background
The module supplies numerical bounds for residues obtained by transporting experimental masses to the anchor scale. These bounds are intended to check the display identity axiom from AnchorPolicy, which equates the residue function evaluated at the anchor to the gap function of the corresponding Z value. The canonical arithmetic object from ArithmeticOf supplies a realization-independent initial Peano structure, while the identity event from ObserverForcing is the zero-cost recognition event at state equal to 1.
proof idea
This is a one-line definition that directly assigns the canonical anchor from AnchorPolicy to the AnchorSpec type.
why it matters
The definition supplies the fixed anchor point used by the residue certificates in this module to verify the display identity at anchor. It thereby connects the audit data for leptons and quarks to the theoretical gap function and the phi-ladder mass formula. The construction closes the interface between the imported anchor policy and the numerical bounds that test the integer-rung model against experimental residues.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.