not_within_micro_tolerance
plain-language theorem explainer
If a real number x satisfies |x| ≤ 0.1 then its distance to gap(1332) exceeds 10, so it cannot lie inside a 10^{-6} neighborhood of that anchor value. Physicists auditing whether Standard-Model RG residues can literally equal the closed-form geometric band value would cite this separation. The proof applies the auxiliary lemma abs_sub_gap1332_gt_ten to obtain a strict lower bound of 10 on the distance and derives an immediate contradiction with the transitivity and irreflexivity of the strict order on the reals.
Claim. If $|x| ≤ 0.1$ then $|x - gap(1332)| ≮ 10^{-6}$, where $gap(Z) = ln(1 + Z/φ) / ln(φ)$ and $gap(1332) > 13.953$.
background
The module records the numeric no-go that a small dimensionless RG residue cannot equal the closed-form anchor. The function gap(Z) is the display map F(Z) = ln(1 + Z/φ) / ln(φ) that the integrated mass anomalous dimension is claimed to match at the anchor scale μ⋆. For the integer 1332 this value is provably larger than 13.953. The hypothesis |x| ≤ 0.1 is the modeling assumption that the residue is small (order 10^{-2} to 10^{-1}).
proof idea
Proof by contradiction. The auxiliary theorem abs_sub_gap1332_gt_ten applied to |x| ≤ 0.1 immediately yields 10 < |x - gap 1332|. The assumption |x - gap 1332| < 10^{-6} together with lt_trans produces |x - gap 1332| < 10. These two strict inequalities contradict lt_irrefl applied to 10.
why it matters
This theorem supplies the explicit numeric separation that prevents equating a literal small RG residue to the geometric anchor gap(1332). It directly implements the module's core claim that small quantities cannot satisfy the anchor identity to micro-tolerance. In the Recognition framework it closes the loophole of identifying the integrated anomalous dimension with the phi-ladder expression without further structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.