Asymptotic SafetyRG Nucleus
This project formalizes a small but sharp part of asymptotic-safety quantum gravity: the UV-safe restriction on coupling regions becomes a genuine nucleus, exclusion theorems become constructive via Heyting negation, and phenomenological predictions are exposed through explicit calibration and drift budgets rather than narrative overreach.
Can quantum gravity admit a UV fixed point that is strong enough to organize matter-sector predictions, while still being formalized in a way that separates constructive proof from physical assumption? The nucleus formalization answers the algebraic part of that question: the UV-safe restriction can be expressed as a genuine closure-like operator with fixed-point logic, rather than as an informal projection slogan.
The underlying theory comes from Astrid Eichhorn's asymptotic-safety program and related work on matter couplings, top/Higgs predictions, and dark-matter portal screening. The formalization does not claim to settle the physics. It instead isolates a mathematically honest slice that can be verified: benchmark truncation data, linearized flow, admissible UV restriction, and theorem-level consequences.
The constructive step matters. When the safe locus is a nucleus carrier, exclusion claims can be stated internally as Heyting negation. This is stronger than translating everything back into classical contradiction after the fact.
The main discovery here is not a new physical constant. It is the reusable proof pattern: a physically meaningful admissibility restriction can be treated as a nucleus, and downstream prediction or exclusion theorems can be built on that carrier without collapsing into vacuity.
That same pattern is transferable to other RG, multiscale, or admissibility-driven theories inside HeytingLean.
| Round | Headline Result | Outcome |
|---|---|---|
| 1 | 2 HIGH + 4 MED findings | prediction vacuity, scale-independence, tensor balance issues identified |
| 2 | Residual LOW findings | decorative parameter removed; prediction layer strengthened |
| 3 | Documentation-only inconsistency | closed before publication packaging |
Formal Verification Certificate
The theorem layer was rechecked in an isolated worktree and exported as a standalone package. All strong claims on this page are bounded to that verified slice rather than the full Heyting repository.
Asymptotic Safety • Lean 4 + Mathlib • Apoth3osis Labs