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
MENTAT Contribution Certificates
Immutable contribution records for the asymptotic-safety publication chain. Theory-level certificates point to the curated theory bundle; proof/kernel/bridge certificates point to the standalone Lean artifact bundle.
MENTAT Contribution Record
IDEA
Conceptual Contribution
CONTRIBUTION LEVEL: IDEA
Ontological EngineerUV Fixed Point Program for Quantum Gravity
Contributor
Astrid Eichhorn
Heidelberg University; formerly University of Southern Denmark
Eichhorn's asymptotic-safety program treats the ultraviolet fixed point of gravity not as a perturbative artifact but as the organizing principle for predictive quantum gravity. The contribution is conceptual: the physically relevant degrees of freedom can remain finite and structured at arbitrarily high energy.
MENTAT Contribution Record
THEORY
Mathematical Foundation
CONTRIBUTION LEVEL: THEORY
Ontological EngineerLinearized RG Flow with Gravitational Corrections
Contributor
Astrid Eichhorn
Heidelberg University; formerly University of Southern Denmark
The theory contribution combines benchmark truncation data, critical exponents, screened portal flow, matter backreaction, and tensor balance into a coherent RG slice. This is the mathematical layer formalized in Lean: a 9-dimensional coupling space, explicit flow laws, and admissibility structure.
Builds Upon
MENTAT Contribution Record
APPLICATION
Applied Contribution
CONTRIBUTION LEVEL: APPLICATION
Ontological EngineerPredictive Particle-Physics and Dark-Matter Consequences
Contributor
Astrid Eichhorn
Heidelberg University; formerly University of Southern Denmark
The application layer connects the RG picture to bounded top, Higgs, and neutrino predictions together with portal-based dark-matter exclusion. In the formalization, these remain conditional on explicit calibration, drift, damping, and screening assumptions rather than being overstated as unconditional empirical facts.
Builds Upon
MENTAT Contribution Record
PROOF
Formally Verified
CONTRIBUTION LEVEL: PROOF
Ontological EngineerLean 4 Formalization of the Asymptotic-Safety RG Nucleus
Contributor
Apoth3osis Labs
R&D Division
Apoth3osis Labs formalized the asymptotic-safety slice as a standalone Lean 4 package: 19 source modules, 38 theorem declarations, 17 compile-time regression examples, and zero sorry/admit. The central formal achievement is the order nucleus on UV-safe coupling regions together with constructive dark-matter exclusion via Heyting negation.
Builds Upon
MENTAT Contribution Record
KERNEL
Computationally Verified
CONTRIBUTION LEVEL: KERNEL
Ontological EngineerKernel Verification and Hostile Audit Closure
Contributor
Apoth3osis Labs
R&D Division
The formalization was re-audited through multiple hostile passes. High and medium findings on vacuity, predicate semantics, unused hypotheses, scale-independence, and misleading certificate naming were resolved. Final residual findings dropped to documentation-only LOW issues, which were also closed before publication packaging.
Builds Upon
MENTAT Contribution Record
BRIDGE
Cross-Level Connection
CONTRIBUTION LEVEL: BRIDGE
Ontological EngineerExecutable RK4 Mirror and Publication Bridge
Contributor
Apoth3osis Labs
R&D Division
The bridge contribution exports the theorem layer into a public-facing proof package, a research page, a PPC page, and C/Rust mirrors of the computational RG surface. The extraction stays honest by exposing only the computational slice that can actually be mirrored and compiled.
Builds Upon
Governed by MENTAT-CA-001 v1.0 · March 2026
“Once men turned their thinking over to machines in the hope that this would set them free. But that only permitted other men with machines to enslave them.”
Frank Herbert, Dune
A janitor who proves a theorem outranks a tenured professor who publishes noise.
Not as a slogan. As a structural fact of how the network operates. The only currency that matters is the quality of your contribution, measured not by committee but by mathematics.
A valid, original framing or conjecture
Formal argument with paper-level rigor
Connecting theory to observable outcomes
Working software the project depends on
Reproducible research with methodology and data
Machine-verified claim checked by a proof assistant
Foundational, load-bearing implementation
Connecting subsystems or knowledge domains end-to-end
Strategic direction & roadmaps
Writing, documentation & papers
Visual, UX & information design
Teaching, tutorials & workshops
Community, outreach & events
Partnerships, governance & policy
Translation, media & accessibility
Ethics, review & quality assurance
Every accepted contribution receives a MENTAT Contribution Record — cryptographically signed, IPFS-pinned, permanently yours. No committee decides your worth. The type checker does.