IndisputableMonolith.Recognition.Certification
This module supplies the closed-interval type and basic membership lemmas used to certify anchor residues in Recognition Science. It is imported by AnchorPolicyCertified to replace an external RG-residue axiom with explicit interval bounds. The module contains only definitions and elementary interval facts; no theorems are proved here.
claimA closed interval $[lo, hi]$ is the set of reals $x$ satisfying $lo \leq x \leq hi$. Membership $x ext{ memI } I$ and width $w(I)$ are defined directly from the endpoints. AnchorCert, Igap, and Valid are predicates that assert a residue lies inside a certified interval of controlled width.
background
The module sits inside the Recognition domain and defines the primitive Interval lo hi together with memI, width, and abs_sub_le_width_of_memI. These objects formalize the closed interval with endpoints lo ≤ hi. Sibling declarations then build AnchorCert, Igap, Valid, M0_pos_of_cert, anchorIdentity_cert, equalZ_residue_of_cert, zeroWidthCert and zeroWidthCert_valid on top of the interval primitives. The setting is the certification layer that lets downstream physics modules avoid global axioms for Standard-Model residues.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module is imported by IndisputableMonolith.Physics.AnchorPolicyCertified, which uses the certified interval predicates to replace the axiom |f_residue f μ⋆ - gap(ZOf f)| < 1e-6 with explicit, checkable bounds. It therefore supplies the concrete objects needed to close the interface gap between Recognition.Certification and the physics anchor policy.
scope and limits
- Does not encode the full renormalization-group flow equations.
- Does not compute numerical values inside the alpha band.
- Does not discharge any hypothesis about the phi-ladder or J-cost.
- Does not contain the eight-tick octave or D = 3 derivations.