>_PAPER.PROOF.CODE

Asymptotic SafetyRG Flow as Nucleus in Lean 4

Astrid Eichhorn's asymptotic-safety program is formalized here as a constructive proof pipeline: linearized beta flow, UV projection, nucleus structure on coupling regions, calibrated phenomenology, tensor-balance witnesses, and executable RK4 extraction. The central move is algebraic, not rhetorical: the RG restriction is implemented as a genuine nucleus on UV-safe regions.

GITHUB REPO RESEARCH PAGE LEAN ARCHIVE IPFS ROOT

PAPER ↔ PROOF CORRESPONDENCE

Paper Theme	Lean Surface	Status
UV fixed point and truncation data	CouplingSpace + BetaFunctions	PROVED
RG projection and UV admissibility	RGFlow	PROVED
Nucleus structure on coupling regions	NucleusInstance	PROVED
Matter lifts and calibrated phenomenology	MatterSector + GravityMatter + Predictions	PROVED
Scale-dependent ratchet	ScaleSymmetry	PROVED
Tensor screening / antiscreening balance	TensorFieldTheory/*	PROVED
Executable extraction sanity	Extraction/* + Sanity	PROVED

>_KEY.MATHEMATICS

linearizedBeta_at_fixedPoint

\beta^{\mathrm{lin}}(g^\*) = 0

The linearized benchmark flow vanishes exactly at the gravitational fixed point.

portal_beta_nonpos_of_screening

\theta_p + \Delta_p \le 0 \;\wedge\; g_p \ge 0 \Longrightarrow \beta_p^{\mathrm{lin}} \le 0

Screening plus nonnegative portal coupling forces nonpositive portal flow.

projectToUVSafe_idempotent

\pi_{UV}(\pi_{UV}(g)) = \pi_{UV}(g)

UV projection is a genuine idempotent restriction map.

portal_zero_of_uvSafe_and_screening

UV\text{-safe}(g) \wedge \mathrm{screening}(g) \Longrightarrow g_{portal}=0

The simplest portal coupling is removed on the screened UV-safe locus.

orderNucleus / coreNucleus

j : \mathrm{Nucleus}(\mathrm{OrderDual}(\mathrm{Set}\; \mathrm{CouplingPoint}))

The RG restriction becomes a genuine nucleus on coupling regions.

heytingNegation_carrier

\neg_R(U) = U^c \cap UV_{safe}

Constructive exclusion is internalized as Heyting negation on the UV-safe carrier.

matter_matters

f_{gen}>0 \wedge y_{lift}>0 \wedge q_{lift}>0 \Longrightarrow \mathrm{backReact}>0

Matter content contributes a positive backreaction when the constituent lifts are positive.

topMass_from_shift_bound

|c| \le B_c \wedge |d| \le B_d \wedge B_c + B_d \le \tau \Longrightarrow m_t \in \mathrm{band}

Prediction bands are derived from separate calibration and RG-drift budgets.

neutrinoMass_below_target

\mathrm{calibration} \cdot \mathrm{backreaction} \le \mathrm{damping}\cdot m_\nu^{\max} \Longrightarrow m_\nu \le m_\nu^{\max}

The neutrino theorem uses model-side damping and backreaction rather than restating its conclusion.

scaleSafeSet_mono

m \le n \Longrightarrow \mathrm{scaleSafeSet}(n) \subseteq \mathrm{scaleSafeSet}(m)

Coarser scales yield smaller admissible regions.

rgDimensionalRatchet

\mathcal{R}_s : L \to L \text{ with monotone scale law}

The scale-indexed admissible sets package into a dimensional ratchet.

balanced_nonGaussian_fixedPoint

\mathrm{balanced}(\tau) \wedge \lambda_\* \ne 0 \Longrightarrow \mathrm{nonGaussianFixedPoint}(\tau)

The tensor quartic witness is derived through the screening/antiscreening balance mechanism.

>_CORRECTIONS

The prediction layer was tightened after audit so the mass-band theorems consume separate calibration and RG-drift budgets rather than a tautological final bound.

The tensor quartic witness now depends materially on the balance hypothesis instead of defining the conclusion into the predicate.

The scale ratchet is now genuinely scale-sensitive, and the old misleading RK4 error surface was renamed to a truthful projection certificate.

>_DEPENDENCY.GRAPH

Hover over the nodes to trace the proof spine from coupling-space definitions to the top-level prediction, extraction, and regression layers.

Foundation Core Bridge Top level

>_PROOF.BLUEPRINT

DOWNLOAD .LEAN

DEFINITIONS

g \in \mathbb{R}^9

Nine couplings, including the portal coordinate.

THEOREMS

QED

g^\*_{portal}=0

gravitationalFixedPoint_portalOff — The benchmark fixed point already lives on the portal-off slice.

>_ARTIFACTS

Lean Proof Artifacts

lean-proofs.tar.gz

Full extracted Lean proof surface.

DOWNLOAD

AsymptoticSafety/CouplingSpace.lean

9-dimensional coupling-space definitions.

DOWNLOAD

AsymptoticSafety/NucleusInstance.lean

The nucleus and Heyting-negation carrier.

DOWNLOAD

Tests/AsymptoticSafety/Sanity.lean

17 compile-time regression examples.

DOWNLOAD

Verified C Artifacts

asymptotic_safety.h

Shared data types mirroring the Lean coupling structures.

DOWNLOAD

coupling_space.c

Coupling-space arithmetic and fixed-point data.

DOWNLOAD

beta_functions.c

Linearized beta-vector field.

DOWNLOAD

rg_flow.c

Euler step, UV projection, and portal-off restriction.

DOWNLOAD

numerical_rg.c

RK4 mirror and demo portal run.

DOWNLOAD

verified-c.tar.gz

Archive of the C mirror surface.

DOWNLOAD

Safe Rust Artifacts

Cargo.toml

Standalone safe Rust crate manifest.

DOWNLOAD

src/coupling_space.rs

Coupling-space mirror types and helpers.

DOWNLOAD

src/beta_functions.rs

Critical exponents and linearized flow.

DOWNLOAD

src/rg_flow.rs

UV projection and admissibility checks.

DOWNLOAD

src/numerical_rg.rs

RK4 step and demo portal extraction.

DOWNLOAD

safe-rust.tar.gz

Archive of the Rust mirror surface.

DOWNLOAD

>_PROVENANCE.CHAIN

PAPERS

Eichhorn, Held, Donà, Shaposhnikov/Wetterich, tensor-balance sources

LEAN 4

Nucleus instance, constructive negation, calibrated prediction layer

MIRROR CODE

Faithful C and Rust computational mirrors of the flow surface

IPFS

Content-addressed archives for paper, proof, and code surfaces

>_IPFS

Lean Archive

Qmf9oT7JMAHUsMZFx1CrAxRd4GowKHsESxWLFmgvYAbw96

C Archive

QmcX5ftxjfgoJJh3qwHZyxKBSP5mcRAnbAyTDeeTiAUaR4

Rust Archive

QmQ4AmE6M41zc9a5jWcZJMF43ND9P1kdjNE2WDiodDmGzL

Root Bundle

QmNnesFQTbkL1gsR7jfMfhjpAaYGRdk7buyvNDrfwCao1w

>_VERIFICATION.SEAL

Formal Verification Certificate

The asymptotic-safety slice has been rechecked as a standalone Lean package and exported with matching C and Rust mirrors. The central nucleus claim and the downstream prediction/exclusion theorems are bounded to what the kernel and the extracted artifacts actually verify.

38 THEOREMS VERIFIED20 MODULES1,338 LINES0 SORRY3 HOSTILE AUDITS

Asymptotic Safety • Lean 4 + Mathlib • Apoth3osis Labs

RESEARCH PAGE PPC INDEX GITHUB

⊢⊣⊢⊣

>_MENTAT.JOIN

“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.

ONTOLOGICAL ENGINEER8 designations

IDEA

A valid, original framing or conjecture

THEORY

Formal argument with paper-level rigor

APPLICATION

Connecting theory to observable outcomes

CODE

Working software the project depends on

EXPERIMENT

Reproducible research with methodology and data

PROOF

Machine-verified claim checked by a proof assistant

KERNEL

Foundational, load-bearing implementation

BRIDGE

Connecting subsystems or knowledge domains end-to-end

NOETIC ENGINEER8 designations

VISIONARY

Strategic direction & roadmaps

NARRATOR

Writing, documentation & papers

DESIGNER

Visual, UX & information design

EDUCATOR

Teaching, tutorials & workshops

CULTIVATOR

Community, outreach & events

DIPLOMAT

Partnerships, governance & policy

INTERPRETER

Translation, media & accessibility

SENTINEL

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.

APPLY TO MENTAT EXPLORE PROJECTSMESH-ENCRYPTED NETWORK FOR TRUSTED AUTONOMOUS TRANSACTIONS