Physics Anchor Policy Certified Equal Z Residue From Cert

Certified equal-charge residues

In particle physics, the renormalization group describes how a quantity such as a coupling constant changes with energy. The Recognition Science framework uses a discrete ledger of recognition events, a record of which configurations the universe distinguishes, to organize these flows. At a chosen energy scale, called an anchor, each particle species has a residue, a small correction term that encodes how far the species' behavior departs from a simple closed form.

The framework's machine-checked library, a collection of formal theorems verified by computer, contains a theorem named equalZ_residue_from_cert. In plain language, it proves: if two particle species share the same integer charge label Z, and if an external certificate provides valid bounds on their residues at the anchor, then the two residues must differ by no more than twice the certified error tolerance. The proof is fully formal: given the certificate's validity and the residue bounds, the inequality follows by a short chain of existing lemmas.

This theorem does not compute the residues themselves. It does not implement the renormalization-group equations in the machine-checked library. Instead, it turns an external numerical audit, for example a Python calculation, into a rigorously checkable statement: once you supply certified intervals for each species' residue, the framework can derive per-species closeness to the closed-form gap and equal-charge degeneracy bounds without assuming an equality axiom. The theorem's power lies in making the dependency explicit and machine-checkable, not in performing the physics.

For the reader, the consequence is a clean separation of duties. The external computation supplies the numbers; the framework supplies the logical guarantee that those numbers respect the theory's structure. If two species share a charge, their residues cannot be arbitrarily far apart, no matter what the external audit claims, as long as the certificate is valid. This is a modest but precise result: it constrains the input, it does not replace it.

/-- Equal-Z degeneracy bound from a certificate: if two species share the same Z, their residues
must lie within the certified band. -/
theorem equalZ_residue_from_cert
    (C : AnchorCert Species)
    (hC : Valid Z Fgap C)
    (resAtAnchor : Species → ℝ)
    (hres : ∀ f, memI (C.Ires f) (resAtAnchor f))
    {f g : Species} (hZ : Z f = Z g) :
    |resAtAnchor f - resAtAnchor g| ≤ 2 * C.eps (Z f) := by
  simpa [Species, Z, Fgap] using
    (equalZ_residue_of_cert (Z := Z) (Fgap := Fgap) (C := C) hC resAtAnchor hres hZ)

/-- If an external certificate bounds the per-species residues at the anchor, then every species'
residue is close to the closed-form display `gap(Z)` (inequality form). -/
theorem anchor_identity_from_cert
    (C : AnchorCert Species)
    (hC : Valid Z Fgap C)
    (resAtAnchor : Species → ℝ)
    (hres : ∀ f, memI (C.Ires f) (resAtAnchor f)) :
    ∀ f : Species, |resAtAnchor f - Fgap (Z f)| ≤ 2 * C.eps (Z f) := by
  -- Directly reuse the generic lemma.
  simpa [Species, Z, Fgap] using
    (anchorIdentity_cert (Z := Z) (Fgap := Fgap) (C := C) hC resAtAnchor hres)

What this page does not claim

The theorem does not compute or implement the Standard Model renormalization-group equations. The theorem does not assert that the residues are exactly equal, only that they lie within a certified band. The theorem does not derive the certificate itself; it only uses the certificate as an input.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/AnchorPolicyCertified.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: