% FOR OVERLEAF: If iopart.cls is not available, uncomment the following 4 lines and comment out \documentclass[12pt]{iopart}:
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsfonts}
\usepackage{amsthm}
\usepackage{graphicx}
\usepackage{natbib}
\usepackage{booktabs}
\usepackage{hyperref}
\usepackage{xcolor}

% Better spacing
\setlength{\parskip}{0.5em}
\setlength{\parindent}{0pt}

% Theorem environments
\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{axiom}{Axiom}

% \documentclass[12pt]{iopart}

\begin{document}

\title{Zero-Parameter Quantum Gravity from Discrete Recognition Calculus}

\author{Jonathan Washburn\\
Independent Research, Austin, Texas, USA\\
\texttt{washburn@recognitionphysics.org}}
\date{}
% \address{Independent Research, Austin, Texas, USA}
% \ead{washburn@recognitionphysics.org}
% \submitto{\it Classical and Quantum Gravity}  % Comment out this line if using article class

\maketitle

\begin{abstract}
We derive classical and quantum gravity from a minimal information-theoretic axiom—a 
recognition event requires non-empty data—with parameter-fixed, gauge-rigid displays 
(dimensionless quantities invariant under admissible units moves). 
The discrete recognition calculus yields conserved ledger dynamics on graphs, forcing 
exact integer 1-forms, a unique convex cost functional $J(x)=\tfrac{1}{2}(x+x^{-1})-1$, 
and an 8-tick minimal period in three dimensions. 
These results dictate a discrete light-cone bound $\Delta r \le c\,\Delta t$ and a 
parameter-free Planck normalization $\lambda_{\mathrm{rec}} = \sqrt{\hbar G/(\pi c^3)}$. 
Mesh refinement recovers the continuity equation $\partial_t\rho+\nabla\!\cdot\!J=0$ and 
Einstein's field equations with emergent Lorentz invariance. 
The unique scale-recursion fixed point is the golden ratio $\varphi=(1+\sqrt{5})/2$, 
proven to be the only positive solution satisfying four independent physical constraints; 
we machine-verify that common alternatives ($e$, $\pi$, $\sqrt{2}$, $\sqrt{3}$, $\sqrt{5}$) fail. 
Beyond the linearized regime, we present an interacting, BRST-consistent quantum theory of gravity under the RS bridge: we derive the constraint algebra and gauge fixing, construct the Faddeev--Popov/BRST sector, and give a background-field renormalization with an RS-compatible UV mechanism expressed entirely in dimensionless displays. We further construct the nonperturbative gauge-fixed path integral as a discrete-exterior-calculus (DEC) limit that is background independent in the mesh refinement, and we reproduce black-hole semiclassics (Hawking temperature and entropy) with the RS normalization. All late-time phenomenology is expressed in terms of the explicit anchors introduced in the companion manuscripts. 
Structural theorems (T2--T7, bridge identities, completeness) are machine-verified in Lean~4; the expanded interacting/UV/nonperturbative/semiclassical results are presented as classical proofs with explicit audits and falsifiers. 
Key testable predictions: galaxy rotation curves with zero per-galaxy tuning 
(median $\chi^2/N=2.75$ vs.~MOND 2.47), subtle scale-dependent weak-lensing residuals, Solar-System PPN bands, gravitational-wave speed bands consistent with GW170817, and pulsar timing signatures at $\sim\!10\,\mathrm{ns}$. 
Nanoscale-$G$ claims are withdrawn in this manuscript pending external constraints.
\end{abstract}

\bigskip
\noindent\textbf{Scope.} This manuscript presents a parameter‑fixed, background‑independent quantization of gravity under RS: interacting (BRST‑consistent) dynamics, audit‑rigid ultraviolet bands via the background‑field method, a nonperturbative DEC\,$\to$\,continuum path‑integral construction, the correct GR limit, black‑hole semiclassics, and an audit‑rigid interface to the Standard Model at the representation/charge level. Standard‑Model couplings and anomaly freedom are established as RS integer identities (no spectral or Yukawa inputs); all displays are dimensionless and falsifiable. Items introduced beyond the Lean‑verified structural core are presented as classical derivations with explicit audits (see Table~\ref{tab:qg-verification}); precision cosmology, scattering/positivity, and machine verification of these new modules are deferred to companion work.

\bigskip
\noindent\textbf{Keywords:} quantum gravity; general relativity; discrete calculus; machine verification; Lean theorem proving; parameter-free physics; falsifiability

\section{Introduction}

\paragraph{Problem and stance.}
Modern fundamental physics explains an enormous range of phenomena, yet it leaves a basic structural gap: many of its key numbers are merely \emph{measured} and not \emph{derived}. This is the parameter problem. Our stance is parameter-fixed and gauge-rigid: only dimensionless displays that survive admissible gauge (units) moves are reported, and all such displays are fixed by derivation rather than fit. Concretely, admissible gauge moves jointly rescale the length and time anchors at fixed speed,
\[
(\ell_0,\tau_0)\mapsto (s\,\ell_0,s\,\tau_0),\qquad c=\frac{\ell_0}{\tau_0}\ \ \text{fixed},
\]
and we restrict attention to quantities invariant under these moves. In this gauge, a single route identity ties the two anchor routes to one dimensionless constant,
\[
\frac{\tau_{\mathrm{rec}}}{\tau_0}\;=\;\frac{\lambda_{\mathrm{kin}}}{\ell_0}\;=:\;K,\qquad \frac{\ell_0}{\tau_0}=c,
\]
so that calibration is unique up to units and no hidden "knobs'' remain. Within this posture we state our main classical claim: a discrete calculus reproduces general relativity (GR) in the continuum limit and yields a computable Planck normalization with concrete, falsifiable gravitational predictions.

\paragraph{Promise (scope and placement).}
All classical derivations needed to read the physics stand in the main text in conventional GR and astrophysics notation. The formal spine (discrete calculus, exactness, counting, and bridge invariants) and a machine-verified closure that audits the identities are relegated to the Methods and Appendix; they are policy-level supports, not prerequisites for reading the equations here.

\subsection*{The recognition axiom (information-theoretic framing)}

Our starting point is minimal: a recognition event requires non-empty data. Formally, there exists no recognition function on the empty set. We denote this constraint as \textbf{MP} (Meta Principle):
\[
\text{MP} := \neg\,\exists\,\mathsf{Recognize}(\varnothing,\varnothing).
\]
While tautological in classical logic, this information-theoretic constraint forces a discrete ledger structure with conserved double-entry bookkeeping. Recognition events must post to a non-void domain, inducing a directed graph of dependencies with integer-valued credits and debits. The axiom is minimal in the lattice sense: any weaker statement fails to derive the theorem bundle below (Theorem~\ref{thm:MinimalAxiom} in Methods proves necessity and sufficiency).

\subsection*{Why the golden ratio $\varphi$ is not numerological}

The golden ratio $\varphi=(1+\sqrt{5})/2$ appears throughout our results. This is not a choice or a fit; it is the unique positive solution to $x^2=x+1$, and this equation arises from \emph{four independent physical requirements}:
\begin{enumerate}
\item \textbf{Cost-functional fixed point.} The unique convex symmetric cost $J(x)=\tfrac{1}{2}(x+x^{-1})-1$ (Theorem~\ref{thm:T5}) admits a scale-recursion fixed point forcing $x^2=x+1$.
\item \textbf{Minimal 8-tick structure.} The minimal period $2^3=8$ in three dimensions (Theorem~\ref{thm:T6}), combined with causality bounds, yields temporal scales organized by $\varphi$.
\item \textbf{Recognition-closure uniqueness.} A selection criterion pairing recognition events with ledger closure admits exactly one positive solution (Theorem~\ref{thm:RecognitionRealityUnique} in Methods).
\item \textbf{Mass-ladder minimality.} Quantized spectra with integer rungs and minimal residues force $\varphi$-scaling; alternative bases destroy degeneracy structure.
\end{enumerate}
We explicitly prove that common mathematical constants \emph{fail} these constraints:
\begin{itemize}
\item $e\approx 2.718$: $e^2\approx 7.389 \ne e+1\approx 3.718$.
\item $\pi\approx 3.142$: $\pi^2\approx 9.870 \ne \pi+1\approx 4.142$.
\item $\sqrt{2}\approx 1.414$: $(\sqrt{2})^2=2 \ne \sqrt{2}+1\approx 2.414$.
\item $\sqrt{3}\approx 1.732$: $(\sqrt{3})^2=3 \ne \sqrt{3}+1\approx 2.732$.
\item $\sqrt{5}\approx 2.236$: $(\sqrt{5})^2=5 \ne \sqrt{5}+1\approx 3.236$.
\end{itemize}
These exclusions are machine-verified in Lean~4. Notably, $\sqrt{5}$ appears in the formula $\varphi=(1+\sqrt{5})/2$, yet $\sqrt{5}$ itself fails the criterion---only the specific combination $(1+\sqrt{5})/2$ satisfies $x^2=x+1$. Changing $\varphi$ to any other value breaks the derivation chain at multiple independent points; there is no freedom to ``tune'' this constant.

\subsection*{What is proved vs.\ what is predicted}

\paragraph{Proved (stated classically).}
(i) \textbf{Discrete exactness} implies potentials are unique up to an additive constant on each reach component (the classical ``potential up to a gauge constant''). (ii) In three spatial dimensions, \textbf{minimal complete coverage} of the unit cell takes exactly eight steps (an 8-beat Gray traversal). (iii) A \textbf{discrete light-cone bound} holds: radial advance per tick is upper-bounded by $c$ in the continuum limit. (iv) A \textbf{Planck normalization} is obtained and is reported in both length and dimensionless forms,
\[
\lambda_{\mathrm{rec}}=\sqrt{\frac{\hbar\,G}{\pi\,c^{3}}}\qquad\Longleftrightarrow\qquad
\frac{c^{3}\,\lambda_{\mathrm{rec}}^{2}}{\hbar\,G}=\frac{1}{\pi}\,.
\]
These results are derived without tunable parameters; the continuum statements appear in standard GR notation and the discrete scaffolding is provided for audit in the Methods/Appendix.

\paragraph{Predicted (with falsifiers; derivation status noted).}
(i) \textbf{Information-Limited Gravity (ILG)}: growth and rotation signatures that are 
global-only (no per-galaxy tuning), with lensing residuals that are subtle and scale dependent. 
Non-relativistic kernel properties are verified; covariant weak-field/PPN pieces are scaffolded. 
(ii) \textbf{Laboratory nulls at micrometer scales}: a predicted null in 
$10$--$100\,\mu\mathrm{m}$ torsion/oscillator experiments. 
(iii) \textbf{Nanoscale modifier $G(r)$}: withdrawn pending external constraints; no quantitative claim is made here.
(iv) \textbf{Pulsar tick discreteness} at the $\sim 10\,\mathrm{ns}$ level in stacked timing residuals. 
Each prediction is tied to an explicit audit or controls policy and comes with a fail-fast 
threshold documented in Methods/Experiments. No adjustable continuous parameters enter these displays.

\subsection*{How this differs}
The derivations introduce \emph{no per-object tunable parameters}; displays are parameter-fixed under the admissible units quotient. All equations in the body are written in conventional symbols (GR field equations, Poisson/growth in cosmology, and Newtonian rotation curves), and the mapping from the discrete calculus to these classical forms is exhibited explicitly through (a) the units quotient—observables are dimensionless and invariant under admissible $(\ell_0,\tau_0)$ rescalings at fixed $c$—and (b) a route identity that fixes the time-first and length-first constructions to the same dimensionless constant $K$. The result is a gauge-rigid bridge into standard practice: what we show in equations is exactly what we test.

% Editorial/style source for manuscript infrastructure (typesetting only). 

% Source note (not for typesetting): RS→CLASSICAL BRIDGE SPEC v1.0 
% Template note (not for typesetting): manuscript class/style scaffold 

\section{Discrete calculus $\to$ continuum: the classical scaffold}

This section states the classical surface of the discrete scaffold and its continuum limit. All proofs and any machine-verified details are deferred to the Methods and Appendix. No tunable parameters enter any statement below; only dimensionless displays survive admissible units moves.

\subsection{Atomic tick and conservation}\label{subsec:atomicity-continuity}

\paragraph{Axiom (atomic posting).} Time advances in indivisible ticks. At each tick exactly one posting occurs in the ledger. There is no concurrency per tick.

\paragraph{Conservation (closed-loop neutrality).} For any closed chain of posts, the net ledger flux is zero. Equivalently, the integer \emph{imbalance} $\varphi=\text{debit}-\text{credit}$ telescopes to the same value at start and end of any closed tour.

\paragraph{Continuum mapping.} Under mesh refinement with bounded densities and currents (space step $\Delta x\to 0$, time step $\Delta t\to 0$ at fixed ratio), discrete incidence maps to divergence and conservation becomes the usual continuity equation
\begin{equation}
\partial_t \rho + \nabla\!\cdot\! \mathbf{J} = 0\,,
\end{equation}
with $\rho$ the coarse-grained density and $\mathbf{J}$ the coarse-grained current. Proof details and the formal discrete statements (atomic tick; closed-chain flux zero) are deferred; here we only use their classical consequences.\footnote{Classical bridge and formal identifiers summarized in the internal specification. See Methods for the exact statements and proofs. Source: RS$\to$Classical bridge spec. }

\subsection{Exactness and potential uniqueness}\label{subsec:exactness}

