Physics Anchor Policy Certified

Certified anchors

A physics anchor is a point where Recognition Science's internal predictions meet measured or computed values from the Standard Model. The framework's core theorems derive constants and particle properties from first principles, but some Standard Model quantities, such as renormalization group residues, come from external computation. The certified anchor policy governs how those external numbers enter the framework without being assumed as axioms.

In plain language, the module creates a receipt system. An external computation, such as a Python audit, produces a table of intervals: for each particle species, a range of possible residue values and a range of possible gap values. The module checks that this table is valid, then proves two things. First, every species' residue lies close to the closed-form gap value, within a bound derived from the certified intervals. Second, if two species share the same charge Z, their residues must lie within the same certified band. These are formal theorems in the machine-checked library of formal theorems, not assumptions.

What the module deliberately does not do is implement the Standard Model renormalization group equations inside the framework. The kernels and integration remain external. The certified anchor policy only makes the dependency explicit and machine-checkable: the external table is the certificate, and the framework's theorems verify that the certificate's consequences hold. This separation keeps the framework's own axioms clean while still allowing external physics to constrain its predictions.

The practical effect is a clear boundary. When a reader sees a claim about a particle mass or coupling in Recognition Science, they can trace whether it comes from the framework's proved chain or from a certified external input. The certificate is the audit trail, and the theorems ensure that any table passing the validity check yields the stated bounds. This is how the framework stays honest about what it derives and what it imports.

/-- 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)

/-- 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)

What this page does not claim

The module does not implement Standard Model renormalization group equations inside the framework. The module does not prove that the external tables are correct, only that their consequences follow if they pass the validity check.

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: