Apoth3osis
>_PAPER.PROOF.CODE
← Back to PPC Index

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 REPORESEARCH PAGELEAN ARCHIVEIPFS ROOT
MODULES
20
19 source modules + sanity suite
THEOREMS
38
Theorem declarations in the asymptotic-safety stack
EXAMPLES
17
Compile-time regression assertions
LINES
1338
Asymptotic-safety stack plus sanity test
SORRY
0
No incomplete proof terms shipped
AUDITS
3
Final code verdict reduced to doc-only LOW
PAPER ↔ PROOF CORRESPONDENCE
Paper ThemeLean SurfaceStatus
UV fixed point and truncation dataCouplingSpace + BetaFunctionsPROVED
RG projection and UV admissibilityRGFlowPROVED
Nucleus structure on coupling regionsNucleusInstancePROVED
Matter lifts and calibrated phenomenologyMatterSector + GravityMatter + PredictionsPROVED
Scale-dependent ratchetScaleSymmetryPROVED
Tensor screening / antiscreening balanceTensorFieldTheory/*PROVED
Executable extraction sanityExtraction/* + SanityPROVED
>_KEY.MATHEMATICS
linearizedBeta_at_fixedPoint
βlin(g\*)=0\beta^{\mathrm{lin}}(g^\*) = 0

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

portal_beta_nonpos_of_screening
θp+Δp≤0  ∧  gp≥0⟹βplin≤0\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
πUV(πUV(g))=πUV(g)\pi_{UV}(\pi_{UV}(g)) = \pi_{UV}(g)

UV projection is a genuine idempotent restriction map.

portal_zero_of_uvSafe_and_screening
UV-safe(g)∧screening(g)⟹gportal=0UV\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:Nucleus(OrderDual(Set  CouplingPoint))j : \mathrm{Nucleus}(\mathrm{OrderDual}(\mathrm{Set}\; \mathrm{CouplingPoint}))

The RG restriction becomes a genuine nucleus on coupling regions.

heytingNegation_carrier
¬R(U)=Uc∩UVsafe\neg_R(U) = U^c \cap UV_{safe}

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

matter_matters
fgen>0∧ylift>0∧qlift>0⟹backReact>0f_{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∣≤Bc∧∣d∣≤Bd∧Bc+Bd≤τ⟹mt∈band|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
calibration⋅backreaction≤damping⋅mνmax⁡⟹mν≤mνmax⁡\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≤n⟹scaleSafeSet(n)⊆scaleSafeSet(m)m \le n \Longrightarrow \mathrm{scaleSafeSet}(n) \subseteq \mathrm{scaleSafeSet}(m)

Coarser scales yield smaller admissible regions.

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

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

balanced_nonGaussian_fixedPoint
balanced(τ)∧λ\*≠0⟹nonGaussianFixedPoint(τ)\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.

CouplingSpaceBetaFunctionsRGFlowFixedPointNucleusInstanceMatterSectorGravityMatterScaleSymmetryTensorFieldTheoryPredictionsExtractionSanity
Foundation Core Bridge Top level
>_PROOF.BLUEPRINT
DOWNLOAD .LEAN
DEFINITIONS
g∈R9g \in \mathbb{R}^9

Nine couplings, including the portal coordinate.

THEOREMS
QED
gportal\*=0g^\*_{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
FORMALLY VERIFIED • LEAN 4 • MACHINE-CHECKED • APOTH3OSIS∀∃⊢→∧∨¬≡QED38 theorems • 0 sorry20 modules · 3 audits0 SORRY

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 PAGEPPC INDEXGITHUB