\paragraph{Proposition (discrete exactness).} Let $w$ be an integer $1$-form on oriented edges of a locally finite graph. If the sum of $w$ around every finite closed chain is zero, then $w$ is a gradient: there exists an integer-valued potential $\varphi$ on vertices such that
\begin{equation}
w(u\!\to\! v) = \varphi(v) - \varphi(u)\,.
\end{equation}

\paragraph{Uniqueness up to constants.} On each reach component (weakly connected component), the potential is unique up to an additive constant: if $w=\nabla\varphi=\nabla\psi$ then $\varphi-\psi$ is constant on that component.

\noindent\emph{Classical role.} This is the usual discrete Poincaré lemma: zero circulation implies path independence, hence a potential. We use it to justify gauge freedom $\varphi\!\mapsto\!\varphi+c$ and to pass from conserved ledgers to potentials. Proof is deferred to Methods (formal T4).

\subsection{Cost functional and the action bridge}\label{subsec:cost-EL}

\paragraph{Statement (unique convex symmetric cost).} Among convex, symmetric, analytic costs on $\mathbb{R}_{>0}$ that satisfy $J(x)=J(x^{-1})$, $J(1)=0$, and $J''(1)=1$, there is a unique choice:
\begin{equation}
J(x) = \frac{1}{2}\left(x+\frac{1}{x}\right) - 1, \qquad x>0.
\end{equation}

\paragraph{Euler--Lagrange bridge (local quadratic regime).} Near equilibrium write $x=1+\varepsilon$ with $|\varepsilon|\ll 1$. Then
\begin{equation}
J(1+\varepsilon) = \frac{1}{2}\varepsilon^2 + O(\varepsilon^3),
\end{equation}
so a discrete action $\sum J(x_k)$ coarse-grains to a quadratic Dirichlet form. In the continuum, stationary paths solve the corresponding Euler--Lagrange equations of the quadratic limit (e.g., Laplace/Helmholtz-type equations for appropriate field identifications). Uniqueness of $J$ and the rigorous bridge to stationary action are deferred to Methods (formal T5); here we use only the classical picture and the quadratic expansion.

\subsection{Eight-tick minimality (3D) and coverage obstruction}\label{subsec:eight-tick}

\paragraph{Counting lemma (hypercube passes).} Consider the $D$-dimensional hypercube. Any spatially complete pass that visits each vertex at least once has period at least $2^{D}$. At threshold $T=2^{D}$ there exist bijective covers (e.g., Gray cycles). In three dimensions this yields:
\begin{equation}
\text{minimal period} = 2^{3}=8\,.
\end{equation}
For $T<2^{D}$, no surjection onto all $2^D$ vertex patterns exists (coverage obstruction). We use this purely as a counting input downstream; formal proofs and constructions are deferred to Methods (formal T6/T7).

\subsection{Causal cone bound and emergent Lorentz invariance}\label{subsec:cone-lorentz}

\paragraph{Discrete step bounds and anchors.} Let each admissible step advance time by a fixed tick $\tau_0$ and radius by at most a fixed length $\ell_0$. Define the anchor speed
\begin{equation}
c := \frac{\ell_0}{\tau_0}\,.
\end{equation}
Along any $n$-step path, $\Delta t = n\,\tau_0$ and $|\Delta r|\le n\,\ell_0$, hence the \emph{discrete cone bound}
\begin{equation}
|\Delta r| \;\le\; c\,\Delta t\,.
\end{equation}

\paragraph{Continuum Minkowski limit.} Under mesh refinement ($\Delta x,\Delta t\to 0$ at fixed $c$) with bounded velocities, the discrete cone bound defines a local light cone. In the limit, kinematics is locally Lorentz invariant and governed by the Minkowski metric: the invariant interval $ds^2=c^2 dt^2 - d\mathbf{x}^2$ separates timelike/causal displacements from spacelike ones. No free parameter enters: $c$ is fixed by anchors, and admissible units moves rescale $\ell_0,\tau_0$ together at fixed $c$. A formal step-bound lemma and its cone inequality are deferred to Methods.

\bigskip
\noindent\emph{Provenance.} The items above align with the discrete-to-classical bridge summarized in the internal specification: atomic tick (T2), continuity/closed flux (T3), potential uniqueness (T4), unique cost (T5), eight-tick minimality and coverage (T6/T7), and the causal cone bound. Methods give the exact propositions and their machine-verified status. Source: RS$\to$Classical bridge spec. 

\section{The bridge to classical observables (gauge rigidity)}

This section fixes the interface between discrete recognition statements and laboratory observables. Anchors are $(\tau_0,\ell_0;c)$ with the anchor identity $c=\ell_0/\tau_0$. The only admissible gauge moves are joint rescalings $(\tau_0,\ell_0)\mapsto (s\,\tau_0, s\,\ell_0)$ with $s>0$ at fixed $c$. An observable is a dimensionless display that is invariant under these moves. Route consistency is enforced by a single equality (the K-gate) tying two independent constructions of the same dimensionless constant. A Planck-side identity then pins the recognition length $\lambda_{\mathrm{rec}}$ on the $(\hbar,G,c)$ scale without any tunable parameters.

\subsection{Units quotient and dimensionless displays}\label{subsec:units-quotient}

\paragraph{Admissible gauge.}
We work on the anchor manifold $\mathcal{U}=\{(\tau_0,\ell_0;c):\ \tau_0>0,\ \ell_0>0,\ c=\ell_0/\tau_0\}$. The admissible rescaling is
\[
(\tau_0,\ell_0;c)\;\sim\;(\tau_0',\ell_0';c)\quad\Longleftrightarrow\quad
\exists s>0:\ (\tau_0',\ell_0',c)=(s\,\tau_0, s\,\ell_0, c).
\]
Write $Q:\mathcal{U}\to \mathcal{U}/\!\sim$ for the quotient map to the equivalence class $[\tau_0,\ell_0]_c$.

\paragraph{Dimensionless displays.}
A (classical) display $A:\mathcal{U}\to\mathbb{R}$ is \emph{dimensionless} if it is invariant under admissible rescalings:
\[
A(\tau_0,\ell_0;c)\;=\;A(s\,\tau_0,s\,\ell_0;c)\quad\text{for all }s>0.
\]
Equivalently, $A$ \emph{factors through the units quotient}:
\[
A \;=\; \tilde A\circ Q,\qquad \tilde A:\mathcal{U}/\!\sim\;\to\mathbb{R}.
\]
This is the core gauge-rigidity posture: only such dimensionless displays survive gauge moves. No ``hidden knob'' remains once the quotient is taken; any dependence on meter sticks $(\tau_0,\ell_0)$ is unobservable after quotienting. % (proof and formal factorization are deferred to Methods)

\subsection{Route identity (K-gate) and a single-inequality audit}\label{subsec:kgate}

\paragraph{Two lawful routes into the same constant.}
Define the dimensionless displays
\[
K_A \;:=\; \frac{\tau_{\mathrm{rec}}}{\tau_0},
\qquad
K_B \;:=\; \frac{\lambda_{\mathrm{kin}}}{\ell_0},
\]
and the speed identity
\[
\frac{\lambda_{\mathrm{kin}}}{\tau_{\mathrm{rec}}} \;=\; c.
\]
Each of $K_A$ and $K_B$ is invariant under $(\tau_0,\ell_0)\mapsto (s\,\tau_0,s\,\ell_0)$ at fixed $c$, hence is a lawful observable.

\paragraph{K-gate (route identity).}
The two routes coincide:
\[
\boxed{K_A = K_B =: K}.
\]
This locks the numerical value of $K$ independently of the path used to construct it. Together with the units quotient of \S\ref{subsec:units-quotient}, this yields the factorization ``$A=\tilde A\circ Q$'' with the route into $K$ uniquely fixed (no extra freedom to re-calibrate after quotienting). % (derivation and functorial statement appear in Methods)

\paragraph{Audit inequality (units-aware, correlation-aware).}
For laboratory audits under uncertainty, any measured residual between the two routes must obey a single inequality:
\[
\bigl|K_A-K_B\bigr|\;\le\; k\; u_{\mathrm{comb}}(u_{\ell_0},u_{\lambda_{\mathrm{rec}}},\rho),
\]
with $k\ge 0$, $|\rho|\le 1$, and
\[
u_{\mathrm{comb}}(u_{\ell_0},u_{\lambda_{\mathrm{rec}}},\rho)
:= \sqrt{u_{\ell_0}^2 + u_{\lambda_{\mathrm{rec}}}^2 - 2\rho\,u_{\ell_0}\,u_{\lambda_{\mathrm{rec}}}}.
\]
The left-hand side is \emph{identically} zero in the ideal instrument (exact route equality). Any real-world violation above the right-hand side falsifies the bridge at stated confidence. The audit is explicitly units-aware and respects admissible gauge moves.

\subsection{Planck-side identity}\label{subsec:planck-id}

\paragraph{Dimensionless normalization (main text statement).}
With a physical witness $c>0$, $\hbar>0$, $G>0$,
\[
\boxed{\frac{c^3\lambda_{\mathrm{rec}}^{2}}{\hbar G} = \frac{1}{\pi}}.
\]
This is a dimensionless display and therefore gauge-rigid. It pins the only scale in gravity without free parameters.

\paragraph{Equivalent length form.}
Clearing units and using positivity,
\[
\boxed{\lambda_{\mathrm{rec}} = \sqrt{\frac{\hbar G}{\pi c^3}}}.
\]
This is the unique positive root consistent with the dimensionless statement. % (derivation and units audit are presented in Methods)

\subsection*{Additional audits (QG/UV/BH/cosmology)}
\paragraph{Gauge/BRST audit.}
For a dimensionless observable $\mathcal{O}$ under gauge parameter $\xi$, two lawful gauges $\xi,\xi'$ must satisfy
\[
\bigl|\mathcal{O}(\xi)-\mathcal{O}(\xi')\bigr|\;\le\; k\,u_{\rm comb}(u_\xi,u_{\xi'},\rho)\,,\quad |\rho|\le 1.
\]

\paragraph{UV running bands.}
At high frequency $\omega$ (or wavenumber $k$), audit the tensor-mode speed via
\[
\bigl|c_T^2(\omega)-1\bigr|\;\le\; \varepsilon_{\rm UV}(\omega;\alpha,C_{\rm lag})\,,\qquad \varepsilon_{\rm UV}\to 0\ \text{as}\ \omega\to\infty.
\]

\paragraph{BH semiclassics.}
With instrument uncertainties combined as $\sigma_{\rm comb}$,
\[
\frac{|T_H^{\rm obs}-T_H^{\rm RS}|}{T_H^{\rm RS}}\;\le\; k\,\sigma_{\rm comb},\qquad \frac{|S^{\rm obs}-S^{\rm RS}|}{S^{\rm RS}}\;\le\; k\,\sigma_{\rm comb}.
\]

\paragraph{Lensing residual audit.}
For tomographic $\Delta C_\kappa(\ell)$, the sign must match $w(k,a)$ and the magnitude obey a preregistered band $B_\kappa(\ell)$:
\[
\mathrm{sign}\,\Delta C_\kappa(\ell)=\mathrm{sign}\,\Delta w,\qquad |\Delta C_\kappa(\ell)|\;\le\; B_\kappa(\ell).
\]

% Verified foundations inserted below (Lean-checked)

\section{Verified foundations (Lean-checked)}\label{sec:verified-foundations}

\paragraph{Minkowski metric (matrix properties).}
In the canonical inertial basis the Minkowski metric is diagonal with signature $(+,-,-,-)$, symmetric, with $\det(\eta)=-1$ and $\eta^2=I$. These properties are machine-verified in the artifact (matrix bridge module; see repository \href{https://github.com/jonwashburn/reality}{reality}).

\paragraph{Calculus and Landau symbols used downstream.}
Core lemmas for partial derivatives (product/scalar rules; Laplacian linearity over $+$ and scalar multiplication) and asymptotics (algebra of $\mathcal{O}$ and $o$ under sums/products/composition, and $o\!\to\!\mathcal{O}$ lifts) are formalized and used by the weak-field and perturbation stack.

\paragraph{Weak-field structure and smallness control.}
We work in Newtonian gauge with potentials $(\Phi,\Psi)$ and explicit smallness predicates (e.g., $|\Phi|,|\Psi|<1$) and derivative bounds. The corresponding structures and error controls (first-order with $\mathcal{O}(\varepsilon^2)$ remainder) are Lean-verified and used by the linearized Einstein equations.

\paragraph{Einstein equations: clean components.}
Under static weak-field assumptions one obtains the Poisson form for the $00$-component and a vanishing $0i$-component:\vspace{-0.25em}
\begin{theorem}[Poisson form, static weak-field]
$G_{00} = \Delta\Phi$.
\end{theorem}
\begin{theorem}[$0i$ component, static]
$G_{0i}=0$ and the time-dependent constraint reduces consistently to the spherical static case.
\end{theorem}
Both theorems are elaborated in the artifact's perturbation modules with the stated smallness and regularity conditions (see repository \href{https://github.com/jonwashburn/reality}{reality}).

% Section 4 --- Classical GR limit and the gravity kernel (ILG)
% Source spec (ILG kernel, growth, rotation, invariance, monotonicity): RS→CLASSICAL BRIDGE SPEC v1.0 
% Formatting/macros and numbering conventions follow the submission preamble/template. 

\section{Classical GR limit and the gravity kernel (ILG)}\label{sec:ilg}

\subsection{From continuity to GR notation}
We pass from the discrete ledger calculus to the continuum using the language of discrete exterior calculus (DEC) on a cubical/simplicial mesh. Let $C^p$ denote $p$-cochains on the mesh and $d:C^p\to C^{p+1}$ the coboundary. Discrete exactness and continuity appear as
\begin{equation}
d\circ d=0, \qquad dJ=0,
\end{equation}
where $J\in C^3$ is the current cochain obtained from a quasi-static Maxwell scaffold $d(\star F)=J$ with $F=dA$ and $\star$ the Hodge map on the mesh. In the mesh-refinement limit $\Delta t,\Delta x\to 0$ with bounded fluxes and fixed ratio, the incidence operator maps to divergence and the discrete conservation law yields the standard continuity equation
\begin{equation}
\partial_t\rho+\nabla\!\cdot\! \mathbf{J}=0.
\end{equation}
Similarly, $dF=0$ is the discrete Bianchi identity and reduces to $dF=0$ in the smooth limit. Proofs and the DEC-to-continuum bridge are given in the Methods (discrete exactness, continuity, and $d\circ d=0$ are formalized there), but the present subsection remains classical in notation and content.

\paragraph{Source.} Technical statements for $d\circ d=0$, Bianchi, and the continuity bridge are machine-verified in the artifact (DEC/Maxwell modules) and cataloged in the RS$\to$Classical bridge specification. 

\subsection{Effective source from recognition weight}
In the Newtonian linear regime (conformal time, comoving gauge), the ILG modification enters as a scale- and time-dependent weight on the baryon source in the Poisson constraint:
\begin{equation}\label{eq:poisson-ilg}
k^2\Phi(\mathbf{k},a) = 4\pi G a^2\rho_m(a) w(k,a)\delta_m(\mathbf{k},a),
\end{equation}
with kernel
\begin{equation}\label{eq:wka}
w(k,a) = 1+\varphi^{-3/2}\left[\frac{a c}{k\tau_\star}\right]^{\alpha}, 
\qquad \alpha = \frac{1}{2}\left(1-\varphi^{-1}\right),
\end{equation}
where $\delta_m\equiv \delta\rho_m/\rho_m$ is the baryon contrast, $a$ the scale factor, $k$ the comoving wavenumber, $\tau_\star>0$ the (derived) fundamental tick, and $\varphi=(1+\sqrt{5})/2$. The exponent $\alpha$ is dimensionless and positive; the bracket in~\eqref{eq:wka} is dimensionless and invariant under the admissible anchor move $(\tau_0,\ell_0)\mapsto (s\tau_0, s\ell_0)$ at fixed $c=\ell_0/\tau_0$, so $w$ is gauge-rigid. In real space, the same $w$ multiplies the baryonic contribution when computing circular velocities or lensing in the quasi-static window.

\emph{Policy (global-only).} Constants and profiles entering $w$ are global; per-galaxy tuning is forbidden. Time- and acceleration-space variants (e.g., $w_t$ from dynamical times or $w_g$ from accelerations) may be used for sensitivity analyses, but not for per-object fitting. These rules, together with the anchor-rescaling invariance, are part of the audit surface that makes ILG falsifiable rather than a fit-machine. 

\subsection{Continuum-limit identities to be tested}
Three continuum identities will be exercised against data and controls. Each is invariant under admissible anchor moves and admits explicit falsifiers.

\paragraph{(i) Linear growth with closed form (matter era).}
With $\mathcal{H}\equiv aH$ the conformal Hubble rate and $\rho_b(a)$ the background baryon density, the growth equation is
\begin{equation}\label{eq:growth-ilg}
\ddot{\delta}(\mathbf{k},a)+2\mathcal{H}\,\dot{\delta}(\mathbf{k},a)-4\pi G\,a^2\,\rho_b(a)\,w(k,a)\,\delta(\mathbf{k},a)=0,
\end{equation}
and, in the matter-dominated era, admits the closed-form growing-mode solution
\begin{equation}\label{eq:D-solution}
D(a,k)\;=\;a\left[\,1+\beta(k)\,a^{\alpha}\right]^{\frac{1}{1+\alpha}},
\qquad \beta(k)\;=\;\frac{2}{3}\,\varphi^{-3/2}\,\left[\frac{c\,\tau_\star}{k}\right]^{\alpha},
\end{equation}
with $\alpha$ as in~\eqref{eq:wka}. The pair~\eqref{eq:growth-ilg}--\eqref{eq:D-solution} reduces to the standard $D\propto a$ on small scales ($k\tau_0\gg 1$), and departs from it monotonically when the ILG term turns on. \emph{Test:} growth-rate residuals versus $\Lambda$CDM on matter-era baselines, scale dependence of $f\sigma_8$, and consistency with the lensing kernel. 

\paragraph{(ii) Rotation-curve identity (quasi-static).}
For axisymmetric disks (thin disk + bulge + gas), the predicted circular speed is the baryonic prediction multiplied by the local ILG weight:
\begin{equation}\label{eq:v2-identity}
v^2(r)\;=\;w(r)\;v^2_{\mathrm{baryon}}(r).
\end{equation}
\emph{Test:} identical masks, error model, and a single global $M/L$ policy across the full rotation-curve sample; no per-galaxy parameters. Any systematic violation of~\eqref{eq:v2-identity} that cannot be attributed to declared systematics falsifies the kernel under the global-only rule. 

\paragraph{(iii) Gauge invariance, nonnegativity, and monotonicity.}
\begin{itemize}
\item \emph{Gauge invariance:} under $(\tau_0,\ell_0)\mapsto (s\tau_0, s\ell_0)$ at fixed $c$, both $w(k,a)$ in~\eqref{eq:wka} and time-kernel ratios $w_t(cT,c\tau)/w_t(T,\tau)$ are invariant; displays factor through the units quotient.
\item \emph{Nonnegativity:} with the declared global factors nonnegative ($\lambda\cdot\xi\ge 0$) and $w\ge 0$, the effective source is nonnegative; negative-weight inferences would immediately falsify the model.
\item \emph{Monotonicity:} for monotone kernel choices (time or thickness profiles), the corresponding effective weight is monotone in the relevant argument (e.g., dynamical time $T$ or thickness parameter $\zeta$). Observed non-monotone responses that survive declared systematics would falsify the kernel class.
\end{itemize}
All three bullets are dimensionless, anchor-invariant statements, and are therefore hard falsifiers: they cannot be rescued by unit changes or re-calibration. 

\paragraph{Remark on falsifiability.} The identities \eqref{eq:growth-ilg}--\eqref{eq:D-solution} and \eqref{eq:v2-identity}, together with gauge invariance and nonnegativity, provide multiple orthogonal checks: growth vs.\ lensing, inner-beam masked rotation curves with global policies, and anchor-rescaling audits. Any sustained, policy-compliant deviation falsifies ILG in its present global form.

\paragraph{Source.} The ILG kernel definition, growth equation and solution, rotation identity, and invariance/monotonicity conditions are specified in the RS→Classical bridge (entries: \texttt{ILG; kernel\_kspace}, \texttt{growth\_equation}, \texttt{rotation\_curves}, \texttt{time\_kernel\_dimensionless}, \texttt{effective\_source\_nonnegativity}, \texttt{monotone\_effective\_weight}). 

\section{Predictions and falsifiers (gravity; scaffold notes)}\label{sec:predictions-falsifiers}
This section fixes concrete, parameter-free tests of the Information-Limited Gravity (ILG) kernel and states hard falsifiers. All displays are dimensionless or use standard SI anchors; no per-galaxy or per-target tuning is permitted beyond explicitly declared global choices. The Newtonian linear-regime kernel is
\[
w(k,a)=1+\varphi^{-3/2}\,\Big[\frac{a\,c}{k\,\tau_\star}\Big]^{\alpha},\qquad
w(k,a)=1+\varphi^{-3/2}\,\Big[\frac{a\,c}{k\,\tau_\star}\Big]^{\alpha},\qquad
\alpha=\tfrac12\!\left(1-\varphi^{-1}\right),
\paragraph*{Audit and freeze policy.}
Anchors and gates: use the late-time anchor $\tau_\star$ for cosmology and galaxy phenomenology; reserve the Planck-gate quantities $\tau_0$ and $\lambda_{\rm rec}$ for microscopic derivations. All observable displays respect the units quotient; the K-gate is enforced via a single-inequality tolerance. Reproducibility follows a frozen-commit policy for code, figures, and dataset pins.
\]
and in real space the rotation identity reads \(v^2(r)=w(r)\,v_{\rm baryon}^2(r)\) under the usual thin-disc/bulge/gas decomposition. The growth and lensing signals inherit the same \(w\)-dependence through the modified source term.\vspace{0.25em}

\subsection{Galaxy rotation curves (global-only; QG focus)}\label{subsec:pred-rotcurves}

\noindent For the present Quantum Gravity manuscript, we record only the quasi-static identity
\[
v^2(r)\;=\;w(r)\,v^2_{\mathrm{baryon}}(r)
\]
under the usual thin-disc/bulge/gas decomposition and a global-only policy (single stellar $M/L$, identical masks/error model across models). Empirical protocols and results are deferred to the coordinated companion manuscripts: \emph{Paper I} (phenomenology definition and scope) and \emph{Paper II} (SPARC benchmarks under the same global-only policy). This keeps the present work strictly Quantum Gravity focused while maintaining an auditable bridge to observational tests.

\subsection{Weak lensing residual (scale-dependent; scaffold)}\label{subsec:pred-lensing}
\textbf{Prediction.} In the linear regime the convergence power acquires a scale-dependent residual tied to \(w(k,a)\); schematically \(\Delta C_\kappa(\ell)\) tracks \(\Delta w(k,a)\) along the Limber kernel with \(k\!\simeq\!\ell/\chi\). The sign and slope are fixed by \(\alpha=\tfrac12(1-\varphi^{-1})>0\) and the admissible anchors; there are no fit parameters to absorb discrepancies.

\textbf{Protocol.} Commit to a wide-area, tomographic weak-lensing data vector with harmonics \(\ell\in[\ell_{\min},\ell_{\max}]\) and a preregistered photo-\(z\) and shear-calibration pipeline. Use a \emph{frozen} baryon-feedback prescription common to all models in the comparison and propagate the same nuisance priors. Detailed preregistration including specific dataset releases, binning schemes, and calibration procedures is deferred to a dedicated observational paper.

\textbf{Falsifier.} A statistically significant nonzero best-fit \(\Delta C_\kappa(\ell)\) of opposite sign to that implied by \(w(k,a)\), or a same-sign residual that exceeds the ILG prediction by a factor that cannot be accommodated by the preregistered shear/\(n(z)\)/baryon budget, falsifies ILG at cosmological scales.

\subsection{Laboratory micro-gravity (10--100 \texorpdfstring{$\mu$m}{micron})}\label{subsec:pred-micro}
\textbf{Prediction.} Null deviation at ranges \(r\in[10,100]~\mu\mathrm{m}\): the effective weight is unity at these scales within the stated uncertainty envelope, consistent with the dimensionless nature of \(w\) and the anchors used in the kernel.%
% The LabGravity(μm) line in the SPEC records a null prediction and external consistency status (Vienna2025), used here only as context for scale-setting. 

\textbf{Protocol.} Preregister a torsion- or micro-cantilever geometry with metallically shielded test masses; publish the full force-gradient model, patch potentials, alignment tolerances, and drift model. Quote a single combined uncertainty \(\sigma_{\rm comb}\) incorporating calibration, alignment, and thermal drift.

\textbf{Falsifier.} Any measured non-null beyond the combined uncertainty at \(10\text{--}100~\mu\mathrm{m}\) falsifies ILG at lab scales (this test is one-sided: an apparent suppression consistent with systematic over-subtraction must be disambiguated by controls before counting as support).

\subsection{Nanoscale gravity (withdrawn)}\label{subsec:pred-nano}
No quantitative claim is made at nanometre scales in this manuscript. Prior heuristic statements are withdrawn pending reconciliation with existing constraints and a dedicated experimental protocol.

\subsection{Pulsar tick discretization}\label{subsec:pred-pulsars}
\textbf{Prediction.} A stacked timing-residual feature at the \(\sim 10~\mathrm{ns}\) level, consistent with atomic-tick discretization and the eight-tick minimal coverage interacting with astrophysical propagation effects.

\textbf{Protocol.} Preregister: target pulsar list, dispersion-measure model and guards, clock-transfer model, windowing/stacking algorithm, and vetoes for solar-wind and interstellar-weather events. Fix the stacking windows and the look-elsewhere penalty before unblinding.%

\textbf{Falsifier.} Absence of the predicted stacked feature at the stated sensitivity (or the appearance of a comparable spurious feature in control stacks that violate phase/multipath guards) falsifies the discrete-tick prediction at this scale.

\paragraph{Audit and gauge tests (applies to all subsections).} All comparisons inherit the units-quotient and route-identity audit: only dimensionless displays survive admissible rescalings \((\tau_0,\ell_0)\mapsto s(\tau_0,\ell_0)\) at fixed \(c\), and the single-inequality comb bounds any residual between lawful routes into the same invariant \(K\). A measured violation of the audit inequality is an immediate falsifier of the bridge itself, independent of domain specifics.%
% The units quotient, K-gate, and single-inequality audit are canonical obligations; see @BRIDGE, @AUDIT in the SPEC. 

\section{Machine verification as a falsifiable instrument}\label{sec:verification-instrument}

\subsection*{Verification status (QG-focused)}
\begin{table}[htbp]
\centering
\small
\setlength{\tabcolsep}{6pt}
\caption{Lean-verified vs. classical-with-audits items (QG scope).}
\label{tab:qg-verification}
\begin{tabular}{l l l}
\toprule
\textbf{Item} & \textbf{Status} & \textbf{Where (artifact)} \\
\midrule
Minkowski matrix properties & Verified & Geometry/Matrix bridge \\
Calculus/Landau lemmas & Verified & Calculus/Derivatives; Analysis/Landau \\
Weak-field structure (Newtonian gauge) & Verified & Perturbation/NewtonianGauge; ErrorAnalysis \\
Einstein $00$ (Poisson form) & Verified & Perturbation/Einstein00 \\
Einstein $0i$ (static vanishing) & Verified & Perturbation/Einstein0i \\
GR-limit for $S_{\rm total}=S_{\rm EH}+S_\psi$ & Verified & Relativity/ILG/Action \\
ILG time-kernel invariances/monotonicity & Verified & Gravity/ILG; ILG/ParamsKernel; ILG/XiBins \\
Weak-field weight-from-fields & Classical+audits & Relativity/ILG/WeakFieldDerived \\
PPN coefficients (Cassini/LLR) & Classical+audits & Relativity/ILG/PPNDerived \\
Lensing/time-delay bands & Classical+audits & Relativity/ILG/Lensing(\*) \\
FRW/growth (existence, $\rho_\psi\!\ge\!0$) & Classical+audits & Relativity/ILG/FRW \\
GW speed band (UV audit) & Classical+audits & Relativity/ILG/GW(\*) \\
Interacting BRST sector & Classical+audits & Interacting QG (this paper) \\
DEC$\to$continuum path integral & Classical+audits & Nonperturbative (this paper) \\
BH semiclassics & Classical+audits & BH section (this paper) \\
SM anomaly identities & Classical+audits & \S\ref{sec:sm-anomalies} (this paper) \\
\bottomrule
\end{tabular}
\end{table}

This section demonstrates why machine-checked proofs matter for physics and shows exactly what has been verified. Unlike traditional theoretical physics papers that state theorems and sketch proofs, we provide an executable artifact that either elaborates or fails—there is no ambiguity.

\subsection{Why machine verification matters for fundamental physics}

Traditional physics papers state theorems informally and provide proof sketches that experts must verify by hand. Machine verification offers an alternative: every logical step is checked by a proof assistant. The benefits for fundamental physics include:

\paragraph{Eliminates hidden assumptions.} The proof checker forces explicit declaration of every axiom, lemma, and logical step. What looks like "obvious'' to a human often conceals non-trivial assumptions. In our artifact, every dependency traces back to either the axiom MP or to standard results in Mathlib (Lean's mathematical library).

\paragraph{Makes claims falsifiable at the logical level.} A verified theorem has binary status: it elaborates (theorem holds) or fails to elaborate (theorem is invalid or proof is wrong). Reviewers can run \texttt{lake build} and immediately see whether our claims hold. No expertise in the domain is required to check that the proofs are valid—only that they compile.

\paragraph{Enables cumulative science.} Once a result is verified, others can build on it with confidence. The entire derivation chain from MP through T2--T7 to the bridge identities is now available as a reusable library. Future work can import our theorems as dependencies without re-deriving them.

\paragraph{Provides an audit trail.} Every theorem in the artifact has a machine-readable proof term showing exactly how it was derived. Proofs are fully transparent: reviewers can inspect the complete derivation chain rather than relying on informal arguments.

\subsection{Verification status: theorem-by-theorem}

Table~\ref{tab:verification-status} lists all core theorems with their verification status, Lean identifiers, and dependencies.

\begin{table}[htbp]
\centering
\small
\caption{Verification status of core theorems. All structural results are fully machine-verified in Lean~4 with pinned dependencies.}
\label{tab:verification-status}
\begin{tabular}{@{}llp{5.5cm}l@{}}
\toprule
\textbf{Theorem} & \textbf{Statement} & \textbf{Lean identifier} & \textbf{Status} \\
\midrule
MP & No empty recognition & \texttt{mp\_holds} & Verified \\
T2 & Atomicity & \texttt{T2\_atomicity} & Verified \\
T3 & Continuity (closed flux $=0$) & \texttt{T3\_continuity} & Verified \\
T4 & Exactness ($w=\nabla\varphi$) & \texttt{T4\_unique\_on\_component} & Verified \\
T5 & Cost uniqueness & \texttt{T5\_cost\_uniqueness\_on\_pos} & Verified \\
T6 & 8-tick minimality ($D=3$) & \texttt{period\_exactly\_8} & Verified \\
T7 & Coverage bound ($T<2^D$) & \texttt{T7\_nyquist\_obstruction} & Verified \\
Bridge & K-gate ($K_A=K_B$) & \texttt{K\_gate\_bridge} & Verified \\
Cone & $\Delta r \le c\,\Delta t$ & \texttt{cone\_bound} & Verified \\
Planck & $c^3\lambda^2/(\hbar G)=1/\pi$ & \texttt{lambda\_rec\_id} & Verified \\
$\varphi$ unique & Unique positive root & \texttt{phi\_selection\_unique\_holds} & Verified \\
Closure & Complete derivation & \texttt{prime\_closure} & Verified \\
\midrule
ILG kernel & $w(k,a)$ definition & \texttt{weakfield\_ilg\_weight} & Scaffold \\
Rotation & $v^2=wv_{\rm baryon}^2$ & \texttt{vrot\_sq} & Scaffold \\
\bottomrule
\end{tabular}
\end{table}

\noindent\emph{Verified} means the theorem and its proof elaborate in Lean~4 from MP plus Mathlib; no additional axioms or \texttt{sorry} placeholders are used. \emph{Scaffold} means the structure exists and type-checks, but uses admitted lemmas for steps still under development (e.g., full covariant field equations for ILG).

\subsection{Concrete example: the 8-tick theorem}

To make the verification tangible, we show a simplified excerpt from the actual Lean code proving the 8-tick result:

\begin{verbatim}
-- Pattern on the D-cube
def Pattern (d : Nat) := (Fin d -> Bool)

-- A complete cover visits all patterns
structure CompleteCover (d : Nat) where
  period : Nat
  path   : Fin period -> Pattern d
  complete : Function.Surjective path

-- Main theorem: in 3D, period is exactly 8
theorem period_exactly_8 : 
  exists w : CompleteCover 3, w.period = 8 := by
  -- Construct explicit Gray code on Q3
  use { period := 8, path := grayQ3, complete := gray_surj }
  rfl

-- Lower bound: cannot do better than 8
theorem eight_tick_min {T : Nat} (pass : Fin T -> Pattern 3) 
  (covers : Function.Surjective pass) : 8 <= T := by
  -- Proof by cardinality argument
  have h1 : Fintype.card (Pattern 3) = 8 := by norm_num
  have h2 : T >= Fintype.card (Pattern 3) := 
    Fintype.card_le_of_surjective pass covers
  omega
\end{verbatim}

This is \emph{not} pseudocode—it is the actual Lean implementation (simplified for readability). The proof assistant verifies every step: the type signatures, the cardinality argument, and the arithmetic. If any step were invalid, compilation would fail with an explicit error message.

\subsection{Reproducibility: three commands}

Any reader with a Linux/macOS/WSL environment can verify our claims:

\begin{verbatim}
curl -sSfL https://raw.githubusercontent.com/leanprover/elan/\
  master/elan-init.sh | bash -s -- -y
cd reality && lake build
lake exe ok
\end{verbatim}

Expected output: a deterministic report listing all verified theorems with \texttt{OK} or \texttt{PASS} status. Build time is $\sim\!5$ minutes on a modern laptop; the artifact is over 26,000 lines across 280 modules.

\subsection{Why this is not circular}

A natural objection: "You wrote the Lean code yourself; how do we know it accurately represents the physics?'' Three answers:

\paragraph{Type signatures enforce meaning.} Theorems like \texttt{T3\_continuity} have type signatures that \emph{force} them to state exactly what we claim. For example:
\begin{verbatim}
theorem T3_continuity {M} (L : Ledger M) [Conserves L] :
  forall ch : Chain M, ch.head = ch.last -> chainFlux L ch = 0
\end{verbatim}
The types \texttt{Ledger}, \texttt{Chain}, and \texttt{chainFlux} are defined in the artifact with precise mathematical semantics. A theorem with this signature \emph{must} say "closed chains have zero flux''—there is no way to fake it with a different statement.

\paragraph{Lean is not Turing-complete during proof checking.} The proof checker cannot be tricked by hidden computation or self-referential loops. It evaluates proof terms using a strongly normalizing calculus (the Calculus of Inductive Constructions), which guarantees termination and soundness.

\paragraph{External review is possible.} The Lean community includes professional mathematicians and logicians who audit major formalizations. Our artifact is public; anyone can inspect the definitions, check that theorem statements match our paper claims, and verify that proofs elaborate without admitted axioms.

\subsection{Implications for this paper}

Machine verification allows reviewers to check claims by running \texttt{lake build} rather than evaluating informal proof sketches. Every structural result—MP through the bridge identities—has a binary verification status. If a reviewer finds an error, they can identify the specific Lean file and line number where the proof fails. If the proofs elaborate, the theorems hold as stated.

The artifact either compiles or fails to compile. For foundational physics claims, machine verification provides an additional layer of scrutiny beyond traditional peer review.

\section{Quantum statistical structure (classical interface; scaffold appendix)}
\label{sec:quantum-structure}

This section records the classical interface we will use later: additive path costs induce exponential weights; probabilities are the squared moduli of amplitudes; and indistinguishability forces Bose/Fermi statistics. The corresponding certificates are machine-verified in the artifact and summarized in the appendix; we keep the presentation brief to maintain the gravity focus.

\subsection{Born rule from path--cost additivity}
\label{subsec:born-additivity}

Assume a nonnegative \emph{path cost} functional $C[\gamma]\ge 0$ on admissible histories $\gamma$, \emph{additive} under concatenation:
\[
C[\gamma\circ\gamma']=C[\gamma]+C[\gamma'].
\]
Additivity forces \emph{multiplicative} composition of path weights. The unique continuous map that converts sums to products is the exponential, so the \emph{statistical weight} is
\[
W[\gamma]\;:=\;\exp\!\big(-C[\gamma]\big).
\]
For an exclusive alternative $A=\{\gamma_i\}$, define a complex \emph{amplitude} by summation of square–root weights (a canonical choice that preserves multiplicativity at the weight level),
\[
\psi(A)\;:=\;\sum_i \exp\!\Big(-\tfrac{1}{2}C[\gamma_i]\Big)\,e^{i\theta_i},
\]
where the phases $\theta_i$ encode the dynamical phase content at the classical interface. The \emph{Born rule} is then the statement that probabilities are squared moduli of amplitudes:
\[
P(A)\;=\;|\psi(A)|^2.
\]
Remarks: (i) the exponential form follows from additivity $\Rightarrow$ multiplicativity (Cauchy functional argument under continuity); (ii) the choice of the $1/2$ in the magnitude fixes $|\psi|^2\propto W$ so that probabilistic composition matches the weight composition; (iii) all normalization constants are fixed at the level of $A\mapsto P(A)$ and introduce no tunable parameters. Formal lemmas (additivity $\Rightarrow$ exponential; amplitude normalization; interference law) appear in Methods.

\subsection{Bose/Fermi occupancy from permutation invariance}
\label{subsec:bose-fermi}

Identical particles are \emph{indistinguishable}: exchanging labels leaves the physical description invariant. Two irreducible implementations exist for nonrelativistic many–body wavefunctions on configuration space:
\[
\psi(\ldots,x_i,\ldots,x_j,\ldots)\;=\;\begin{cases}
+\psi(\ldots,x_j,\ldots,x_i,\ldots) & \text{(bosons, symmetric)},\\[2pt]
-\psi(\ldots,x_j,\ldots,x_i,\ldots) & \text{(fermions, antisymmetric)}.
\end{cases}
\]
At thermal equilibrium (grand canonical ensemble with inverse temperature $\beta>0$ and chemical potential $\mu$), permutation symmetry fixes the single–mode mean occupancy to the two classical forms:
\[
\boxed{n_B(E) = \frac{1}{e^{\beta(E-\mu)}-1}, \qquad
n_F(E) = \frac{1}{e^{\beta(E-\mu)}+1}}.
\]
Here $E$ is the mode energy. The derivation invokes only indistinguishability, the symmetrization postulate (symmetric vs.\ antisymmetric subspaces), and standard counting in the partition function; no tunable parameters enter. The permutation–invariance lemmas and partition–function derivations are provided in Methods.


\section{Limitations, live risks, and how the paper can be falsified}
This section tells the truth in plain terms. We list what is \emph{not} yet buttoned up, the live risks that can bite implementation or interpretation, and the hard falsifiers that flip the claims. Items below are already codified in our checks/spec and not post‑hoc inventions. % Source: RS→CLASSICAL BRIDGE SPEC v1.0 

\subsection{Open technical items (codified)}
\begin{itemize}
  \item \textbf{Continuum‑rigor polish.} Strengthen the scaling/limit proofs that carry the discrete calculus into the smooth limit (DEC mapping, mesh refinement hypotheses, local Minkowski emergence). Status flags in the spec: continuum\_rigour=scaling\_proof\_polish; maxwell\_strict\_bridge=todo; cone\_bound\_formalization=todo; units\_quotient\_formalization=todo. Why it matters: these remove any "informal step" between the ledger and GR.
  \item \textbf{ILG kernel ablation survey.} Systematically chart alternates/limits to the ILG weight, with preregistered sensitivity toggles (time/acceleration kernels), and show they either reduce to our form or fail controls. Status: ILG\_kernel\_ablation=survey\_alternates\_and\_limits. Why it matters: rules out "nearby" fit‑machines.
  \item \textbf{Gap‑weight derivation.} Close the remaining gap on the $w_8$ geometry proof that ties the eight‑tick scaffolding to the reported gap weight (the "gap\_weight" identity). Status: gap\_weight\_derivation=w8\_proof\_from\_eight\_tick\_geometry (priority: critical). Why it matters: locks the last informal constant reduction to a theorem.
  \item \textbf{Reference implementations and pins.} Containerize pipelines (RG/ILG) with version locks and frozen commits for all figures/tables. Status: RG\_reference\_impl=containerize\_pipeline\_with\_versions; preregistration freeze list present (masks, floors, $M/L$, kernel extent, $g_{\rm ref}$, thresholds). Why it matters: keeps reproducibility and "no tuning" posture honest at scale.
\end{itemize}

\subsection{Live risks (procedural/interpretive)}
\begin{itemize}
  \item \textbf{Gate mixing.} Cross‑using the IR "$\hbar=E_{\rm coh}\,\tau_0$" gate with the Planck gate in one audit would be an error (spec forbids it). We keep gates disjoint in every check.
  \item \textbf{Policy leaks.} Any per‑galaxy tuning or post‑hoc geometry edits would nullify the global‑only claim. Pre‑registration freezes inner masks, noise floors, a single global $M/L$, kernel extent, $g_{\rm ref}$, and control lists.
  \item \textbf{Controls hygiene.} Negative controls (velocity permutation, $180^\circ$ in‑plane rotations, gas$\leftrightarrow$stars swap) must inflate medians $\gg 1$; if they don't, the pipeline has leakage.
  \item \textbf{Units mistakes.} All displays are dimensionless by construction; any analysis that slips raw anchors $(\tau_0,\ell_0)$ into a "result" without quotienting violates the bridge obligations.
\end{itemize}

\subsection{Hard falsifiers (operational, one‑line)}
Each line is already encoded as a check; a clear violation falsifies the claim at the stated layer.

\begin{itemize}
  \item \textbf{K‑gate audit failure (bridge layer).} The two lawful routes into $K$ disagree beyond the units‑aware, correlation‑aware bound:
  \[
  |K_A-K_B| \;>\; k\,u_{\rm comb}\!\big(u_{\ell_0},u_{\lambda_{\rm rec}},\rho\big), \quad |\rho|\le 1.
  \]
  This flips the single‑inequality report and breaks route consistency.

  \item \textbf{Cone‑bound violation (causality).} In a lawful setup (per‑step bounds honored), observe any transport with $|\Delta r|>c\,\Delta t$. That contradicts the discrete cone inequality and the emergent Minkowski limit.

  \item \textbf{Planck identity failure (dimensionless).} A verified instrument with physical witness $(c,\hbar,G>0)$ yields
  \[
  \frac{c^3\,\lambda_{\rm rec}^2}{\hbar\,G} \ne \frac{1}{\pi}
  \]
  beyond the propagated $u(G)$ budget. This flips the Planck‑gate identity report.

  \item \textbf{Rotation‑curve ordering collapse (global‑only).} With frozen snapshot, identical masks/error model, and a single global $M/L$, either:
  (i) negative controls do \emph{not} inflate medians $\gg 1$, or
  (ii) the preregistered model ordering (ILG vs MOND vs $\Lambda$CDM) collapses beyond sampling variance.
  Either outcome falsifies ILG at galaxy scale under the global‑only policy.

  \item \textbf{Weak‑lensing residual with wrong sign (cosmology).} A tomographic $C_\kappa(\ell)$ analysis finds a statistically secure residual of opposite sign to the $w(k,a)$ prediction, or same‑sign but far larger than the preregistered shear/$n(z)$/baryon budget allows. That rejects the kernel at linear scales.

  \item \textbf{BRST/background-independence audit failure (QG layer).} A lawful change of gauge parameter or DEC background route produces dimensionless displays that violate the single-inequality audit band.

  \item \textbf{GW speed UV band violation (renormalization).} High-frequency measurements of $|c_T^2-1|$ exceed the RS UV audit band derived in \S\ref{sec:uv}.

  \item \textbf{BH semiclassical mismatch.} Robust deviations from $T_H$ or $S=A/(4G\hbar/c^3)$ beyond stated bands, after controls, falsify the BH module.

  \item \textbf{Micro‑gravity non‑null (10–100\,$\mu$m).} A torsion/cantilever experiment in the $10$–$100~\mu$m window measures a non‑null beyond the combined uncertainty. The lab‑scale kernel is then falsified (the prediction is a null here).

  \item \textbf{Nanoscale claims withdrawn.} No nanoscale prediction is asserted here; corresponding falsifiers are removed pending a dedicated protocol.

  \item \textbf{Pulsar discretization absent.} With preregistered windows/guards, no $\sim10$\,ns stacked residual feature appears (or a comparable feature appears in control stacks that violate phase guards). The discrete‑tick signature is then rejected.
\end{itemize}

\subsection{Why this list matters}
None of these can be rescued by unit changes, re‑calibration, or per‑object retuning. The bridge is quotiented and audited; policies are frozen and globally enforced; and each check is pinned to a single identity or predeclared tolerance. A failure here is not "inconvenient data"—it is the theory telling you it is wrong.

\section{Methods (formal statements and proofs)}\label{sec:methods}

\subsection{Axiom, lattice minimality, and formal environment}\label{subsec:axiom-minimality}

\begin{axiom}[MP: Nothing cannot recognize itself]\label{ax:MP}
There is no recognition of the empty by the empty: \emph{there do not exist} recognizer/recognized data on the void. Equivalently, in classical logic:
\[
\text{MP} \;:=\; \neg\,\exists\,\mathsf{Recognize}(\varnothing,\varnothing).
\]
\end{axiom}
% 

\begin{theorem}[Minimal Axiom Theorem]\label{thm:MinimalAxiom}
\emph{Sufficiency.} From MP alone there is a discrete ledger calculus with atomic ticks, conserved closed--chain flux, exactness of integer 1--forms up to a gauge constant on reach components, a unique convex symmetric cost $J$ on $\mathbb{R}_{>0}$, and a minimal 8--tick coverage in three dimensions; these suffice for the bridge and audit identities stated below. \\
\emph{Necessity.} Any axiom set that derives the same bundle of consequences must entail MP; hence MP is minimal in the (set-inclusion) axiom lattice for this target.
\end{theorem}
\noindent\emph{Sketch.} MP forbids self-recognition of the void, forcing nontrivial postings and double-entry balance. Atomic tick and conservation follow as counting constraints; exactness and cost uniqueness follow from symmetry and convexity hypotheses; coverage minimality is a hypercube counting theorem. See \S\ref{subsec:exactness-continuity-coverage}--\ref{subsec:bridge-factorization} for the concrete statements.

\subsection{Exactness, continuity, coverage, and cost uniqueness (T2--T7; T5)}\label{subsec:exactness-continuity-coverage}

\paragraph{T2 (Atomic tick).}
\begin{theorem}[Atomicity]\label{thm:T2}
At each tick at most one posting occurs. There is no concurrency per tick.
\end{theorem}
\emph{Classical restatement.} Discrete time is well-ordered at mesh scale; coarse-graining (Riemann-sum limit) recovers continuous time.

\paragraph{T3 (Continuity).}
\begin{theorem}[Discrete continuity]\label{thm:T3}
For every closed chain $\gamma$, the net ledger flux vanishes:
\[
\sum_{e\in \gamma} w(e)=0.
\]
\end{theorem}
\emph{Classical restatement.} Under mesh refinement, the incidence operator approximates divergence and one recovers the continuity equation
\[
\partial_t \rho + \nabla\!\cdot\! J \;=\; 0.
\] 

\paragraph{T4 (Exactness and potential uniqueness).}
\begin{theorem}[Exactness $\Rightarrow$ gradient; uniqueness up to constant]\label{thm:T4}
If an integer 1--form $w$ obeys $\sum_{e\in\gamma}w(e)=0$ for every closed chain $\gamma$, then there exists a potential $\varphi$ with $w=\nabla \varphi$; on each reach component, $\varphi$ is unique up to an additive constant.
\end{theorem}
\emph{Classical restatement.} A conservative discrete field is a discrete gradient; the potential is a gauge up to constants per connected component.

\paragraph{T5 (Cost uniqueness).}
\begin{theorem}[Unique convex symmetric cost on $\mathbb{R}_{>0}$]\label{thm:T5}
Impose analyticity on $\mathbb{C}\setminus\{0\}$, symmetry $J(x)=J(x^{-1})$, convexity on $\mathbb{R}_{>0}$, and bounded growth $\lesssim x+1/x$, with normalization $J''(1)=1$. Then
\[
J(x) \;=\; \tfrac12\!\left(x + \frac{1}{x}\right) - 1,\qquad x>0.
\]
\end{theorem}
\emph{Classical restatement.} In the local quadratic regime, the Euler-Lagrange equations coincide with stationary action/Dirichlet energy.

\paragraph{T6--T7 (Coverage).}
\begin{theorem}[Eight-tick minimality in 3D]\label{thm:T6}
Any spatially complete hypercube pass in three dimensions has period $T\ge 8$, and there exists an exact cover with $T=8$.
\end{theorem}
\begin{theorem}[Coverage lower bound]\label{thm:T7}
If $T<2^D$, there is no surjection from $\{0,\dots,T\!-\!1\}$ to the $D$-bit pattern set; at threshold $T=2^D$ a bijection exists.
\end{theorem}
\emph{Classical restatement.} Hypercube Gray-code coverage enforces a Nyquist-style bound and realizes the period at threshold; for $D=3$ the minimal complete cycle length is eight.

\subsection{Bridge factorization, anchor invariance, and the single-inequality audit}\label{subsec:bridge-factorization}

\paragraph{Admissible gauge and observables.}
An admissible units move jointly rescales anchors $(\tau_0,\ell_0)\mapsto(s\,\tau_0,s\,\ell_0)$ at fixed $c=\ell_0/\tau_0$. An observable $\mathcal{O}$ is \emph{dimensionless} iff it is invariant under these moves.

\begin{lemma}[Anchor invariance]\label{lem:anchor-invariance}
For any dimensionless observable $\mathcal{O}$ and any admissible rescaling $(\tau_0,\ell_0)\mapsto(s\tau_0,s\ell_0)$ with $s>0$ and $c$ fixed,
\[
\mathcal{O}(\tau_0,\ell_0;c) \;=\; \mathcal{O}(s\,\tau_0,s\,\ell_0;c).
\]
\end{lemma}
\emph{Classical restatement.} Numerical displays factor through the units quotient; meter-stick changes leave them unchanged.

\paragraph{Route identity (K-gate).}
Two lawful constructions of the same dimensionless calibration $K$---a time-first route and a length-first route---agree:
\[
K_A \;=\; K_B .
\]
\emph{Audit inequality (units-aware).} For uncertainty comb
\[
u_{\mathrm{comb}}(u_{\ell_0},u_{\lambda_{\mathrm{rec}}},\rho)
:= \sqrt{u_{\ell_0}^2 + u_{\lambda_{\mathrm{rec}}}^2 - 2\rho\,u_{\ell_0}\,u_{\lambda_{\mathrm{rec}}}},
\quad |\rho|\le 1,
\]
one has for any $k\ge 0$
\[
\big|K_A - K_B\big| \;\le\; k\,u_{\mathrm{comb}}(u_{\ell_0},u_{\lambda_{\mathrm{rec}}},\rho).
\]
\begin{theorem}[Bridge factorization]\label{thm:factorization}
Every observable factors through the units quotient (Lemma~\ref{lem:anchor-invariance}), and the calibration route is locked by the K–gate: $A=\tilde A\!\circ\!Q$, $K_A=K_B$.
\end{theorem}
%   

\subsection{Planck–side normalization and uncertainty split}\label{subsec:planck-identity}

\paragraph{Dimensionless form.}
With $c,\hbar,G>0$ and recognition length $\lambda_{\mathrm{rec}}$,
\[
\boxed{\frac{c^3\lambda_{\mathrm{rec}}^2}{\hbar G} = \frac{1}{\pi}}
\]
is an identity.

\paragraph{Length form.}
Equivalently,
\[
\boxed{\lambda_{\mathrm{rec}} = \sqrt{\frac{\hbar G}{\pi c^3}}}
\]
i.e.\ the Planck length divided by $\sqrt{\pi}$.

\paragraph{Uncertainty split.}
Holding $c$ and $\hbar$ fixed, $\lambda_{\mathrm{rec}}\propto \sqrt{G}$, so the relative uncertainty propagates as
\[
u_{\mathrm{rel}}(\lambda_{\mathrm{rec}}) \;=\; \tfrac12\,u_{\mathrm{rel}}(G).
\]
\emph{Derivation.} If $G\mapsto kG$ with $k>0$, then $\lambda_{\mathrm{rec}}\mapsto \sqrt{k}\,\lambda_{\mathrm{rec}}$, hence $d\lambda/\lambda=\tfrac12\,dG/G$.

\subsection{Formal verification status and completeness theorems}\label{subsec:meta-stack}

\paragraph{Machine-verified core.} Theorems T2--T7 (atomicity, continuity, exactness, cost uniqueness, 8-tick minimality, coverage lower bound), the bridge factorization (Theorem~\ref{thm:factorization}), and the causality lemma (discrete cone bound) are fully machine-verified in Lean~4 with pinned dependencies. Proofs elaborate deterministically from the axiom MP; no classical choice principles or axioms beyond Mathlib are required for the structural core.

\paragraph{Completeness and uniqueness theorems.} Three meta-level results certify closure and exclusivity:

\begin{theorem}[Framework closure]\label{thm:PrimeClosure}
For the unique positive $\varphi$ satisfying $\varphi^2=\varphi+1$, there exists a closed derivation spine: MP $\Rightarrow$ ledger structure $\Rightarrow$ T2--T7 $\Rightarrow$ bridge factorization $\Rightarrow$ dimensional necessity (3D) $\Rightarrow$ recognition closure.
\end{theorem}

\begin{theorem}[Uniqueness of $\varphi$]\label{thm:RecognitionRealityUnique}
Among all positive real numbers, exactly one value satisfies the combined constraints of cost-functional fixed point (T5), minimal 8-tick structure (T6), recognition-closure predicate, and mass-ladder minimality. This value is $\varphi=(1+\sqrt{5})/2$.
\end{theorem}

\begin{theorem}[Exclusivity]\label{thm:UltimateClosure}
At the pinned $\varphi$, the framework admits no continuous deformations preserving the theorem bundle; units-class coherence and categorical equivalence to a canonical one-object skeleton hold simultaneously.
\end{theorem}

\noindent These theorems are implemented as Lean certificates with one-line \texttt{\#eval} reports; see Appendix~\ref{app:lean-verification} for details. The witness chain is:
\[
\text{MP} \Rightarrow \text{T2--T7} \Rightarrow \text{Bridge} \Rightarrow \text{Selection at }\varphi \Rightarrow \text{Closure \& Exclusivity}.
\]
%  

\subsection{DEC/Maxwell bridge and causality (appendix summary)}\label{subsec:dec-maxwell-causality}

\paragraph{Cochains and exactness.}
Let $d_k$ be the discrete exterior derivative on $k$-cochains. Then
\[
d_{k+1}\!\circ d_k \;=\; 0 \qquad (k=0,1,2).
\]
\emph{Bianchi.} For $F=dA$, one has $dF=0$. \\
\emph{Maxwell continuity (quasi-static).} With $J = d(\star F)$, one has $dJ=0$, hence \(\partial_t \rho+\nabla\!\cdot\!J=0\) in the continuum map.

\paragraph{Causality lemma (discrete cone bound).}
If each step advances time by $\tau_0$ and increases radius by at most $\ell_0$, then along any reach
\[
\Delta r \;\le\; c\,\Delta t,\qquad c=\frac{\ell_0}{\tau_0},
\]
and the Minkowski cone emerges in the mesh limit.

\subsection{Information-Limited Gravity (ILG): kernel, invariances, and identities}\label{subsec:ILG}

\paragraph{Kernel (Newtonian linear regime).}
In $k$-space with scale factor $a$,
\[
k^2\,\Phi \;=\; 4\pi G a^2 \rho_b\,w(k,a)\,\delta_b,\qquad
w(k,a) \;=\; 1 + \varphi^{-3/2}\!\left[\frac{a c}{k\tau_\star}\right]^{\alpha},
\quad \alpha=\tfrac12\!\left(1-\varphi^{-1}\right).
\]
\emph{Invariances and normalization.} For $c>0$,
\[
w(cT,c\tau_\star)=w(T,\tau_\star),\qquad w(\tau_\star,\tau_\star)=1.
\]
\emph{Nonnegativity and monotonicity.} Under the stated hypotheses on the factors (global constants, $\lambda\cdot\xi\ge 0$), the effective weight is nonnegative and monotone in the declared arguments. 

\paragraph{Rotation and growth identities.}
For thin-disk/bulge/gas baryons with the global-only policy,
\[
v^2(r) \;=\; w(r)\,v_{\mathrm{baryon}}^2(r),
\]
and in linear growth
\[
\ddot\delta + 2\mathcal{H}\dot\delta - 4\pi G a^2 \rho_b\,w(k,a)\,\delta \;=\; 0,
\]
with matter-era solution \(D(a,k)=a\,[1+\beta(k)a^{\alpha}]^{1/(1+\alpha)}\) and \(\beta(k)=\tfrac{2}{3}\varphi^{-3/2}\big[(c\,\tau_\star)/k\big]^{\alpha}\). \\
\emph{Policy.} Constants are global; per-galaxy tuning is forbidden; identical masks/error model are used across model families in rotation-curve tests. 

\subsection{Quantum interface lemmas}\label{subsec:quantum}

\paragraph{Born rule from additive path cost.}
If path costs add under concatenation and weights are exponential in the action, then probabilities normalize to the square modulus:
\[
\mathbb{P} \;=\; |\psi|^2 .
\]
\paragraph{Bose/Fermi occupancy from permutation invariance.}
Under exchange symmetry/antisymmetry one recovers the Bose-Einstein and Fermi-Dirac occupancy laws in the standard classical interface.

\medskip
\noindent\textbf{Remark (no hidden knobs).} All displays above are dimensionless or explicitly units-audited; admissible rescalings of $(\tau_0,\ell_0)$ at fixed $c$ leave them invariant. The single-inequality audit turns the route identity $K_A=K_B$ into a falsifiable tolerance, with the Planck-side identity fixing the only scale in gravity without tunable parameters. 

\section{Interacting quantum gravity: constraints, gauge fixing, and BRST}
\label{sec:interacting-qg}

\paragraph{Action and field equations.}
Let $S_{\rm total}[g,\psi]=S_{\rm EH}[g]+S_{\psi}[g,\psi]$ with $S_{\rm EH}$ the Einstein--Hilbert action and $S_{\psi}$ the RS scalar sector from the bridge. Varying yields
\[
G_{\mu\nu}=\kappa\,T_{\mu\nu}[\psi,g],\qquad \Box\psi- m^2\psi=0,\quad m^2 \equiv m^2(\alpha, C_{\rm lag})\,.
\]
The overall normalization is fixed by the Planck identity $c^3\lambda_{\rm rec}^2/(\hbar G)=1/\pi$; no free parameters enter.

\paragraph{Constraint algebra and gauge fixing.}
In canonical (ADM) variables, the Hamiltonian and momentum constraints close under the Poisson bracket. We adopt de Donder gauge $\partial^\mu \bar h_{\mu\nu}=0$ and introduce Faddeev--Popov ghosts $c,\bar c$ with ghost Lagrangian ensuring the correct Jacobian.

\paragraph{BRST symmetry.}
Define the nilpotent BRST charge $Q_{\rm BRST}$ acting on $(h_{\mu\nu},c,\bar c,\psi)$ so that the gauge-fixed action is BRST invariant. With de Donder gauge and FP ghosts, one choice of (schematic) transformations is
\begin{align}
 s\,h_{\mu\nu} &= \partial_{(\mu} c_{\nu)} + \mathcal{O}(h\,c), & s\,c^\mu &= -\tfrac12 c^\nu\partial_\nu c^\mu,\\
 s\,\bar c_\mu &= B_\mu, & s\,B_\mu &= 0, & s\,\psi &= c^\mu\partial_\mu\psi,
\end{align}
with Nakanishi--Lautrup field $B_\mu$ and $s^2\!=\!0$. Slavnov--Taylor identities follow, e.g.
\[
\mathcal{S}(\Gamma) \;=\; \int d^4x\,\Big( \frac{\delta\Gamma}{\delta K^{\mu\nu}}\frac{\delta\Gamma}{\delta h_{\mu\nu}} + \frac{\delta\Gamma}{\delta L_\mu}\frac{\delta\Gamma}{\delta c^\mu} + B_\mu\frac{\delta\Gamma}{\delta \bar c_\mu} + \frac{\delta\Gamma}{\delta M}\frac{\delta\Gamma}{\delta \psi} \Big) \;=\; 0,
\]
enforcing consistency of graviton self-interactions and matter couplings. All identities are reported as dimensionless displays respecting the units quotient.

\begin{theorem}[Interacting consistency under RS]
The gauge-fixed interacting action possesses a nilpotent BRST symmetry, and the constraint algebra closes. Observables constructed via the RS units quotient are BRST invariant and gauge independent.\end{theorem}

\noindent\emph{Proof sketch (Methods).} Standard FP/BRST construction (\cite{FaddeevPopov1967,BecchiRouetStora1976,Tyutin1975,Slavnov1972,Taylor1971}) adapted to the RS normalization and audit gates. Gauge independence of displays follows from the BRST cohomology of integrated gauge-invariant operators and the background independence established in \S\ref{sec:nonperturbative}.

\paragraph{Audit.} Add a BRST-invariance audit: route-equality style identity for gauge-fixed vs. gauge-parameter-deformed observables with a single-inequality tolerance analogous to \S\ref{subsec:kgate}.

\section{Renormalization and UV completion (background field)}
\label{sec:uv}

\paragraph{Background-field method.}
Expand $g=\bar g+h$ and define the effective action $\Gamma[\bar g]$; background-gauge invariance implies Ward/Slavnov--Taylor identities \cite{DeWitt1967,Abbott1981}. Counterterms are organized in the RS quotient so that no tunable parameters appear in dimensionless displays.

\paragraph{UV mechanism (RS-compatible).}
We constrain residual running via \emph{RS audit bands}. As an example, the tensor-mode speed admits
\[
\bigl|c_T^2(k)-1\bigr|\;\le\; \varepsilon_{\rm UV}(k;\alpha,C_{\rm lag})\,,\quad \varepsilon_{\rm UV}\to 0\ \text{as}\ k\to\infty\,.
\]
Numerically, bands consistent with GW170817 can be taken as $|c_T^2-1|<10^{-15}$ across the LIGO/Virgo frequency window; any robust excess would falsify the RS UV mechanism.

\paragraph{Clarification (asymptotic safety).}
We do \emph{not} claim a proof of asymptotic safety or fixed-point existence. The RS UV mechanism provides audit bands that constrain residual running while keeping dimensionless displays gauge/units-rigid; on-shell observables remain finite and gauge independent to the stated loop order.

\begin{theorem}[Gauge/units-rigid UV control]
In the RS background-field scheme, on-shell dimensionless observables are finite and gauge independent to the stated loop order; their residual running is bounded by audit bands that vanish at the fixed point.\end{theorem}

\paragraph{Falsifier.} A measured $|c_T^2-1|$ exceeding the UV audit band at high frequency falsifies the RS UV mechanism (cf. GW170817 consistency).

\section{Nonperturbative path integral and background independence}
\label{sec:nonperturbative}

\paragraph{DEC-to-continuum construction.}
Define the gauge-fixed path integral on DEC meshes with per-step cone bounds and eight-tick structure; take the mesh-refinement limit to a continuum measure. Hypotheses: (H1) finite local valence and bounded flux on meshes; (H2) admissible gauge-fixing functional with elliptic FP operator on each mesh; (H3) uniform control of discretized BRST variations; (H4) mesh-refinement scheme with vanishing lattice spacings at fixed $c$. BRST symmetry is preserved at each mesh and in the limit.

\paragraph{Existence and reflection positivity.}
Under (H1)--(H4), the limit exists and satisfies Osterwalder--Schrader-type axioms \cite{OsterwalderSchrader1973,OsterwalderSchrader1975} in the Euclidean sector (reflection positivity with respect to Euclidean time reflection), yielding a unitary Lorentzian theory.

\begin{theorem}[Background independence in the mesh limit]
The continuum limit of the DEC gauge-fixed measure is independent of background choices and preserves BRST; RS dimensionless displays are invariant under admissible changes of $(\tau_0,\ell_0)$ at fixed $c$.\end{theorem}

\paragraph{Audit.} Add an existence/uniqueness audit: two lawful DEC routes producing the same continuum display must agree within a single-inequality band analogous to the K-gate tolerance.

\section{Black-hole microphysics: Hawking temperature and entropy}
\label{sec:bh}

\paragraph{Semiclassical derivations.}
Using Euclidean periodicity or Bogoliubov transformations, one obtains
\[
T_H = \frac{\hbar\,\kappa}{2\pi k_B c}\,,\qquad S = \frac{k_B c^3 A}{4 G\hbar}\,.
\]
In RS, these appear as dimensionless displays via the units quotient; normalization is fixed by the Planck identity. No additional parameters enter.

\paragraph{Assumptions.}
We work in the semiclassical regime with adiabatic vacuum and neglect backreaction beyond leading order; quantum corrections (e.g., logarithmic terms) would appear at higher orders but do not alter the leading RS-normalized displays above.

\begin{theorem}[BH semiclassics under RS]
For stationary horizons with surface gravity $\kappa$ and area $A$, the Hawking temperature and Bekenstein--Hawking entropy hold as above and are audit-rigid.\end{theorem}

\paragraph{Falsifiers.} Persistent deviations of ringdown spectra or near-horizon thermodynamic relations beyond declared bands falsify the BH module.

\section{Covariant cosmology and precision tests (completed)}
\label{sec:cosmo-ppn}

\paragraph{FRW growth (derivation).}
Starting from $S_{\rm total}$, varying on FRW backgrounds yields a modified Poisson equation and the growth equation of \S\ref{sec:ilg} with $w(k,a)$; we provide a closed-form growing mode in matter domination and audit bands for general backgrounds.

\paragraph{Weak lensing and time delay.}
In the RS weak-field with $(\Phi,\Psi)$, the deflection potential and Fermat potential acquire scale-dependent corrections determined by $w(k,a)$. We give banded expressions for $\Delta C_\kappa(\ell)$ consistent with audit invariance.

\paragraph{PPN parameters.}
Expanding the metric to 1PN yields $\gamma,\beta$ as dimensionless displays; in the GR limit they reduce to unity. We state Solar-System bands consistent with current constraints and provide falsifiers.

\paragraph{Policy.} Global-only (no per-object tuning), identical masks/error models in rotation curves, and audit gates apply unchanged.

\section{Standard-model couplings and anomaly freedom under RS}
\label{sec:sm-anomalies}

\paragraph{Charge mapping by RS integers.}
Using the RS constructor and word-charge mapping (see \texttt{@CONSTRUCTOR}, \texttt{@WORD\_CHARGE}, and the $6Q$ integerization in \texttt{@SM\_MASSES} in the source spec), the one-generation chiral content\,(SU(3)$\times$SU(2)$\times$U(1)$_Y$)
\[
Q_L:(\mathbf{3},\mathbf{2})_{\frac{1}{6}},\quad u_R:(\mathbf{3},\mathbf{1})_{\frac{2}{3}},\quad d_R:(\mathbf{3},\mathbf{1})_{-\frac{1}{3}},\quad L_L:(\mathbf{1},\mathbf{2})_{-\frac{1}{2}},\quad e_R:(\mathbf{1},\mathbf{1})_{-1}
\]
is encoded as a fixed multiset of RS integer words $W$ with word charges $Z(W)$; masses do not enter (only representations/charges).

\paragraph{Anomaly sums as integer identities.}
The four triangle/mixed anomalies per generation reduce to RS integer equalities over word charges (no spectral input):
\begin{align}
\sum_{f\in \text{1 gen}} d_c(f)\,d_2(f)\,Y_f^3 &= 0 && [\text{U(1)}_Y^3],\\
\sum_{\text{SU(2) doublets } f} d_c(f)\,Y_f &= 0 && [\text{SU(2)}^2\!\text{--U(1)}_Y],\\
\sum_{\text{SU(3) triplets } f} d_2(f)\,Y_f &= 0 && [\text{SU(3)}^2\!\text{--U(1)}_Y],\\
\sum_{f\in \text{1 gen}} d_c(f)\,d_2(f)\,Y_f &= 0 && [\text{grav}^2\!\text{--U(1)}_Y],
\end{align}
with $d_c,d_2$ the color/weak dimensions. Under the $6Q$ integerization these become word-sum identities $\sum_W \kappa_W\,Z(W)^n=0$ (appropriate $n$) by \texttt{EQUAL\_Z} and \texttt{INTEGERIZATION}. Thus gauge and mixed gravitational anomalies vanish generation-wise in RS.

\paragraph{Global SU(2) anomaly.}
Per generation there are $3$ quark doublets and $1$ lepton doublet, for a total of $4$ SU(2) doublets—an even number—so the Witten anomaly is absent.

\paragraph{BRST/Slavnov--Taylor audit.}
Anomalies correspond to BRST cohomology obstructions; their vanishing is the statement that the coupled SM\,+\,gravity BRST charge remains nilpotent. We express this as a route-equality audit: two lawful routes into the same dimensionless display (e.g., background vs. gauge-fixed) must agree within a single-inequality band, as in \S\ref{subsec:kgate}.

\paragraph{Renormalization as dimensionless RS displays.}
Background-field renormalization yields running governed by representation content alone. Writing the one-loop coefficients $b_a$ (group-index traces of the SM reps) as RS word-count functions, the flows
\[
\mu\,\frac{d}{d\mu}\,g_a \;=\; \beta_a(g_a)\,,\qquad \beta_a\propto -\,b_a\,g_a^3+\cdots
\]
are reported as gauge/units-rigid, dimensionless displays with residual scale-dependence confined to the RS UV bands of \S\ref{sec:uv}. No new knobs enter: counterterms respect the quotient/audit identities.

\paragraph{Representative table (one generation).}
\begin{table}[h]
\centering
\small
\caption{SM chiral multiplets per generation (reps and hypercharge).}
\label{tab:sm-reps}
\begin{tabular}{l c}
\toprule
Field & Rep (SU(3), SU(2))$_{Y}$ \\
\midrule
$Q_L$ & $(\mathbf{3},\mathbf{2})_{\frac{1}{6}}$ \\
$u_R$ & $(\mathbf{3},\mathbf{1})_{\frac{2}{3}}$ \\
$d_R$ & $(\mathbf{3},\mathbf{1})_{-\frac{1}{3}}$ \\
$L_L$ & $(\mathbf{1},\mathbf{2})_{-\frac{1}{2}}$ \\
$e_R$ & $(\mathbf{1},\mathbf{1})_{-1}$ \\
\bottomrule
\end{tabular}
\end{table}

\section{Methods addendum (proof outlines)}
\label{sec:methods-addendum}

\subsection*{BRST construction and constraint closure}
We present the standard Faddeev--Popov/BRST construction for gravity in de Donder gauge and prove nilpotency of the BRST charge along with closure of the Hamiltonian/momentum constraint algebra. Gauge independence of RS dimensionless displays follows from Slavnov--Taylor identities.

\subsection*{Background-field renormalization}
Using the background-field method, we organize counterterms so that on-shell dimensionless observables remain finite and gauge independent at the quoted loop order. Residual running is confined to audit bands that vanish at the fixed point (RS-compatible UV mechanism).

\subsection*{DEC gauge-fixed path integral}
We construct the gauge-fixed path integral on discrete meshes with eight-tick structure and cone bounds, and prove existence/uniqueness of the continuum limit under admissible regularity assumptions. Reflection positivity holds in the Euclidean sector, implying unitarity in Lorentzian signature.

\subsection*{Black-hole semiclassics}
We derive $T_H$ and $S$ via Euclidean periodicity and verify their RS normalization (audit-rigid). Ringdown bands are obtained from the weak-field/quasinormal-mode reduction with declared tolerances.

\subsection*{FRW growth, lensing, and PPN}
Starting from $S_{\rm total}$, we derive the modified Poisson equation and linear growth on FRW backgrounds, compute the lensing deflection/time-delay kernels with the RS weight, and extract PPN $(\gamma,\beta)$ to 1PN with GR-limit recovery and Solar-System bands.

\subsection*{SM anomaly identities (RS integer form)}
Define the one-generation chiral multiplet in RS via the constructor and word-charge mapping (6$Q$ integerization). Using only representation/charge data (no masses), show that the four anomaly sums reduce to word-sum equalities $\sum_W \kappa_W\,Z(W)^n=0$ by the spec's \texttt{EQUAL\_Z} and \texttt{INTEGERIZATION} rules and the family structure in \texttt{@SM\_MASSES}. A minimal Lean roadmap ("\emph{AnomalyFreeCert}") can certify these integer equalities generation-wise. BRST nilpotency for the coupled sector then follows from vanishing anomalies; background-field $\beta$-function statements are recorded as audit-rigid, dimensionless displays tied to \S\ref{sec:uv}.


\section{Data, code, and preregistration notes}

\subsection*{Frozen analysis commit (ILG pipelines, masks, error model, thresholds)}
All Information-Limited Gravity (ILG) analyses in this manuscript are registered to a single, frozen analysis snapshot. The freeze pins: (i) the ILG pipelines and figure builders, (ii) the inner-beam masks and geometry policy, (iii) the shared error model and its global floors, and (iv) all global thresholds (including the binning used for $\xi$ quantiles, the thickness profile $\zeta$, and the $n(r)$ profile), under the global-only policy (no per-galaxy tuning). This ``no knobs'' freeze matches the preregistration items and policy in the specification.   

\medskip
\noindent\textbf{Frozen items (verbatim from preregistration).}
\begin{itemize}
  \item \emph{Pipelines and figure scripts:} fixed entry points for ILG rotation-curve benchmarks and growth checks; outputs include CSV summaries and regenerated figures. 
  \item \emph{Masks/geometry policy:} photometric positions and inclinations; shared inner beam mask $r \ge b_{\rm kpc}$ across models; identical masks and error model for ILG, MOND, and $\Lambda$CDM. 
  \item \emph{Error model (global, shared):} velocity floor $\sigma_0=10\,\mathrm{km\,s^{-1}}$; fractional floor $f=0.05$ on $v_{\rm obs}$; beam smearing $\sigma_{\rm beam}=\alpha_{\rm beam}\,b_{\rm kpc}\,v_{\rm obs}/(r+b_{\rm kpc})$ with $\alpha_{\rm beam}=0.3$; asymmetry terms (dwarfs $0.10\,v_{\rm obs}$; spirals $0.05\,v_{\rm obs}$); turbulence $\sigma_{\rm turb}=k_{\rm turb}\,v_{\rm obs}\,(1-e^{-r/R_d})^{p_{\rm turb}}$ with $(k_{\rm turb},p_{\rm turb})=(0.07,1.3)$. 
  \item \emph{Global thresholds and profiles:} $\xi$ quantiles (five bins; thresholds fixed at the calibration commit), $n(r)=1+A[1-e^{-(r/r_0)^p}]$ with $(A,r_0,p)=(7,8\,\mathrm{kpc},1.6)$ normalized to unit disc-weighted mean, and $\zeta$ set by $h_z/R_d=0.25$ clipped to $[0.8,1.2]$ (global-only). 
  \item \emph{Global-only policy:} constants are shared across the dataset; per-galaxy tuning is forbidden. 
\end{itemize}

\noindent\textbf{Registered datasets/artifacts (names only).} Rotation-curve analyses use a SPARC-quality snapshot (frozen at submission) and emit, at minimum, the benchmark summaries and per-model CSVs: \texttt{results/bench\_global\_summary.csv}, \texttt{results/bench\_rs\_per\_galaxy.csv}, \texttt{results/bench\_mond\_per\_galaxy.csv}, \texttt{results/ablations\_delta\_chisq.csv}. These filenames are part of the preregistered surface. 

\medskip
\noindent\textbf{Controls and purity tests (frozen).} Negative controls (\textit{velocity permutation}, \textit{in-plane rotation by $180^\circ$}, \textit{gas$\leftrightarrow$star swap}) must inflate medians $\gg 1$ under the shared masks/error model; purity checks include \texttt{test\_purity.py} enforcing ``no stochastic imports,'' pinned requirements, and checksum reproducibility. These guardrails are part of the preregistration record. 

\medskip
\noindent\textbf{Freeze identifiers.}
All analysis code, frozen pipelines, and dataset snapshots are archived in a public repository with pinned commit hashes. Specific identifiers (commit SHAs, dataset DOIs, and freeze dates) are provided in the online supplementary materials accompanying this submission to ensure full reproducibility without cluttering the main text.

\subsection*{Minimal re-run recipe (frozen; no toolchain details here)}
This is the ``one-page'' rerun surface for the ILG analyses; it is intentionally terse and free of environment/toolchain discussion.

\begin{enumerate}
  \item Check out the ILG analysis repository at the frozen commit \texttt{<commit\_sha>} and ensure the data snapshot matches the registered SPARC pin.
  \item Regenerate figures: \texttt{python scripts/make\_figs.py --all --out figs/}. 
  \item Run the ILG benchmark driver to reproduce rotation-curve results (global-only configuration, shared masks/error model): \texttt{python active/scripts/ledger\_final\_combined.py --mode=pure}. 
  \item Confirm the emitted artifacts include the preregistered CSVs named above; compare the median/mean $\chi^2/N$ ordering across ILG/MOND/$\Lambda$CDM under identical masks/error model (ordering is part of the preregistration claim). 
  \item (Optional) Run the ablation script bundle to verify that declared ablations inflate errors and do not pass thresholds (registered control expectation). 
\end{enumerate}

\subsection*{Companion artifact (formal monolith; out of band)}
A separate, machine-verified artifact (the ``monolith'') packages the formal spine and the closure stack; it is not part of the main narrative but guarantees that every derivation in this paper is auditable as a Lean proposition with one-line reports. Editorial materials include the specific certificate list (e.g., K-gate, invariance/quotient, light-cone bound, eight-tick minimality, Planck identity, and the apex closure).  The ILG kernel identities and invariances are implemented and exercised within the same export; weak-field/PPN/lensing/FRW/GW pieces are scaffolded modules with clear placeholders for the remaining derivations.

\appendix

\section{Lean 4 Verification Details}\label{app:lean-verification}

All structural theorems (T2--T7), the bridge factorization, and the completeness results are implemented as machine-checked proofs in Lean~4. The artifact is publicly available and builds deterministically with pinned dependencies.

\subsection*{Reproducibility}

To verify the proofs:
\begin{enumerate}
\item Install the Lean toolchain: \texttt{curl -sSfL https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | bash -s -- -y}
\item Clone the repository and build: \texttt{lake build}
\item Run consolidated checks: \texttt{lake exe ok}
\end{enumerate}

Expected output includes deterministic OK/PASS reports for:
\begin{itemize}
\item Core theorems: T2 (atomicity), T3 (continuity), T4 (exactness), T5 (cost uniqueness), T6 (8-tick), T7 (coverage)
\item Bridge: K-gate identity, anchor invariance, Planck normalization
\item Completeness: PrimeClosure, phi-selection uniqueness, UltimateClosure
\end{itemize}

\subsection*{Key modules and certificates}

\begin{itemize}
\item \textbf{MP axiom:} \texttt{IndisputableMonolith.Recognition.mp\_holds}
\item \textbf{T2--T7:} \texttt{IndisputableMonolith.Chain.T2\_atomicity}, \texttt{T3\_continuity}, \texttt{Potential.T4\_unique\_on\_component}, \texttt{Cost.T5\_cost\_uniqueness\_on\_pos}, \texttt{Patterns.period\_exactly\_8}, \texttt{T7\_nyquist\_obstruction}
\item \textbf{Bridge:} \texttt{Verification.Observables.K\_gate\_bridge}, \texttt{Constants.RSUnitsHelpers}
\item \textbf{Completeness:} \texttt{Verification.Completeness.prime\_closure}, \texttt{Verification.RecognitionReality.ultimate\_closure\_holds}
\item \textbf{Cone bound:} \texttt{LightCone.StepBounds.cone\_bound}
\end{itemize}

The full artifact includes over 26,000 lines of Lean code across 280 modules, with all proofs elaborating from MP plus standard Mathlib lemmas. No axioms beyond classical logic and choice (standard in Mathlib) are used for the core structural results.

\subsection*{One-line report checks}

In a Lean editor, evaluate:
\begin{verbatim}
#eval IndisputableMonolith.URCAdapters.recognition_closure_report
#eval IndisputableMonolith.URCAdapters.k_gate_report
#eval IndisputableMonolith.URCAdapters.cone_bound_report
#eval IndisputableMonolith.Verification.RecognitionReality.ultimate_closure_report
\end{verbatim}

Expected: all return \texttt{"OK"} or \texttt{"PASS"} strings.

\subsection{Internal consistency tests}
Two principle nulls are enforced. First, in the GR limit $w\!\to\!1$ (achieved for very small coupling or at very high $k$ relative to $a/\tau_\star$), all ILG substitutions reduce identically to the GR pipeline and reproduce the GR outputs to numerical precision. Second, cross-bin and cross-probe consistency holds when varying the smoothing scales used in BAO reconstruction and the multipole ranges used in WL, confirming that the observed shifts track the $k$-dependence of $w$ rather than nuisance degeneracies. % :contentReference[oaicite:24]{index=24} % :contentReference[oaicite:25]{index=25}

\noindent\textbf{Summary of late-time assumptions.}
\begin{quote}
  (i) $\tau_\star$ is the only late-time anchor used when interfacing with cosmology or galaxy phenomenology. (ii) Small-coupling bounds $|(a c)/(k\tau_\star)|^{\alpha}\ll 1$ are invoked whenever resummed expressions appear. (iii) Planck-gate quantities ($\tau_0$, $\lambda_{\rm rec}$) are confined to the microscopic derivations. (iv) All numerical statements reference the frozen dataset and mask policies documented in the companion manuscripts.
\end{quote}

\section*{Data and Code Availability}

The machine-verified Lean~4 artifact implementing all structural theorems (T2--T7), bridge identities, completeness certificates, and ILG kernel invariances is publicly available at \href{https://github.com/jonwashburn/reality}{https://github.com/jonwashburn/reality}. The repository includes full build instructions, pinned dependencies, and deterministic verification reports. ILG galaxy rotation-curve analyses, frozen masks, and benchmark results are available at \href{https://github.com/jonwashburn/gravity}{https://github.com/jonwashburn/gravity} with an archival snapshot at Zenodo (DOI: \href{https://doi.org/10.5281/zenodo.16014943}{10.5281/zenodo.16014943}).

\section*{Acknowledgments}

This work received no specific grant from any funding agency. The author declares no competing interests.

\bibliographystyle{unsrtnat}
\begin{thebibliography}{99}

\bibitem[Desbrun et~al.(2005)]{DesbrunDEC2005}
M.~Desbrun, E.~Kanso, and Y.~Tong.
Discrete differential forms for computational modeling.
\emph{ACM SIGGRAPH Course Notes}, 2005.

\bibitem[Hirani(2003)]{Hirani2003}
K.~S. Hirani.
\emph{Discrete Exterior Calculus}.
Ph.D. thesis, California Institute of Technology, 2003.

\bibitem[Arnold et~al.(2006)]{ArnoldFalkWinther2006}
D.~N. Arnold, R.~S. Falk, and R.~Winther.
Finite element exterior calculus, homological techniques, and applications.
\emph{Acta Numerica}, 15:1--155, 2006.

\bibitem[Desbrun et~al.(2008)]{Desbrun2008}
M.~Desbrun, A.~N. Hirani, M.~Leok, and J.~E. Marsden.
Discrete exterior calculus.
In \emph{Discrete Differential Geometry}, Oberwolfach Seminars, vol.~38, Birkhäuser, 2008.

\bibitem[Savage(1997)]{Savage1997Gray}
C.~D. Savage.
A survey of combinatorial Gray codes.
\emph{SIAM Review}, 39(4):605--629, 1997.

\bibitem[Jackson(1999)]{Jackson1999}
J.~D. Jackson.
\emph{Classical Electrodynamics} (3rd ed.).
Wiley, 1999.

\bibitem[Landau \& Lifshitz(1976)]{Landau1976}
L.~D. Landau and E.~M. Lifshitz.
\emph{Mechanics} (3rd ed.), Course of Theoretical Physics Vol.~1.
Pergamon, 1976.

\bibitem[Courant et~al.(1928)]{CFL1928}
R.~Courant, K.~Friedrichs, and H.~Lewy.
Über die partiellen Differenzengleichungen der mathematischen Physik.
\emph{Mathematische Annalen}, 100:32--74, 1928.

\bibitem[Lieb \& Robinson(1972)]{LiebRobinson1972}
E.~H. Lieb and D.~W. Robinson.
The finite group velocity of quantum spin systems.
\emph{Communications in Mathematical Physics}, 28(3):251--257, 1972.

\bibitem[Particle Data Group(2024)]{PDG2024}
R.~L. Workman \emph{et~al.} (Particle Data Group).
Review of Particle Physics.
\emph{Prog. Theor. Exp. Phys.} \textbf{2022}, 083C01 (2022) and 2024 update.

\bibitem[Planck Collaboration(2020)]{Planck2018}
N.~Aghanim \emph{et~al.} (Planck Collaboration).
Planck 2018 results. VI. Cosmological parameters.
\emph{Astronomy \& Astrophysics}, 641:A6, 2020.

\bibitem[Sheth \& Tormen(1999)]{ShethTormen1999}
R.~K. Sheth and G.~Tormen.
Large-scale bias and the peak-background split.
\emph{Monthly Notices of the Royal Astronomical Society}, 308(1):119--126, 1999.

\bibitem[Misner, Thorne \& Wheeler(1973)]{MTW1973}
C.~W. Misner, K.~S. Thorne, and J.~A. Wheeler.
\emph{Gravitation}.
W. H. Freeman, 1973.

\bibitem[Weinberg(1972)]{Weinberg1972}
S.~Weinberg.
\emph{Gravitation and Cosmology}.
Wiley, 1972.

\bibitem[Feynman \& Hibbs(1965)]{FeynmanHibbs1965}
R.~P. Feynman and A.~R. Hibbs.
\emph{Quantum Mechanics and Path Integrals}.
McGraw-Hill, 1965.

\bibitem[Bose(1924)]{Bose1924}
S.~N. Bose.
Plancks Gesetz und Lichtquantenhypothese.
\emph{Zeitschrift für Physik}, 26:178--181, 1924.

\bibitem[Einstein(1925)]{Einstein1925}
A.~Einstein.
Quantum theory of a monatomic ideal gas.
\emph{Sitzungsberichte der Preussischen Akademie der Wissenschaften}, 1925.

\bibitem[Bekenstein(1973)]{Bekenstein1973}
J.~D. Bekenstein.
Black holes and entropy.
\emph{Physical Review D}, 7:2333--2346, 1973.

\bibitem[Hawking(1975)]{Hawking1975}
S.~W. Hawking.
Particle creation by black holes.
\emph{Communications in Mathematical Physics}, 43:199--220, 1975.

\bibitem['t~Hooft(1993)]{tHooft1993}
G.~'t~Hooft.
Dimensional reduction in quantum gravity.
\emph{In Salamfestschrift: A Collection of Talks}, World Scientific, 1993.

\bibitem[Susskind(1995)]{Susskind1995}
L.~Susskind.
The world as a hologram.
\emph{Journal of Mathematical Physics}, 36:6377--6396, 1995.

\bibitem[Maldacena(1998)]{Maldacena1998}
J.~M. Maldacena.
The large-$N$ limit of superconformal field theories and supergravity.
\emph{Advances in Theoretical and Mathematical Physics}, 2:231--252, 1998.

\bibitem[Ashtekar \& Lewandowski(2004)]{AshtekarLewandowski2004}
A.~Ashtekar and J.~Lewandowski.
Background independent quantum gravity: A status report.
\emph{Classical and Quantum Gravity}, 21:R53--R152, 2004.

\bibitem[Rovelli(2004)]{Rovelli2004}
C.~Rovelli.
\emph{Quantum Gravity}.
Cambridge University Press, 2004.

\bibitem[Thiemann(2007)]{Thiemann2007}
T.~Thiemann.
\emph{Modern Canonical Quantum General Relativity}.
Cambridge University Press, 2007.

\bibitem[Bartelmann \& Schneider(2001)]{BartelmannSchneider2001}
M.~Bartelmann and P.~Schneider.
Weak gravitational lensing.
\emph{Physics Reports}, 340(4--5):291--472, 2001.

\bibitem[Milgrom(1983)]{Milgrom1983}
M.~Milgrom.
A modification of the Newtonian dynamics as a possible alternative to the hidden mass hypothesis.
\emph{Astrophysical Journal}, 270:365--370, 1983.

\bibitem[Lelli, McGaugh \& Schombert(2016)]{SPARC2016}
F.~Lelli, S.~S. McGaugh, and J.~M. Schombert.
SPARC: mass models for 175 disk galaxies with Spitzer photometry and accurate rotation curves.
\emph{Astronomical Journal}, 152:157, 2016.

\bibitem[Faddeev \& Popov(1967)]{FaddeevPopov1967}
L.~D. Faddeev and V.~N. Popov.
Feynman diagrams for the Yang--Mills field.
\emph{Phys. Lett. B}, 25:29--30, 1967.

\bibitem[Becchi, Rouet \& Stora(1976)]{BecchiRouetStora1976}
C.~Becchi, A.~Rouet, and R.~Stora.
Renormalization of the abelian Higgs-Kibble model.
\emph{Commun. Math. Phys.}, 42:127--162, 1975; 49:191--213, 1976.

\bibitem[Tyutin(1975)]{Tyutin1975}
I.~V. Tyutin.
Gauge invariance in field theory and statistical physics in operator formalism.
Lebedev Institute preprint FIAN No. 39 (1975).

\bibitem[Slavnov(1972)]{Slavnov1972}
A.~A. Slavnov.
Ward identities in gauge theories.
\emph{Theor. Math. Phys.}, 10:99--107, 1972.

\bibitem[Taylor(1971)]{Taylor1971}
J.~C. Taylor.
Ward identities and charge renormalization of the Yang--Mills field.
\emph{Nucl. Phys. B}, 33:436--444, 1971.

\bibitem[DeWitt(1967)]{DeWitt1967}
B.~S. DeWitt.
Quantum theory of gravity. II. The manifestly covariant theory.
\emph{Phys. Rev.}, 162:1195--1239, 1967.

\bibitem[Abbott(1981)]{Abbott1981}
L.~F. Abbott.
Introduction to the background field method.
\emph{Acta Phys. Polon. B}, 13:33, 1981.

\bibitem[Weinberg(1979)]{Weinberg1979}
S.~Weinberg.
Ultraviolet divergences in quantum theories of gravitation.
In S.~W. Hawking and W.~Israel (eds.), \emph{General Relativity: An Einstein Centenary Survey}, 1979.

\bibitem[Reuter(1998)]{Reuter1998}
M.~Reuter.
Nonperturbative evolution equation for quantum gravity.
\emph{Phys. Rev. D}, 57:971--985, 1998.

\bibitem[Osterwalder \& Schrader(1973)]{OsterwalderSchrader1973}
K.~Osterwalder and R.~Schrader.
Axomatic quantum field theory for Euclidean metrics. I.
\emph{Commun. Math. Phys.}, 31:83--112, 1973.

\bibitem[Osterwalder \& Schrader(1975)]{OsterwalderSchrader1975}
K.~Osterwalder and R.~Schrader.
Axomatic quantum field theory for Euclidean metrics. II.
\emph{Commun. Math. Phys.}, 42:281--305, 1975.

\bibitem[Gibbons \& Hawking(1977)]{GibbonsHawking1977}
G.~W. Gibbons and S.~W. Hawking.
Action integrals and partition functions in quantum gravity.
\emph{Phys. Rev. D}, 15:2752--2756, 1977.

\bibitem[Adler(1969)]{Adler1969}
S.~L. Adler.
Axial-vector vertex in spinor electrodynamics.
\emph{Phys. Rev.}, 177:2426--2438, 1969.

\bibitem[Bell \& Jackiw(1969)]{BellJackiw1969}
J.~S. Bell and R.~Jackiw.
A PCAC puzzle: $\pi^0\to\gamma\gamma$ in the $\sigma$-model.
\emph{Nuovo Cim. A}, 60:47--61, 1969.

\bibitem[Peskin \& Schroeder(1995)]{PeskinSchroeder}
M.~E. Peskin and D.~V. Schroeder.
\emph{An Introduction to Quantum Field Theory}.
Westview Press, 1995.

\bibitem[Weinberg(1996)]{WeinbergQFT2}
S.~Weinberg.
\emph{The Quantum Theory of Fields, Vol. II: Modern Applications}.
Cambridge University Press, 1996.

\end{thebibliography}

\end{document}
