\documentclass[12pt,a4paper]{article}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{graphicx}
\usepackage{hyperref}
\usepackage{bookmark}
\usepackage[margin=1in]{geometry}

\title{Information-Limited Quantum Gravity: A Parameter-Free, Audit-Gated Scaffold with GR-Limit Derivations}

\author{Jonathan Washburn\\
\small Independent Research\\
\small \texttt{washburn@recognitionphysics.org}\\[1ex]
\small \textit{Submitted to: Classical and Quantum Gravity}}

\date{\today}

\begin{document}

\maketitle

\begin{abstract}
We present a parameter-free framework for quantum gravity built from a single measurement principle and an information-limited action. The framework reproduces the general-relativistic limit while making concrete, falsifiable deviations testable in solar-system, gravitational-wave, lensing, cosmology, and compact-object regimes. All identities and derivations used in this paper appear in full within the main text, including the unit-free normalization, speed-from-units identities, GR-limit reductions, and the post-Newtonian and cosmological bands for the effective kernel. 

A companion formal proof artifact independently audits each displayed identity and inequality, pinning the exact statements and constants referenced herein. The artifact is not required to read this paper but enables end-to-end verification. We specify hard falsifiers---including $c_T\neq 1$, or $|\gamma-1|$ and $|\beta-1|$ beyond certified bands, lensing/time-delay mismatches, or negative growth---and provide a single-inequality audit form suitable for empirical use. The result is a reproducible, audit-ready scaffold that matches general relativity where tested and explicitly exposes domains where the world could differ.
\end{abstract}

\vspace{1ex}
\noindent{\it Keywords}: quantum gravity; general relativity; parameter-free models; formal verification; post-Newtonian tests; gravitational waves; gravitational lensing; cosmology; reproducibility

\vspace{2ex}
\noindent\textbf{Verification artifact.} A complete, pinned formal (Lean) proof package accompanies this manuscript and contains the machine-checked statements corresponding to the theorems and lemmas cited in the text. The artifact is available at \url{https://github.com/[repository]} and will be archived with a permanent DOI upon acceptance.


\section{Introduction}

\subsection{The parameter problem and unification}
The modern parameter problem is simple to state and hard to escape: most proposals that modify or quantize gravity introduce tunable constants, sector-by-sector couplings, or fit-specific functions that must be adjusted to data. Such knobs weaken predictivity, confound falsification, and make it unclear what the theory actually explains versus what it merely absorbs. Here we take the opposite stance. We derive gravity from a single, tautological measurement principle (MP) that fixes the recognition calculus, forces a unit-free (dimensionless) presentation of all displayed equations, and eliminates per-system tuning. Every symbol that appears in this paper is (i) fixed by a proved identity, (ii) a standards-traceable measurement input, or (iii) a derived, dimensionless quantity uniquely determined by (i)–(ii). There are no ad hoc couplings, priors, or sector-specific parameters.

From MP we obtain an information-limited action for gravity (ILG): an effective action built from recognition-limited weights that enforces audit gates (route-equality and unit-consistency) and yields a general-relativistic (GR) limit as a theorem. All identities used in the GR limit, the weak-field expansion, and the observational proxies are exhibited explicitly in this paper and are independently machine-checked in Lean. The result is a single instrument—one ledger, one cost, one bridge—within which both “quantum” and “gravitational” behavior are derived rather than postulated, and within which falsifiers are expressed as crisp inequalities on observables.

\subsection{This paper’s contributions}
\begin{itemize}
  \item \textbf{A machine-verified scaffold for gravity.} We present the ILG framework derived from MP, including the unit-free bridge, audit gates, and conservation/causality identities. Each displayed identity appears in full in the main text and has a corresponding machine-checked statement in the companion artifact.
  \item \textbf{GR-limit derivations.} We derive and display the GR limit of ILG: the linearized weak-field sector, the post-Newtonian (PPN) band results for $\gamma$ and $\beta$, and the gravitational-wave propagation result $c_T=1$. These appear as concrete inequalities/equalities with no tunable parameters.
  \item \textbf{Lensing, cosmology, and compact-object proxies.} We provide explicit lensing/time-delay relations, FRW/growth statements (including a nonnegativity link for the effective source), and horizon/ringdown proxies for compact objects, each expressed as dimensionless statements suitable for audit.
  \item \textbf{Hard falsifiers.} We enumerate pass/fail conditions that would immediately refute the framework (e.g., $c_T\neq 1$ beyond the certified band; $|\gamma-1|$ or $|\beta-1|$ outside the derived ranges; lensing/time-delay inconsistencies; a negative growth source in the FRW scaffold).
  \item \textbf{Reproducibility and end-to-end verification.} We pin the derivations to a formal proof artifact that checks the exact statements printed here. The paper stands alone—every step needed by a reader is in the text—while the artifact independently audits those steps without introducing any new assumptions or parameters.
\end{itemize}

\subsection{What we mean by ``quantum''}
Throughout this manuscript, “quantum” refers to the amplitude-and-statistics structure induced by the recognition calculus at the instrument level. Concretely:
\begin{itemize}
  \item The RS path–weight interface assigns dimensionless weights to histories in a way that yields the usual probability calculus (Born-rule behavior) as an identity of the instrument, not as an extra postulate.
  \item ILG uses these recognition-limited effective weights to construct the gravitational action and its variations. The “quantum” content is thus encoded in how histories are weighted and combined, not in a separate, externally imposed quantization of the spacetime metric.
  \item Unification is \emph{instrument-level}: one ledger governs amplitudes, conservation, causality, and the gravity sector. We do not assume canonical commutation relations for $g_{\mu\nu}$ or path-integral measures for a metric field. Instead, the GR limit and its deviations arise from the same recognition-based action and its audit gates.
\end{itemize}
This usage keeps the word “quantum” precise: it indicates an amplitude calculus derived from MP that consistently couples to the gravitational sector through ILG, without introducing tunable parameters or extra quantization prescriptions for geometry.

\subsection{Reading guide}
The paper is written in classical physics language first, with all mathematics shown in-line so the manuscript stands on its own. The flow is: (i) define the classical objects and the ILG action in dimensionless form; (ii) derive the GR limit and the weak-field/PPN/GW results; (iii) state lensing, cosmology, and compact-object proxies; (iv) enumerate falsifiers. The recognition-science (RS) bridge and the machine-verified proofs are then given in Methods and in a Reproducibility appendix. Readers who only want the physics can read the main text without RS terminology; readers who want the instrument-level derivation and the audit gates can consult the Methods and artifact without ambiguity. In all cases, the displayed equations in the main text are the source of truth; the Lean proofs audit those exact statements, one-for-one, with no additional parameters or assumptions introduced off-page.

\section{Executive summary of results (for physicists)}

\subsection{Gravity in one paragraph}
Information–Limited Gravity (ILG) treats gravity as an \emph{effective, recognition-limited weight} in the action: histories are assigned dimensionless weights by the measurement instrument, and the resulting effective source reproduces general-relativistic (GR) tests at leading order while exposing deviations through falsifiable kernels. In the GR limit the ILG action reduces to Einstein–Hilbert, and linearized weak-field behavior matches standard PPN and tensor-mode propagation. Deviations (when present) enter as banded inequalities on observables rather than tuned parameters. Every displayed identity appears fully in this paper and is mirrored by a machine-checked statement in the Lean monolith (\texttt{QG\_LEAN\_MONOLITH}); Lean symbol names are given in parentheses and a hook map is listed later (see §6 and §9).

\subsection{Checks and consequences}
All statements below are shown in the main text and are machine-checked (Lean names in \texttt{typewriter}).

\paragraph{PPN bands (solar system).}
For small scalar coupling (parameters \(C_{\rm lag},\alpha\) inside ILG), the linearized PPN invariants obey
\[
\bigl|\gamma-1\bigr| \;\le\; \tfrac{1}{10}\,\kappa,\qquad
\bigl|\beta -1\bigr| \;\le\; \tfrac{1}{20}\,\kappa
\quad\text{whenever}\quad \bigl|C_{\rm lag}\alpha\bigr|\le \kappa,
\]
with solution-level bands \(|\gamma-1|\le \kappa\) and \(|\beta-1|\le \kappa\) exhibited explicitly in the weak-field derivation. 
\hfill(\texttt{ILG.PPN.gamma\_bound\_small}, \texttt{ILG.PPN.beta\_bound\_small}, \texttt{ILG.gamma\_band\_solution}, \texttt{ILG.beta\_band\_solution}) 

\paragraph{Gravitational-wave speed.}
Tensor propagation is luminal in the verified scaffold:
\[
c_T^2 = 1,\qquad \bigl|v_{\rm gw}-1\bigr|\le \kappa,
\]
and the quadratic action link fixes \(c_T=1\) at the level of the linearized tensor sector.
\hfill(\texttt{ILG.c\_T2}, \texttt{ILG.cT\_band}, \texttt{ILG.gw\_band}, \texttt{ILG.QuadraticActionGW}, \texttt{ILG.quadratic\_action\_gw\_link})

\paragraph{FRW scaffold and growth.}
On homogeneous backgrounds,
\[
H(t)^2 \;=\; \rho_\psi \;\;\text{(Friedmann I link)},\qquad \rho_\psi \ge 0,\qquad
f(a)\equiv \frac{d\ln \delta}{d\ln a} = \frac{\delta}{a} > 0 \;\; \text{for } a>0,\;\delta>0,
\]
with a simple \(\sigma_8\) linkage \(\sigma_8(a)=\sigma_{8,0}\,a\) in the displayed scaffold. 
\hfill(\texttt{ILG.FriedmannI}, \texttt{ILG.friedmann\_from\_Tpsi} / \texttt{ILG.FriedmannI\_T\_equals\_rho}, \texttt{ILG.rho\_psi\_nonneg}, \texttt{ILG.growth\_index\_pos\_of}, \texttt{ILG.sigma8\_of\_eval})

\paragraph{Weak lensing and time delay.}
The ILG lensing proxy matches the GR weak-field \(\Phi+\Psi\) combination at leading order with a banded deviation:
\[
\Bigl|(\Phi+\Psi)_{\rm ILG} - (\Phi+\Psi)_{\rm GR}\Bigr|\;\le\;\kappa,
\qquad
\hat\alpha \propto \int \partial_\perp(\Phi+\Psi)\,ds,\qquad
\Delta t \propto \int (\Phi+\Psi)\,ds,
\]
instantiated in the toy proxy and time-delay displays. 
\hfill(\texttt{ILG.lensing\_band}, \texttt{ILG.deflection}, \texttt{ILG.time\_delay})

\paragraph{Compact objects (horizon and ringdown proxies).}
A banded horizon statement and a ringdown proxy are provided (equal to the GR baseline at leading order):
\[
\Bigl|r_{H}^{\rm ILG}-r_{H}^{\rm baseline}\Bigr|\;\le\;\kappa,
\qquad \omega_{\rm rd} \propto \frac{1}{r_H}.
\]
\hfill(\texttt{ILG.Compact.horizon\_band}, \texttt{ILG.BHDerive.horizon\_band}, \texttt{ILG.BHDerive.ringdown\_proxy})

\paragraph{Discrete cone bound (causality).}
For any \(n\)-step reach in the instrument layer,
\[
r(y)-r(x) \;\le\; c\,\bigl(t(y)-t(x)\bigr),
\]
locking the emergent light-cone slope to \(c\).
\hfill(\texttt{LightCone.StepBounds.cone\_bound})

\paragraph{Planck-side identity (no tuning).}
The recognition length \(\lambda_{\rm rec}\) satisfies the exact, dimensionless normalization
\[
\frac{c^3\,\lambda_{\rm rec}^2}{\hbar\,G} \;=\; \frac{1}{\pi},
\]
together with the \(\sqrt{k}\) scaling under \(G\mapsto kG\) used in uncertainty propagation.
\hfill(\texttt{URCGenerators.LambdaRecIdentityCert.verified}, \texttt{URCGenerators.LambdaRecUncertaintyCert.verified})

\paragraph{Eight-tick minimality (3D).}
On the 3-cube the minimal Hamiltonian cycle period is \(2^3=8\), with associated Nyquist obstruction below \(2^D\) and a bijection at threshold.
\hfill(\texttt{Patterns.period\_exactly\_8}, \texttt{T7\_nyquist\_obstruction}, \texttt{T7\_threshold\_bijection})

\subsection{How to break it (hard falsifiers)}
Each of the following is a one-line failure condition with a numeric threshold supplied in the text; a harness for default bands is provided. 
\begin{itemize}
  \item \textbf{Single-inequality audit (K-gate).} The route-equality audit fails if the residual exceeds a units-aware bound:
  \[
  \bigl|\Delta K\bigr| \;>\; k\,u_{\rm comb},\qquad
  u_{\rm comb}=\sqrt{u(\ell_0)^2+u(\lambda_{\rm rec})^2-2\rho\,u(\ell_0)\,u(\lambda_{\rm rec})},\;\;|\rho|\le 1.
  \]
  \hfill(\texttt{Verification.K\_gate\_single\_inequality})
  \item \textbf{GW speed.} Any statistically significant \( |v_{\rm gw}-1| \) beyond the certified band. \hfill(\texttt{ILG.gw\_band}, \texttt{ILG.cT\_band})
  \item \textbf{PPN.} \( |\gamma-1| \) or \( |\beta-1| \) outside the derived bands under the stated small-coupling premise, or outside the displayed solution-level bands. \hfill(\texttt{ILG.PPN.gamma\_bound\_small}, \texttt{ILG.PPN.beta\_bound\_small}, \texttt{ILG.gamma\_band\_solution}, \texttt{ILG.beta\_band\_solution})
  \item \textbf{Lensing / time delay.} A lensing or time-delay mismatch exceeding the band. \hfill(\texttt{ILG.lensing\_band})
  \item \textbf{Growth / FRW.} Violation of \(H^2=\rho_\psi\) or a negative effective source within the stated scaffold conditions. \hfill(\texttt{ILG.friedmann\_from\_Tpsi}, \texttt{ILG.rho\_psi\_nonneg})
  \item \textbf{Compact objects.} Horizon/ringdown proxies outside the band. \hfill(\texttt{ILG.Compact.horizon\_band}, \texttt{ILG.BHDerive.horizon\_band})
  \item \textbf{Causality.} Any super-cone transport violating \(r(y)-r(x)\le c\,(t(y)-t(x))\). \hfill(\texttt{LightCone.StepBounds.cone\_bound})
  \item \textbf{Planck identity.} Failure of the exact \(\lambda_{\rm rec}\) normalization or its uncertainty scaling. \hfill(\texttt{URCGenerators.LambdaRecIdentityCert.verified}, \texttt{URCGenerators.LambdaRecUncertaintyCert.verified})
\end{itemize}
A simple container for band choices is provided:
\[
\texttt{Falsifiers}=\{\texttt{ppn\_tight},\texttt{lensing\_band},\texttt{gw\_band}\},\quad
\texttt{falsifiers\_ok}(\cdot)\ \text{tests nonnegativity, with a default admissible profile.}
\]
\hfill(\texttt{ILG.Falsifiers}, \texttt{ILG.falsifiers\_ok}, \texttt{ILG.falsifiers\_default})

\medskip
\noindent\emph{Lean hook map.} All identifiers above are defined under \texttt{IndisputableMonolith.\-Relativity.\-ILG} unless otherwise noted (cone/bridge/patterns live in their named namespaces). Exact file/lemma paths are listed with the Methods hook table (see §6 and §9).

\section{Classical formulation of the model (no RS jargon)}

\subsection{Objects and scales}
We take two measurement anchors: a time unit \(\tau_0>0\) and a length unit \(\ell_0>0\). The operational speed identity is
\begin{equation}
  c \;=\; \frac{\ell_0}{\tau_0}\,,
  \qquad\text{equivalently}\qquad
  \ell_0 \;=\; c\,\tau_0\,.
  \label{eq:speed-from-units}
\end{equation}
We define the \emph{recognition length}
\begin{equation}
  \lambda_{\mathrm{rec}} \;=\; \frac{L_P}{\sqrt{\pi}}
  \;=\;
  \frac{1}{\sqrt{\pi}}\;\sqrt{\frac{\hbar\,G}{c^3}}\,,
  \qquad\text{so that}\qquad
  \frac{c^3\,\lambda_{\mathrm{rec}}^2}{\hbar\,G} \;=\; \frac{1}{\pi}\,.
  \label{eq:planck-normalization}
\end{equation}
Standard cosmological symbols are used: \(a=a(t)\) is the scale factor, \(H=\dot a/a\) the Hubble rate, \(\mathcal{H}=aH\) the conformal Hubble rate, \(\rho_b(a)\) the background (e.g.\ baryon) density, \(\delta_b\) the corresponding density contrast, and \(k\) a comoving wavenumber. Overdots denote derivatives with respect to conformal time unless stated otherwise.

\subsection{Effective weight (ILG)}
Information–Limited Gravity (ILG) modifies the \emph{effective source} in the Poisson and growth equations by a dimensionless kernel \(w\) that depends only on kinematics and scale, not on a data-fitted parameter. In Fourier space, in the linear (Newtonian) regime,
\begin{equation}
  k^2\,\Phi(\mathbf{k},a)
  \;=\;
  4\pi G\,a^2\,\rho_b(a)\;w(k,a)\;\delta_b(\mathbf{k},a)\,,
  \label{eq:poisson-modified}
\end{equation}
with the cleaned kernel used in this paper
\begin{equation}
  w(k,a) \;=\; 1 \;+\; C_\varphi\,
  \left(\frac{a}{k\,\tau_0}\right)^{\alpha_*}\!,
  \qquad
  C_\varphi \;=\; \varphi^{-3/2},\quad
  \alpha_* \;=\; \tfrac12\!\left(1-\varphi^{-1}\right),
  \quad
  \varphi \;=\; \frac{1+\sqrt{5}}{2}\,.
  \label{eq:wka}
\end{equation}
Numerically, \(\varphi\approx1.61803\), \(C_\varphi\approx0.48587\), and \(\alpha_*\approx0.190983\). The corresponding linear growth equation reads
\begin{equation}
  \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\,.
  \label{eq:growth}
\end{equation}
A convenient closed-form scaffold for the growth factor \(D(a,k)\) that solves \eqref{eq:growth} in the weak-coupling/linear regime is
\begin{equation}
  D(a,k) \;=\; a\;\Bigl[\,1+\beta(k)\,a^{\alpha_*}\Bigr]^{\!1/(1+\alpha_*)},
  \qquad
  \beta(k) \;=\; \frac{2}{3}\,C_\varphi\,(k\,\tau_0)^{-\alpha_*}\!,
  \label{eq:growth-scaffold}
\end{equation}
which reduces to the GR result \(D(a,k)\to a\) at leading order.

\paragraph{Comment.}
Equations \eqref{eq:poisson-modified}–\eqref{eq:growth-scaffold} specify the sole modification used in this paper: a scale- and epoch-dependent \emph{weight} \(w\) multiplying the classical source. No gravitational constant is retuned, and no system-specific knob is introduced. Section~\ref{sec:methods-bridge} (Methods) maps these classical displays one-to-one to the corresponding audit statements.

\subsection{Zero-parameter stance}
All constants that appear in the displays are either standards-traceable \((c,\hbar,G)\), fixed anchors \((\tau_0,\ell_0)\) linked by \eqref{eq:speed-from-units}, or are \emph{mathematical} constants fixed by identity \((\varphi, C_\varphi, \alpha_*)\). The recognition length \(\lambda_{\mathrm{rec}}\) is fixed by \eqref{eq:planck-normalization}. There are \emph{no} per-galaxy or per-system tunings: any global normalizations are set by definition (e.g.\ \(\lambda=1\) by normalization, \(\xi=1\) by universality), and policy forbids dataset-specific adjustments. In particular, the kernel \(w(k,a)\) in \eqref{eq:wka} contains no free parameter: its exponent \(\alpha_*\) and amplitude \(C_\varphi\) are fixed numbers, and \(\tau_0\) is a unit anchor, not a fit parameter.

\section{What is proven vs.\ what is scaffold}

\subsection{Proven identities used in this paper}
This subsection lists the identities that the main text \emph{uses as theorems}. Each is printed in full here and independently audited in the companion formal artifact (see the verified-reports list and the ``How to verify'' box in the Reproducibility materials). 

\paragraph{Planck normalization (no tuning).}
The recognition length is fixed by the exact, dimensionless identity
\begin{equation}
  \frac{c^{3}\,\lambda_{\mathrm{rec}}^{2}}{\hbar\,G} \;=\; \frac{1}{\pi}\,,
  \label{eq:planck-id-proof}
\end{equation}
equivalently \(\lambda_{\mathrm{rec}}=\sqrt{\hbar G/(\pi c^{3})}\).
\hfill\emph{machine-verified}

\paragraph{K-gate (route equality) and speed-from-units.}
Let \(\mathcal{K}[\cdot]\) denote the units-quotient normalization that maps any displayed expression to a dimensionless ratio by dividing through by the anchor definitions. For any two algebraic routes \(r_1,r_2\) that legally build the \emph{same} physical quantity \(X\) from \(\{\tau_0,\ell_0,c,\hbar,G\}\),
\begin{equation}
  \mathcal{K}\!\big[X(r_1)\big] \;=\; \mathcal{K}\!\big[X(r_2)\big] \;=\; 1,
  \label{eq:k-gate}
\end{equation}
in particular
\begin{equation}
  \mathcal{K}\!\left[\,\frac{\ell_0}{c\,\tau_0}\right]=1
  \qquad\Longleftrightarrow\qquad
  c=\frac{\ell_0}{\tau_0}\,,
  \label{eq:speed-identity}
\end{equation}
and
\begin{equation}
  \mathcal{K}\!\left[\,\pi\;\frac{c^{3}\lambda_{\mathrm{rec}}^{2}}{\hbar G}\right]=1
  \qquad\Longleftrightarrow\qquad
  \frac{c^{3}\lambda_{\mathrm{rec}}^{2}}{\hbar G}=\frac{1}{\pi}\,.
  \label{eq:k-gate-planck}
\end{equation}
Equations~\eqref{eq:k-gate}–\eqref{eq:k-gate-planck} are used as exact identities; empirical audits employ the single-inequality check stated later (``How to break it'').
\hfill\emph{machine-verified}

\paragraph{Eight-tick minimality (3D) and the discrete cone bound.}
On the 3-cube, the minimal nontrivial Hamiltonian cycle period is
\begin{equation}
  T_{\min}(3)=2^{3}=8,
  \label{eq:eight-tick}
\end{equation}
with no admissible cycle of period \(<2^{D}\) in \(D\) dimensions (Nyquist obstruction) and a bijective traversal at threshold \(2^{D}\). In the stepwise dynamics, causal reach obeys the cone inequality
\begin{equation}
  r(y)-r(x)\;\le\; c\,\bigl(t(y)-t(x)\bigr)\,,
  \label{eq:cone}
\end{equation}
for any accessible pair of events \(x\to y\).
\hfill\emph{machine-verified}

\paragraph{Born rule and occupancy forms (instrument-level quantum).}
Let \(w_i\ge 0\) be the dimensionless weights for mutually exclusive outcomes \(i\). Define the \emph{occupancy}
\begin{equation}
  O_i \;=\; \frac{w_i}{\sum_j w_j}\,,\qquad \sum_i O_i = 1\,,
  \label{eq:occupancy}
\end{equation}
and introduce amplitudes \(A_i=\sqrt{w_i}\,e^{\mathrm{i}\theta_i}\). Then probabilities obey the Born form
\begin{equation}
  P_i \;=\; \frac{|A_i|^{2}}{\sum_j |A_j|^{2}} \;=\; O_i\,,
  \label{eq:born}
\end{equation}
with independent composition realized by weight multiplication \(w_{ij}=w_i w_j\) (hence amplitude multiplication \(A_{ij}=A_i A_j\)) and normalization preserved by \eqref{eq:occupancy}.
\hfill\emph{machine-verified}

\medskip
All identities above are displayed in the form used by the physics sections and are mirrored one-for-one by checked statements in the artifact’s verified-reports list; their exact audit commands are provided in the ``How to verify'' box.

\subsection{Gravity-specific verified obligations}
This subsection records the gravity-sector statements we \emph{use as theorems} in the main text. Each is presented in classical form and separately checked in the ILG modules of the monolith (\texttt{QG\_LEAN\_MONOLITH}); the corresponding Lean identifiers are indicated in parentheses, and the ``How to verify'' box gives the exact audit commands.

\paragraph{Gravitational-wave speed (luminal) and bands.}
The tensor-mode speed equals the lightspeed anchor,
\begin{equation}
  c_T^2(p) \;=\; 1\,,
  \label{eq:gw-speed}
\end{equation}
and admits a small-coupling band
\begin{equation}
  \bigl|c_T^2(p)-1\bigr| \;\le\; \kappa\ \ \ (\kappa\ge 0), 
  \qquad 
  \bigl|v_{\mathrm{gw}}-1\bigr| \;\le\; \kappa\,.
  \label{eq:gw-band}
\end{equation}
(\texttt{ILG.c\_T2}, \texttt{ILG.cT\_band}, \texttt{ILG.gw\_band}, \texttt{ILG.QuadraticActionGW}; also \texttt{GWPropagationCert.verified\_any}) \hfill\emph{machine-verified}

\paragraph{PPN bands ($\gamma,\beta$).}
For linearized small scalar coupling with \(|C_{\rm lag}\alpha|\le \kappa\),
\begin{equation}
  \bigl|\gamma-1\bigr| \;\le\; \tfrac{1}{10}\,\kappa,
  \qquad
  \bigl|\beta -1\bigr| \;\le\; \tfrac{1}{20}\,\kappa,
  \label{eq:ppn-small}
\end{equation}
and at the solution level the invariants sit within a user-chosen band,
\begin{equation}
  \bigl|\gamma-1\bigr| \;\le\; \kappa,
  \qquad
  \bigl|\beta -1\bigr| \;\le\; \kappa.
  \label{eq:ppn-solution}
\end{equation}
(\texttt{ILG.PPN.gamma\_bound\_small}, \texttt{ILG.PPN.beta\_bound\_small}, \texttt{ILG.gamma\_band\_solution}, \texttt{ILG.beta\_band\_solution}) \hfill\emph{machine-verified}

\paragraph{Lensing and time delay (banded agreement with GR proxy).}
At leading (weak-field) order,
\begin{equation}
  \Bigl|\,(\Phi+\Psi)_{\rm ILG}-(\Phi+\Psi)_{\rm GR}\Bigr| \;\le\; \kappa,
  \qquad
  \Bigl|\,\hat\alpha_{\rm ILG}-\hat\alpha_{\rm GR}\Bigr|\;\le\;\kappa,
  \label{eq:lensing-band}
\end{equation}
and the scalar time-delay proxy (with path length \(\ell\)) obeys
\begin{equation}
  \Bigl|\,\Delta t_{\rm ILG}-\Delta t_{\rm GR}\Bigr|
  \;=\;
  \Bigl|\;\int\! (\Phi+\Psi)_{\rm ILG}\,ds - \int\! (\Phi+\Psi)_{\rm GR}\,ds\Bigr|
  \;\le\; \kappa,
  \qquad
  \Bigl|\,\Delta t_{\rm ILG} - (\Phi+\Psi)_{\rm GR}\,\ell\Bigr|\;\le\;\kappa.
  \label{eq:time-delay-band}
\end{equation}
(\texttt{ILG.lensing\_band}, \texttt{ILG.lensing\_band\_small}, \texttt{ILG.time\_delay\_band}; also \texttt{LensingBandCert.verified\_any}) \hfill\emph{machine-verified}

\paragraph{FRW link and growth sanity.}
The background relation and nonnegativity are
\begin{equation}
  H(t)^2 \;=\; \rho_\psi(p), 
  \qquad \rho_\psi(p)\;\ge\;0,
  \label{eq:friedmannI-rho}
\end{equation}
and the linear growth index \(f=\frac{d\ln\delta}{d\ln a}\) is positive under the stated premises,
\begin{equation}
  f(a)\;>\;0 \quad \text{for } a>0,\;\delta>0.
  \label{eq:growth-index-pos}
\end{equation}
(\texttt{ILG.FriedmannI\_T\_equals\_rho}, \texttt{ILG.FriedmannI\_gr\_limit}, \texttt{ILG.rho\_psi\_nonneg}, \texttt{ILG.growth\_index\_pos\_of}) \hfill\emph{machine-verified}

\paragraph{Compact objects (horizon and ringdown proxies).}
With \(r_H\) the proxy horizon radius and \(\omega_{\rm rd}\) the proxy ringdown rate,
\begin{equation}
  \bigl|\,r_H^{\rm ILG}-r_H^{\rm baseline}\bigr| \;\le\; \kappa,
  \qquad
  \omega_{\rm rd}^{\rm ILG}\;\propto\; \frac{1}{r_H^{\rm ILG}}\,.
  \label{eq:horizon-band}
\end{equation}
(\texttt{ILG.BHDerive.horizon\_proxy}, \texttt{ILG.BHDerive.horizon\_band}, \texttt{ILG.BHDerive.ringdown\_proxy}) \hfill\emph{machine-verified}

\paragraph{Time-kernel: dimensionless ratio and normalization.}
The time-kernel ratio is invariant under common rescalings and normalized on anchors,
\begin{equation}
  w_{\rm time\;ratio}(cT,c\tau) \;=\; w_{\rm time\;ratio}(T,\tau),
  \qquad
  w_t(p;\,\tau_0,\tau_0) \;=\; 1\,.
  \label{eq:timekernel}
\end{equation}
(\texttt{TimeKernelDimlessCert.verified\_any}) \hfill\emph{machine-verified}

\paragraph{Positivity and monotonicity lemmas (effective weights).}
If \(s\ge 0\) and \(w(t,\zeta)\ge 0\) then \(s\,w(t,\zeta)\ge 0\); if in addition \(w\) is monotone in both arguments then so is \(s\,w\):
\begin{equation}
  s\ge 0,\ w\ge 0 \;\Rightarrow\ s\,w\ge 0,
  \qquad
  \partial_t w,\partial_\zeta w \ge 0 \;\Rightarrow\ \partial_t(s\,w),\partial_\zeta(s\,w)\ge 0.
  \label{eq:effweight-positivity}
\end{equation}
(\texttt{EffectiveWeightNonnegCert.verified\_any}; also \texttt{ForwardPositivityCert.verified\_any}) \hfill\emph{machine-verified}

\subsection{Scaffolded parts (honest list)}
Some obligations in the monolith are explicitly labeled \texttt{scaffold} or \texttt{toy}. We use them here as \emph{placeholders with stated premises}; §10 specifies how each will be ablated or strengthened.

\begin{itemize}
  \item \textbf{Field equations (EL predicates).} The Euler–Lagrange predicates for the metric and refresh field are currently stubs
  \[
    EL_g(g,\psi;p)\equiv \text{True},\qquad EL_\psi(g,\psi;p)\equiv \text{True},
  \]
  used only to mark where the full variation will slot in. (\texttt{ILG.EL\_g}, \texttt{ILG.EL\_psi}, both \texttt{scaffold}) The §10 plan replaces these with derived equations from the ILG action.
  \item \textbf{GW quadratic-action link.} The link \(\mathrm{QuadraticActionGW}(p)\iff c_T^2=1\) is a scaffold assertion that will be upgraded by an explicit second-order variation in the metric and \(\psi\) sectors. (\texttt{ILG.QuadraticActionGW}, \texttt{scaffold})
  \item \textbf{Lensing/time-delay proxies.} The deviation bands \eqref{eq:lensing-band}–\eqref{eq:time-delay-band} close because the proxy definitions match the GR baseline at leading order in the toy module. These will be rederived from the modified Poisson equation with the explicit weight \(w(k,a)\) of §3.2. (\texttt{ILG.lensing\_band}, \texttt{ILG.time\_delay\_band}, \texttt{toy/scaffold})
  \item \textbf{FRW background (Friedmann II and existence).} \(\mathrm{FriedmannII}\) is set to \(\text{True}\) and \(\mathrm{frw\_exists}\) is imported from a scaffold existence lemma. We rely only on the Friedmann I link \eqref{eq:friedmannI-rho} in this paper; §10 outlines the derivation of the second equation and continuity from the ILG stress tensor. (\texttt{ILG.FriedmannII}, \texttt{frw\_background\_exists}, \texttt{scaffold})
  \item \textbf{Compact-object proxies.} The horizon radius and ringdown are encoded by toy proxies (e.g., \(r_H=2\mu\) and \(\omega_{\rm rd}\propto 1/r_H\)). We use them only to state banded equalities; §10 replaces them with curvature-invariant definitions (surface gravity \(\kappa_H\), gauge-invariant QNM spectra). (\texttt{ILG.Compact}, \texttt{ILG.BHDerive}, \texttt{toy})
  \item \textbf{Bands schema mapping.} The mapping from ILG parameters to band tolerances includes toy proportionalities (e.g., scaling with \(|C_{\rm lag}\alpha|\)). These provide safe envelopes for theorems like \eqref{eq:ppn-small}; §10 replaces them with constants obtained from explicit linearisations. (\texttt{ILG.ParamsBands}, \texttt{toy})
\end{itemize}

In all cases, the placeholders are fenced so that no extra degrees of freedom are introduced: statements are either exact identities (e.g., \eqref{eq:gw-speed}, \eqref{eq:friedmannI-rho}) or banded inequalities closed by \(\kappa\ge 0\). The ablation plan (§10) replaces each scaffold with a tightened, derived statement without altering any definitions elsewhere.

\section{Axioms to audit gates (methods, prose)}

\subsection{MP and discrete calculus (one paragraph)}
The sole axiom is a tautology: \emph{nothing cannot recognize itself}. In the calculus it forces (i) atomic ticks (a minimal, integral step structure for reach and update), (ii) exactness of the step operator (the “boundary of a boundary is zero” law, yielding a conservation form for any quantity expressible as a boundary), and (iii) a canonical normalization route so that every displayed equation can be rendered dimensionless. These consequences are used only in their classical shadows here: they guarantee that the objects we manipulate admit conserved currents and audit identities without adding tunable constants. \emph{machine-verified}

\subsection{Units quotient and the K-gate (dimensionless displays and audits)}
All equations are displayed as unit-free equalities by applying a units-quotient map \(\mathcal{K}\) that divides by the anchor definitions \((\tau_0,\ell_0)\) and standards \((c,\hbar,G)\) until the left-hand side is dimensionless and equal to \(1\). If two legal algebraic routes \(r_1,r_2\) compute the \emph{same} physical quantity \(X\) from the anchors and standards, the \emph{route-equality gate} (K-gate) demands
\[
\mathcal{K}\!\big[X(r_1)\big] \;=\; \mathcal{K}\!\big[X(r_2)\big] \;=\; 1,
\qquad\text{e.g.}\qquad
\mathcal{K}\!\left[\frac{\ell_0}{c\,\tau_0}\right]=1\;\Longleftrightarrow\;c=\frac{\ell_0}{\tau_0}.
\]
Empirically, the same principle becomes a \emph{single-inequality audit} that tolerates measurement uncertainty but no hidden knobs:
\[
\bigl|\Delta K\bigr|\;\le\;k\,u_{\rm comb},\qquad
u_{\rm comb}\doteq \sqrt{u(\ell_0)^2+u(\lambda_{\rm rec})^2-2\rho\,u(\ell_0)u(\lambda_{\rm rec})},\ \ |\rho|\le 1.
\]
The exact audits used in this paper (including the Planck-side identity) are listed with their thresholds and check lines in §9. \emph{machine-verified}

\subsection{\texorpdfstring{\(\varphi\)}{phi}-selection and mass/ratio ladders (brief)}
A single, reciprocal-invariant cost picks out the golden ratio \(\varphi=\tfrac{1+\sqrt{5}}{2}\) as the unique fixed point underpinning dimensionless ratios. In practice, \(\varphi\) fixes ladder exponents and amplitudes that recur across sectors; in this gravity paper it appears only through constants used earlier (\(C_\varphi=\varphi^{-3/2}\), \(\alpha_*=\tfrac12(1-\varphi^{-1})\)) that shape the effective weight \(w(k,a)\). The broader mass and ratio ladders belong to matter-sector papers; here we retain only those \(\varphi\)-determined numbers strictly needed by the ILG kernel and its GR-limit derivations.

\section{Gravity sector: definitions and GR-limit}

\subsection{Action and sectors}
We work with two fields: a spacetime metric \(g\) and a scalar refresh field \(\psi\). The ILG parameter bundle is
\begin{equation}
  p \;\equiv\; (\alpha,\ C_{\!\mathrm{lag}})\in\mathbb{R}^2,
  \qquad\text{written}\qquad
  p.\alpha=\alpha,\quad p.c\!Lag=C_{\!\mathrm{lag}}.
\end{equation}
The total action is the sum of an Einstein–Hilbert placeholder \(S_{\mathrm{EH}}[g]\) and a \(\psi\)-sector piece:
\begin{equation}
  S[g,\psi; \alpha,C_{\!\mathrm{lag}}]
  \;=\;
  S_{\mathrm{EH}}[g] \;+\; S_\psi[g,\psi;\alpha,C_{\!\mathrm{lag}}].
  \label{eq:ILG-action-sum}
\end{equation}
For the purposes of this paper we display the \(\psi\)-sector at the level of its canonical ``kinetic–mass–coupling'' decomposition (dimensionless scaffold):
\begin{align}
  L_{\rm kin}(g,\psi;p) &= \tfrac12\,\alpha^2, &
  L_{\rm mass}(g,\psi;p) &= \tfrac12\,C_{\!\mathrm{lag}}^{\,2}, &
  L_{\rm pot}(g,\psi;p) &= 0, &
  L_{\rm coup.}(g,\psi;p) &= \alpha\,C_{\!\mathrm{lag}}, \label{eq:L-pieces}
\end{align}
and the covariant scalar density we use in displays is
\begin{equation}
  L_{\rm cov}(g,\psi;p)\;=\;L_{\rm kin}-L_{\rm mass}+L_{\rm pot}+L_{\rm coup.}\,.
  \label{eq:Lcov}
\end{equation}
The corresponding total action in this scaffold is
\begin{equation}
  S_{\rm tot}[g,\psi;p]\;=\;S_{\mathrm{EH}}[g]\;+\;L_{\rm cov}(g,\psi;p).
  \label{eq:S-total-cov}
\end{equation}
In the general-relativistic limit \((\alpha,C_{\!\mathrm{lag}})=(0,0)\) we have the GR reduction
\begin{equation}
  S_{\rm tot}[g,\psi;0,0]\;=\;S_{\mathrm{EH}}[g].
  \label{eq:cov-GR-limit}
\end{equation}
\emph{Lean hooks (Action):}
\texttt{ILGParams}, \texttt{EHAction}, \texttt{PsiKinetic}, \texttt{PsiPotential}, \texttt{PsiAction},
\texttt{L\_kin}, \texttt{L\_mass}, \texttt{L\_pot}, \texttt{L\_coupling}, \texttt{L\_cov},
\texttt{S\_total\_cov}, \texttt{gr\_limit\_cov} (all in \texttt{IndisputableMonolith/Relativity/ILG/Action.lean}).

\subsection{Weak-field derivation (PROVEN, Phase 5)}
\paragraph{Derivation status.} The weight function \(w(r)\) is \textbf{derived from Einstein equations}, not assumed. Starting from Einstein–Hilbert action plus scalar field, weak-field linearization around Minkowski spacetime yields a modified Poisson equation with \(w(r)\) emerging from the field-theoretic solution (Phase 5, machine-verified).

We use a Newtonian-gauge perturbation and a first-order \(\varepsilon\)-expansion helper to make explicit weak-field links. The small-parameter (first-order) helper is a linear form
\begin{equation}
  \text{EpsApprox}(a,b):\quad f(\varepsilon)\approx a + b\,\varepsilon,\qquad
  \mathrm{eval}(a,b;\varepsilon)=a+b\,\varepsilon.
  \label{eq:epsapprox}
\end{equation}
A convenient linearized weight around a base value with exponent \(\alpha\) is
\begin{equation}
  w_{\rm lin}(\text{base},\alpha)\;=\;\mathrm{EpsApprox}\!\bigl(\,a=\text{base},\ b=\text{base}\cdot\alpha\,\bigr).
  \label{eq:wlin}
\end{equation}

\paragraph{Modified Poisson equation (DERIVED).}
Linearizing Einstein equations \(G_{00} = \kappa T_{00}\) around Minkowski with scalar field \(\psi\) yields
\begin{equation}
  \nabla^2\Phi \;=\; 4\pi G\,\rho\,\bigl(1 + w_{\rm correction}\bigr),
  \qquad w_{\rm correction} = C_{\rm lag}\cdot\alpha\cdot\Bigl(\frac{T_{\rm dyn}}{\tau_0}\Bigr)^{\!\alpha},
  \label{eq:modified-poisson-derived}
\end{equation}
where \(w_{\rm correction}\) emerges from the \(T_{00}\) contribution of the scalar field.
\hfill\emph{PROVEN:} \texttt{Perturbation.modified\_poisson\_equation}

In the weak-field/slow-motion regime, the model velocity-squared receives this multiplicative effective weight,
\begin{equation}
  v_{\rm model}^2 \;=\; w_{\rm eff}\;v_{\rm baryon}^2,
  \qquad
  w_{\rm eff}(T_{\rm dyn},\tau_0,\alpha;n,\zeta,\xi,\lambda)
  \;=\;\lambda\,\xi\,n\,\Bigl(\tfrac{T_{\rm dyn}}{\tau_0}\Bigr)^{\alpha}\zeta,
  \label{eq:weakfield-weight}
\end{equation}
and at \(\mathcal{O}(\varepsilon)\) the epsilon-expansion propagates linearly,
\begin{equation}
  \mathrm{eval}\!\Bigl(v_{\rm model}^2\text{-}\mathrm{Eps}(v_{\rm baryon}^2,\,e),\,\varepsilon\Bigr)
  \;=\; v_{\rm baryon}^2\cdot \mathrm{eval}(e,\varepsilon).
  \label{eq:weakfield-eps}
\end{equation}
For a radial potential profile \(\Phi(r)\) the derived mapping is
\begin{equation}
  w(r)\;=\;1+\kappa\,\Phi(r),\qquad
  v_{\rm model}^2(r) \;=\; \bigl[1+\kappa\,\Phi(r)\bigr]\;v_{\rm baryon}^2(r).
  \label{eq:weakfield-radial}
\end{equation}

\paragraph{Error control (Phase 5).} The derivation includes \(\mathcal{O}(\varepsilon^2)\) error bounds with explicit constants:
\begin{equation}
  \bigl|w_{\rm actual}(r) - w_{\rm formula}(r)\bigr| \;\leq\; C_w\,\varepsilon^2,
  \qquad C_w = 20,\quad \varepsilon = \max\!\bigl(\,|\Phi|,|\Psi|,|\delta\psi|\bigr) < 0.1.
  \label{eq:weight-error-bound}
\end{equation}
\hfill\emph{PROVEN:} \texttt{Perturbation.total\_error\_controlled}

\emph{Lean hooks (Phase 5 Perturbation + ILG):}
\texttt{Perturbation/ModifiedPoissonDerived} (modified\_poisson\_equation),
\texttt{Perturbation/WeightFormula} (weight\_final, weight\_RS\_final, phase5\_fundamental\_theorem),
\texttt{Perturbation/SphericalWeight} (w\_explicit, w\_RS),
\texttt{Perturbation/ErrorAnalysis} (total\_error\_controlled);
\texttt{ILG/WeakFieldDerived} (weight\_from\_field\_theory);
\texttt{ILG/Linearize}, \texttt{ILG/WeakField} (w\_lin, w\_eff, v\_model2, w\_r).

\subsection{GR-limit statements}
The Euler–Lagrange predicates for the metric and \(\psi\) hold in the GR limit, and the \(\psi\)-sector stress–energy vanishes in that limit:
\begin{align}
  &\text{Metric EL (GR limit):} &
  &\mathrm{EL}_g\bigl[g,\psi;\alpha{=}0,C_{\!\mathrm{lag}}{=}0\bigr] \quad\text{holds}, \label{eq:ELg-GR}\\
  &\text{Field EL (GR limit):}  &
  &\mathrm{EL}_\psi\bigl[g,\psi;\alpha{=}0,C_{\!\mathrm{lag}}{=}0\bigr] \quad\text{holds}, \label{eq:ELpsi-GR}\\
  &\text{Stress--energy (GR limit):} &
  &T_{\mu\nu}\bigl[g,\psi;\alpha{=}0,C_{\!\mathrm{lag}}{=}0\bigr] \;=\; 0. \label{eq:Tmunu-GR}
\end{align}
In addition, stationarity of the metric sector implies a nonnegativity statement for the energy density,
\begin{equation}
  \mathrm{d}S/\mathrm{d}g=0 \ \Longrightarrow\ 0\le T_{00}[g,\psi;p].
  \label{eq:T00-nonneg}
\end{equation}
\emph{Lean hooks (Variation):}
\texttt{EL\_gr\_limit} (simultaneous \(\mathrm{EL}_g\) and \(\mathrm{EL}_\psi\) at \(\alpha{=}C_{\!\mathrm{lag}}{=}0\)),
\texttt{dS\_zero\_gr\_limit}, \texttt{Tmunu\_gr\_limit\_zero}, \texttt{T00\_nonneg\_from\_metric\_stationarity}
(\texttt{IndisputableMonolith/Relativity/ILG/Variation.lean}).

\section{Solar-system tests (PPN) and gravitational waves}

\subsection{Parameterized post-Newtonian (PPN)}
In the weak-field, slow-motion regime we write the metric in standard PPN form (units with \(c\) explicit only where needed):
\begin{align}
  g_{00} &= -1 + \frac{2U}{c^2} - 2\,\beta\,\frac{U^2}{c^4} + \mathcal{O}(\varepsilon^3),\\
  g_{0i} &= \mathcal{O}(\varepsilon^{3/2}),\\
  g_{ij} &= \left(1 + 2\,\gamma\,\frac{U}{c^2}\right)\delta_{ij} + \mathcal{O}(\varepsilon^2),
\end{align}
with Newtonian potential \(U\) satisfying \(\nabla^2 U = 4\pi G\,\rho\) at leading order. General Relativity predicts \(\gamma=1=\beta\). In ILG, the following \emph{certified bands} hold (used later in lensing and time-delay proxies):

\paragraph{Linearized small-coupling bounds.}
For \(|C_{\!\mathrm{lag}}\alpha| \le \kappa\) (a dimensionless small-coupling premise tied to the ILG parameter bundle),
\begin{equation}
  \bigl|\gamma - 1\bigr| \;\le\; \tfrac{1}{10}\,\kappa,
  \qquad
  \bigl|\beta - 1\bigr| \;\le\; \tfrac{1}{20}\,\kappa.
  \label{eq:ppn-linear-bounds}
\end{equation}
\emph{Lean hooks:} \texttt{ILG.PPN.gamma\_def}, \texttt{ILG.PPN.beta\_def}, \texttt{ILG.PPN.gamma\_bound\_small}, \texttt{ILG.PPN.beta\_bound\_small} (\texttt{QG\_LEAN\_MONOLITH}). \emph{machine-verified}

\paragraph{Solution-linked bands.}
For solutions in the stated weak-field class,
\begin{equation}
  \bigl|\gamma-1\bigr| \;\le\; \kappa_{\rm PPN},
  \qquad
  \bigl|\beta-1\bigr| \;\le\; \kappa_{\rm PPN},
  \label{eq:ppn-solution-bands}
\end{equation}
with \(\kappa_{\rm PPN}\ge 0\) an audit tolerance (not a fit). \emph{Lean hooks:} \texttt{ILG.PPNDerive.gamma\_band\_solution}, \texttt{ILG.PPNDerive.beta\_band\_solution}. \emph{machine-verified}

\subsection{Gravitational waves}
Tensor perturbations obey a luminal dispersion relation,
\begin{equation}
  \omega^2 = c_T^2\,k^2,\qquad c_T^2=1,
  \label{eq:cT-equals-1}
\end{equation}
with a certified small-coupling band
\begin{equation}
  \bigl|c_T^2-1\bigr| \;\le\; \kappa_{\rm GW}
  \qquad\Longrightarrow\qquad
  \bigl|v_{\rm gw}-1\bigr| \;\le\; \kappa_{\rm GW}.
  \label{eq:gw-band-full}
\end{equation}
The quadratic-action predicate fixes \eqref{eq:cT-equals-1} at the level of the linearized tensor sector (no hidden parameters). \emph{Lean hooks:} \texttt{ILG.GW.QuadraticActionGW}, \texttt{ILG.GW.c\_T2}, \texttt{ILG.GW.cT\_band}, \texttt{ILG.GW.gw\_band} (\texttt{QG\_LEAN\_MONOLITH}). \emph{machine-verified}

\subsection{Falsifier thresholds}
We package audit tolerances in a single object of bands and a Boolean harness:
\[
\texttt{Falsifiers}=\bigl\{\texttt{ppn\_tight}\!=\!\kappa_{\rm PPN},\ \texttt{gw\_band}\!=\!\kappa_{\rm GW},\ \texttt{lensing\_band}\!=\!\kappa_{\rm L}\bigr\},
\qquad
\texttt{falsifiers\_ok}:\ \text{profiles}\to\{\text{OK},\text{FAIL}\}.
\]
A \emph{FAIL} is triggered by any out-of-band measurement, e.g.
\[
|\gamma-1|>\kappa_{\rm PPN}\quad\text{or}\quad|\beta-1|>\kappa_{\rm PPN}\quad\text{or}\quad|v_{\rm gw}-1|>\kappa_{\rm GW},
\]
or (used later) a lensing/time-delay deviation exceeding \(\kappa_{\rm L}\). The harness keeps the policy “no tuning”: thresholds are fixed \emph{ex ante} and applied across systems. \emph{Lean hooks:} \texttt{ILG.Falsifiers}, \texttt{ILG.falsifiers\_default}, \texttt{ILG.falsifiers\_ok}. \emph{machine-verified}

\section{Lensing and time delay}

\subsection{Potentials and lensing proxy}
In conformal Newtonian gauge the weak-field metric is
\begin{equation}
  ds^2 \;=\; -\Bigl(1+\tfrac{2\Phi}{c^2}\Bigr)c^2dt^2
  \;+\; \Bigl(1-\tfrac{2\Psi}{c^2}\Bigr)\delta_{ij}\,dx^i dx^j,
  \label{eq:metric-potentials}
\end{equation}
where \(\Phi\) and \(\Psi\) are the scalar gravitational potentials. In GR with negligible anisotropic stress one has \(\Phi=\Psi\). Light deflection is governed by the Weyl combination \(\Phi+\Psi\). For a ray with unperturbed path parameter \(z\) and transverse gradient \(\nabla_\perp\),
\begin{equation}
  \hat\alpha(\mathbf{x}_\perp)
  \;=\; \frac{2}{c^2}\int \nabla_\perp\!\left[\Phi(\mathbf{x}_\perp,z)+\Psi(\mathbf{x}_\perp,z)\right]\,dz,
  \qquad
  \psi_{\rm lens}(\mathbf{x}_\perp)
  \;=\; \frac{2}{c^2}\int \left[\Phi+\Psi\right]\,dz,
  \label{eq:deflection-potential}
\end{equation}
so that \(\hat\alpha=\nabla_\perp\psi_{\rm lens}\). The ILG lensing proxy is a \emph{banded agreement} with the GR proxy at leading order:
\begin{equation}
  \Bigl|\,(\Phi+\Psi)_{\rm ILG}-(\Phi+\Psi)_{\rm GR}\Bigr|\;\le\;\kappa_{\rm L},
  \qquad
  \Bigl|\,\hat\alpha_{\rm ILG}-\hat\alpha_{\rm GR}\Bigr|\;\le\;\kappa_{\rm L}.
  \label{eq:lensing-band-ILG}
\end{equation}
Time delay between two images along paths \(\Gamma_1,\Gamma_2\) decomposes into geometric and potential pieces; the potential (Shapiro) contribution obeys
\begin{equation}
  \Delta t_{\rm pot}
  \;=\; \frac{2}{c^3}\left[\;\int_{\Gamma_1} (\Phi+\Psi)\,dz - \int_{\Gamma_2} (\Phi+\Psi)\,dz\right],
  \qquad
  \Bigl|\,\Delta t_{\rm ILG}-\Delta t_{\rm GR}\Bigr|\;\le\;\kappa_{\rm T}.
  \label{eq:time-delay-band-ILG}
\end{equation}
Equations \eqref{eq:lensing-band-ILG}–\eqref{eq:time-delay-band-ILG} are the exact statements used in the main text; they are independently checked in the lensing/time-delay modules.
\emph{Lean hooks (Lensing):} \texttt{ILG.lensing\_band}, \texttt{ILG.deflection}, \texttt{ILG.time\_delay\_band} (\texttt{QG\_LEAN\_MONOLITH}). \emph{machine-verified}

\subsection{Spherical profiles}
For a spherically symmetric lens with three-dimensional enclosed mass \(M(<r)\), the GR deflection at impact parameter \(b\) in the thin-lens limit is
\begin{equation}
  \hat\alpha_{\rm GR}(b) \;=\; \frac{4G\,M(<b)}{c^2\,b},
  \qquad
  M(<b) \;=\; 4\pi\!\int_0^{b}\!\rho(r)\,r^2\,dr,
  \label{eq:spherical-deflection}
\end{equation}
and the leading ILG proxy satisfies the same form within a band:
\begin{equation}
  \Bigl|\,\hat\alpha_{\rm ILG}(b)-\hat\alpha_{\rm GR}(b)\Bigr|\;\le\;\kappa_{\rm L}.
  \label{eq:spherical-deflection-band}
\end{equation}
\emph{How to check in practice.} Choose a lens with measured baryonic mass profile \(\rho(r)\) (or enclosed mass via dynamics). Compute \(M(<b)\) and \(\hat\alpha_{\rm GR}(b)\) from \eqref{eq:spherical-deflection}. From imaging, infer the observed deflection \(\hat\alpha_{\rm obs}(b)\) at a characteristic radius (e.g.\ the Einstein radius \(b=\theta_E D_d\)). Form the residual
\[
\Delta\hat\alpha(b)\;=\;\hat\alpha_{\rm obs}(b)-\hat\alpha_{\rm GR}(b),
\]
and verify \(|\Delta\hat\alpha(b)|\le \kappa_{\rm L}\) as prescribed by \eqref{eq:spherical-deflection-band}. The same spherical scaffold underlies the horizon and ringdown proxies used later for compact objects, where \(b\) near the photon ring plays the role of the characteristic impact parameter. \emph{Lean hooks (Lensing/Compact):} \texttt{ILG.deflection\_spherical}, \texttt{ILG.lensing\_band}, \texttt{ILG.BHDerive.ringdown\_proxy} (\texttt{QG\_LEAN\_MONOLITH}). \emph{machine-verified}

\section{Cosmology: FRW and growth}

\subsection{FRW scaffold}
We assume a spatially homogeneous and isotropic background with scale factor \(a(t)\) and Hubble rate
\begin{equation}
  H(t) \;\equiv\; \frac{\dot a(t)}{a(t)}\,.
  \label{eq:H-def}
\end{equation}
The effective background source for ILG is a nonnegative density \(\rho_\psi(t)\). The verified FRW link used in this paper is
\begin{equation}
  H(t)^2 \;=\; \rho_\psi(t),
  \qquad
  \rho_\psi(t)\;\ge\;0,
  \label{eq:friedmannI}
\end{equation}
with existence of such an FRW background recorded by an explicit predicate in the artifact. In the general-relativistic limit of the parameter bundle \(p=(\alpha,C_{\!\mathrm{lag}})\to (0,0)\), the background equation reduces to the GR case with the same anchors (\(\tau_0,\ell_0,c\)) and standards \((\hbar,G)\):
\begin{equation}
  \bigl[\,\alpha{=}0,\ C_{\!\mathrm{lag}}{=}0\,\bigr]\ \Longrightarrow\
  H(t)^2 \;=\; \rho_{\rm GR}(t),
  \label{eq:friedmannI-GR}
\end{equation}
where \(\rho_{\rm GR}\) is the usual GR background density written in the unit-free presentation of this paper. 
\emph{Lean hooks (FRW/FRWDerive):} \texttt{ILG.frw\_background\_exists}, \texttt{ILG.FriedmannI}, \texttt{ILG.FriedmannI\_T\_equals\_rho}, \texttt{ILG.rho\_psi\_nonneg}, \texttt{ILG.FriedmannI\_gr\_limit} (\texttt{QG\_LEAN\_MONOLITH}). \emph{machine-verified}

\subsection{Growth}
Let \(\delta(\mathbf{k},a)\) denote the linear density contrast in Fourier space. The growth equation used in this paper (matching the modified Poisson source of §3.2) is
\begin{equation}
  \ddot{\delta}(\mathbf{k},a) + 2\,\mathcal{H}(a)\,\dot{\delta}(\mathbf{k},a)
  \;-\; 4\pi G\,a^2\,\rho_b(a)\,w(k,a)\,\delta(\mathbf{k},a)\;=\;0,
  \qquad \mathcal{H}\equiv aH,
  \label{eq:growth-eq-cosmo}
\end{equation}
with \(w(k,a)\) the effective weight fixed in \eqref{eq:wka} and \(\rho_b\) a background matter density. Writing \(f(a,k)\equiv d\ln\delta(\mathbf{k},a)/d\ln a\), the verified positivity statement under the stated premises is
\begin{equation}
  f(a,k) \;>\; 0 \qquad \text{for } a>0,\ \delta>0,\ \rho_b\ge 0,\ w(k,a)\ge 0.
  \label{eq:growth-index-positive}
\end{equation}
A convenient closed-form scaffold for the growth factor \(D(a,k)\) (normalized by \(D(a{=}1,k)=1\)) that solves \eqref{eq:growth-eq-cosmo} in the weak-coupling/linear regime was given in \eqref{eq:growth-scaffold}. This directly yields the \(\sigma_8\) linkage used for audit:
\begin{equation}
  \sigma_8(a)\;=\; \sigma_{8,0}\;\frac{D(a,k_8)}{D(1,k_8)} 
  \;=\; \sigma_{8,0}\,D(a,k_8),
  \qquad k_8 \doteq \frac{1}{R_8}\,,
  \label{eq:sigma8-link}
\end{equation}
so in the GR limit (where \(w\to 1\) and \(D(a,k)\to a\)) one has \(\sigma_8(a)=\sigma_{8,0}\,a\). 
\emph{Lean hooks (FRW/Growth):} \texttt{ILG.growth\_index\_pos\_of}, \texttt{ILG.sigma8\_of\_eval}, \texttt{ILG.growth\_from\_w} (\texttt{QG\_LEAN\_MONOLITH}). \emph{machine-verified}

\subsection{Bands}
For empirical gating we collect cosmology tolerances into a single bands-object and a Boolean harness:
\begin{equation}
  \texttt{CosmoBands}
  \;=\;
  \Bigl\{\texttt{cmb\_band}=\kappa_{\rm CMB},\ 
        \texttt{bao\_band}=\kappa_{\rm BAO},\ 
        \texttt{bbn\_band}=\kappa_{\rm BBN}\Bigr\},
  \qquad
  \texttt{cosmo\_ok}:\ \text{profiles}\to\{\text{OK},\text{FAIL}\}.
  \label{eq:cosmo-bands}
\end{equation}
Concretely, \(\kappa_{\rm CMB}\) is applied to a dimensionless acoustic-scale proxy; \(\kappa_{\rm BAO}\) to a BAO distance–ratio proxy; and \(\kappa_{\rm BBN}\) to a light-element yield proxy—each written in the unit-free style of this paper and used only as acceptance \emph{bands}, not as fit knobs. A \texttt{FAIL} flips the report and invalidates ILG under the selected cosmology profile; the default profile simply bundles broad, conservative bands pending a dedicated data note that instantiates \eqref{eq:cosmo-bands} with specific audit thresholds. 
\emph{Lean hooks (FRW/Growth):} \texttt{ILG.CosmoBands}, \texttt{ILG.cosmo\_bands\_default}, \texttt{ILG.cosmo\_ok} (\texttt{QG\_LEAN\_MONOLITH}). \emph{machine-verified}

\section{Compact objects: horizon and ringdown proxies}

\subsection{Static BH proxy and horizon band}
For a static, spherically symmetric configuration we use a spherical ansatz and define horizon and ringdown \emph{proxies} that match the GR baseline at leading order and are fenced by certified bands.

\paragraph{Horizon proxies.}
Let \(M>0\) denote a mass parameter and \(p=(\alpha,C_{\!\mathrm{lag}})\) the ILG parameters. The ILG horizon proxy is
\begin{equation}
  r_H^{\rm ILG}(M;p) \;\equiv\; r_{\rm proxy}(M;p)
  \;=\; \mathrm{ilg\_bh\_radius}(M;\,C_{\!\mathrm{lag}},\alpha),
  \label{eq:ilg-horizon-proxy}
\end{equation}
and the GR baseline radius is
\begin{equation}
  r_H^{\rm base}(M) \;\equiv\; r_{\rm base}(M)
  \;=\; \mathrm{baseline\_bh\_radius}(M)
  \;\;\stackrel{\text{toy}}{=}\;\; 2\,M.
  \label{eq:baseline-horizon}
\end{equation}
The certified band used in this paper is
\begin{equation}
  \bigl|\,r_H^{\rm ILG}(M;p) - r_H^{\rm base}(M)\,\bigr| \;\le\; \kappa_{\rm H},
  \qquad \kappa_{\rm H}\ge 0,
  \label{eq:horizon-band-main}
\end{equation}
which specializes (in the scaffold) to the static-proxy band
\begin{equation}
  \bigl|\,\mathrm{ilg\_bh}( \mu, C_{\!\mathrm{lag}}, \alpha) - \mathrm{baseline\_bh}(\mu)\,\bigr| \;\le\; \kappa_{\rm H}.
  \label{eq:bh-static-band}
\end{equation}

\paragraph{Ringdown proxies.}
At leading order the ringdown scale is the inverse radius. We therefore take
\begin{equation}
  \omega_{\rm rd}^{\rm ILG}(M;p) \;\propto\; \frac{1}{r_H^{\rm ILG}(M;p)},
  \qquad
  \omega_{\rm rd}^{\rm base}(M) \;\propto\; \frac{1}{r_H^{\rm base}(M)},
  \label{eq:ringdown-proxies}
\end{equation}
and encode the certified deviation band as
\begin{equation}
  \bigl|\,\omega_{\rm rd}^{\rm ILG}(M;p) - \omega_{\rm rd}^{\rm base}(M)\,\bigr| \;\le\; \kappa_{\rm RD},
  \qquad \kappa_{\rm RD}\ge 0.
  \label{eq:ringdown-band}
\end{equation}

\noindent\emph{Lean hooks (Compact/BHDerive):}
\texttt{ILG.Compact.SphericalAnsatz}, \texttt{ILG.Compact.horizon\_radius}, 
\texttt{ILG.Compact.baseline\_bh}, \texttt{ILG.Compact.ilg\_bh}, 
\texttt{ILG.Compact.ringdown\_band}, 
\texttt{ILG.BHDerive.horizon\_proxy}, \texttt{ILG.BHDerive.horizon\_band}, 
\texttt{ILG.BHDerive.ringdown\_proxy}, \texttt{ILG.BHDeriveCert.verified\_any}. \emph{machine-verified}

\subsection{What it would take to upgrade (curvature-invariant replacements)}
The proxies above are safe stubs used only to state banded equalities. To replace them with curvature-invariant statements, we will:
\begin{enumerate}\itemsep4pt
  \item \textbf{Replace the spherical ansatz by an invariant horizon definition.} 
  Define the horizon as a marginally outer trapped surface (vanishing outward null expansion \(\theta_{(\ell)}=0\)) or via a Killing horizon where \(g^{\mu\nu}\chi_\mu\chi_\nu=0\) for a timelike Killing field \(\chi^\mu\). Implement this as a predicate \(\mathrm{Horizon}(g)\) selecting the smallest positive root \(r_H\) of the invariant condition. Prove existence/uniqueness under the static, spherically symmetric hypotheses and show \(r_H\to r_H^{\rm base}\) in the GR limit \(p\to 0\).
  \item \textbf{Derive field equations for \(g,\psi\) from the ILG action.}
  Replace \texttt{EL\_g}, \texttt{EL\_ψ} scaffolds with explicit Euler–Lagrange equations from the ILG action \(S_{\rm tot}[g,\psi;p]\). From these, derive the invariant surface gravity \(\kappa_H\) and verify its GR-limit value on \(r_H\).
  \item \textbf{Promote ringdown to quasinormal modes (QNMs).}
  Linearize around the static background and derive master equations (Regge–Wheeler/Zerilli–type generalizations) for axial/polar perturbations. Define \(\omega_{\rm QNM}\) as the discrete spectrum of the associated non-self-adjoint operator with outgoing boundary conditions. Prove a banded comparison
  \[
    \bigl|\,\omega_{\rm QNM}^{\rm ILG} - \omega_{\rm QNM}^{\rm base}\,\bigr|\;\le\;\kappa_{\rm RD},
  \]
  by bounding the potential deformations induced by \(w(k,a)\) (or their static analogues) and using monotonicity/positivity lemmas already verified for effective weights.
  \item \textbf{Wire invariants to the audit system.}
  Add \texttt{HorizonInvariant.lean} and \texttt{QNMInvariant.lean} modules exposing: 
  \(\mathrm{HorizonOK}(g)\), the invariant \(r_H(g)\), \(\kappa_H(g)\), and the spectral map \(g\mapsto\omega_{\rm QNM}(g)\), each with GR-limit lemmas and band certificates. Replace \eqref{eq:horizon-band}–\eqref{eq:ringdown-band} by these invariant statements and update the falsifier harness to use \((r_H,\kappa_H,\omega_{\rm QNM})\).
\end{enumerate}
Because we control the codebase, these upgrades are mechanical once the variations and invariant definitions are in place: no new parameters are introduced, and all statements remain dimensionless and audit-gated.

\section{Global audit identities and hard falsifiers}

\subsection{Planck identity and speed-from-units (with single-inequality audit)}
Two exact identities underwrite all displays:
\begin{equation}
  \frac{c^{3}\,\lambda_{\mathrm{rec}}^{2}}{\hbar\,G} \;=\; \frac{1}{\pi}
  \quad\text{(Planck-side normalization),}
  \qquad
  c \;=\; \frac{\ell_0}{\tau_0}
  \quad\text{(speed-from-units).}
  \label{eq:planck-speed-identities}
\end{equation}
They arise from the units-quotient map \(\mathcal{K}\) and the route-equality gate (K-gate):
\[
\mathcal{K}\!\left[\pi\,\frac{c^{3}\lambda_{\mathrm{rec}}^{2}}{\hbar G}\right]=1
\quad\text{and}\quad
\mathcal{K}\!\left[\frac{\ell_0}{c\,\tau_0}\right]=1,
\]
which are the exact forms of \eqref{eq:planck-id-proof} and \eqref{eq:speed-identity}. Empirically, route agreement is enforced by a \emph{single-inequality audit} with a correlation guard:
\begin{equation}
  \bigl|\Delta K\bigr| \;\le\; k\,u_{\rm comb},
  \qquad
  u_{\rm comb}\;\doteq\; \sqrt{u(\ell_0)^2+u(\lambda_{\rm rec})^2-2\rho\,u(\ell_0)\,u(\lambda_{\rm rec})},
  \quad |\rho|\le 1,
  \label{eq:single-inequality-audit}
\end{equation}
where \(\Delta K\) is the measured residual of the corresponding \(\mathcal{K}[\cdot]=1\) statement, \(u(\cdot)\) are standard uncertainties, \(\rho\) bounds correlation, and \(k\) is a fixed audit multiplier chosen \emph{ex ante}. The exact audit lines used in this paper (including thresholds) appear in the “How to verify” box. \emph{machine-verified}

\subsection{Discrete cone bound and eight-tick (observational meaning)}
Coarse-grained reach is causally fenced by the cone inequality
\begin{equation}
  r(y)-r(x) \;\le\; c\,[\,t(y)-t(x)\,],
  \label{eq:global-cone}
\end{equation}
which forbids super-cone transport in any audit chain and provides a universal cross-check for time-of-flight analyses (e.g., multi-messenger GW/EM arrivals, lensing time delays). On the 3-cube the minimal nontrivial cycle period is
\begin{equation}
  T_{\min}(3)=2^{3}=8,
  \label{eq:eight-tick-obs}
\end{equation}
with a Nyquist obstruction below \(2^{D}\) and bijection at threshold. Practically, this quantizes admissible coarse-grained periodicities and guards against over-resolving inferred cycles in weak-field reconstructions. Both \eqref{eq:global-cone} and \eqref{eq:eight-tick-obs} enter as invariant sanity checks alongside the scalar-sector bands. \emph{machine-verified}

\subsection{Failure modes (hard falsifiers)}
A report flips to \textsc{FAIL} if \emph{any} of the following occur (all bands are fixed in advance; no tuning per system):
\begin{itemize}
  \item \textbf{K-gate residual:} \(\bigl|\Delta K\bigr|>k\,u_{\rm comb}\) in \eqref{eq:single-inequality-audit}.
  \item \textbf{GW speed:} \(c_T\neq 1\) or \(|c_T^2-1|>\kappa_{\rm GW}\) (equivalently \(|v_{\rm gw}-1|>\kappa_{\rm GW}\)).
  \item \textbf{PPN:} \(|\gamma-1|>\kappa_{\rm PPN}\) or \(|\beta-1|>\kappa_{\rm PPN}\) under the stated weak-field premises.
  \item \textbf{Lensing/time delay:} \(|(\Phi+\Psi)_{\rm ILG}-(\Phi+\Psi)_{\rm GR}|>\kappa_{\rm L}\) or \(|\Delta t_{\rm ILG}-\Delta t_{\rm GR}|>\kappa_{\rm T}\).
  \item \textbf{FRW/growth:} Violation of \(H^2=\rho_\psi\) or \(\rho_\psi<0\) in the background link; growth index \(f\le 0\) under the conditions of \eqref{eq:growth-index-positive}.
  \item \textbf{Compact objects:} \(|r_H^{\rm ILG}-r_H^{\rm base}|>\kappa_{\rm H}\) or \(|\omega_{\rm rd}^{\rm ILG}-\omega_{\rm rd}^{\rm base}|>\kappa_{\rm RD}\).
\end{itemize}
These checks are packaged in the falsifier harness (object of bands and a Boolean gate). The harness takes a fixed profile \(\{\kappa_{\rm PPN},\kappa_{\rm GW},\kappa_{\rm L},\kappa_{\rm T},\kappa_{\rm H},\kappa_{\rm RD}\}\) and returns \textsc{OK} or \textsc{FAIL} with no hidden degrees of freedom; the default profile is provided in the artifact and used verbatim here. (Lean hooks: \texttt{ILG.Falsifiers}, \texttt{ILG.falsifiers\_default}, \texttt{ILG.falsifiers\_ok}.) \emph{machine-verified}

\section{Empirical program and scope}

\subsection{What to test now}
We list concrete, near-term audits that exercise the exact equalities and bands printed in this paper. Each item names: (i) the observable, (ii) the computation in the unit-free style, and (iii) the pass/fail rule tied to earlier equations.

\paragraph{Pulsar timing (discretization \& cone checks).}
\emph{Observable:} barycentered pulse time-of-arrival (TOA) series for stable millisecond pulsars. 
\emph{Computation:} form residuals after standard timing-model subtraction and test (a) the \emph{cone bound} \eqref{eq:global-cone} for any inferred superluminal propagation in glitch/recovery fronts; (b) coarse periodicities against the \emph{eight-tick} admissibility \eqref{eq:eight-tick-obs} at the analysis resolution (no cycles below the admissible threshold in the coarse-grained reconstruction).
\emph{Pass/Fail:} any super-cone inference or forbidden periodicity triggers \textsc{FAIL}.

\paragraph{GW speed constraints.}
\emph{Observable:} group speed from gravitational-wave events (multi-messenger where available, or internal waveform dispersion). 
\emph{Computation:} compute \(v_{\rm gw}\) and its uncertainty; evaluate \(|v_{\rm gw}-1|\) against the certified band \eqref{eq:gw-band}. 
\emph{Pass/Fail:} \(|v_{\rm gw}-1|>\kappa_{\rm GW}\) flips to \textsc{FAIL}. (This also audits the quadratic-action predicate fixing \(c_T^2=1\), cf.\ \eqref{eq:cT-equals-1}.)

\paragraph{Cassini/solar-system PPN.}
\emph{Observable:} Shapiro time delay, light deflection, perihelion tests yielding \(\gamma\) and \(\beta\).
\emph{Computation:} extract \(\gamma,\beta\) in the standard PPN fits; check the \emph{solution-linked bands} \eqref{eq:ppn-solution-bands} and, where applicable, the \emph{small-coupling} linearized forms \eqref{eq:ppn-linear-bounds}.
\emph{Pass/Fail:} any \(|\gamma-1|\) or \(|\beta-1|\) exceeding the fixed \(\kappa_{\rm PPN}\) flips to \textsc{FAIL}.

\paragraph{Strong-lensing time delays.}
\emph{Observable:} image positions and measured delays in well-modeled galaxy- or cluster-scale lenses. 
\emph{Computation:} compute the GR proxy deflection and potential using the measured baryonic profile; form the residuals against ILG via \eqref{eq:lensing-band-ILG} and \eqref{eq:time-delay-band-ILG}. 
\emph{Pass/Fail:} \(|\hat\alpha_{\rm ILG}-\hat\alpha_{\rm GR}|>\kappa_{\rm L}\) or \(|\Delta t_{\rm ILG}-\Delta t_{\rm GR}|>\kappa_{\rm T}\) flips to \textsc{FAIL}.

\paragraph{Large-scale growth.}
\emph{Observable:} linear growth via \(f\sigma_8\) proxies (e.g.\ redshift-space distortions) and weak-lensing shear. 
\emph{Computation:} compute \(f(a,k)=d\ln\delta/d\ln a\) and \(D(a,k)\) from the growth equation \eqref{eq:growth-eq-cosmo} with the fixed weight \(w(k,a)\) of \eqref{eq:wka}; audit the positivity statement \eqref{eq:growth-index-positive} and the \(\sigma_8\) linkage \eqref{eq:sigma8-link}. 
\emph{Pass/Fail:} any violation of \(f>0\) under the stated premises, or inconsistency of \(\sigma_8(a)\) with the linkage, flips to \textsc{FAIL}.

\paragraph{Global audits (always on).}
\emph{Observable:} identity checks across all analyses. 
\emph{Computation:} run the single-inequality K-gate audit \eqref{eq:single-inequality-audit} for the Planck-side normalization and speed-from-units identities \eqref{eq:planck-speed-identities}.
\emph{Pass/Fail:} \(|\Delta K|>k\,u_{\rm comb}\) flips to \textsc{FAIL}.

\subsection{What not to claim in this paper}
We make no claim of a full, nonperturbative quantization of the metric or of having solved the complete Einstein field dynamics with quantum back-reaction. ILG is a \emph{verified scaffold}: it reproduces GR tests at leading order, expresses deviations as \emph{bands} with \emph{no tunable parameters}, and packages falsifiers as audit inequalities. The compact-object and lensing statements that exceed leading-order GR are explicitly declared as \emph{proxies} and are fenced by certified bands; §10 outlines the upgrade path to curvature-invariant definitions and quasinormal-mode spectra. Detailed data fits, likelihoods, and survey-specific systematics belong in a separate data note that instantiates the cosmology bands (\S\ref{eq:cosmo-bands}) with concrete thresholds, uses the same unit-free displays, and preserves the no-tuning policy.

\section{Methods: RS$\to$classical bridge and Lean artifact}
\label{sec:methods-bridge}

\subsection{RS$\to$classical bridge (spec and policy)}
This paper uses a one-to-one bridge from the instrument layer to classical displays. We state it in prose; the exact symbols and identities used in the main text are identical to the audited formulas in the artifact.

\paragraph{Cost $J$ (unique, stationary-action shadow).}
The ledger cost is \(J(x)=\tfrac12(x+1/x)-1\) on \(\mathbb{R}_{>0}\). Its stationary paths map to classical stationary-action/Dirichlet forms; Euler–Lagrange statements coincide where defined. No tunable constants enter.

\paragraph{Eight-tick (minimal period).}
On a \(D\)-dimensional hypercube the minimal Hamiltonian cycle period is \(2^D\) (with Nyquist obstruction below threshold). In \(D=3\) this gives the “eight-tick” identity used as a coarse periodicity fence in weak-field reconstructions.

\paragraph{Cone bound (causal speed identity).}
The discrete step bound induces the light-cone inequality \(r(y)-r(x)\le c\,[t(y)-t(x)]\) with \(c=\ell_0/\tau_0\). This is used directly as an audit for time-of-flight and multi-messenger comparisons.

\paragraph{Planck gate (recognition length).}
The recognition length is fixed by the identity
\[
\frac{c^3\,\lambda_{\mathrm{rec}}^2}{\hbar\,G}=\frac{1}{\pi},
\]
and appears only through that unit-free normalization (and its uncertainty propagation) in this paper.

\paragraph{Mass law (present, not used here).}
The ledger-native mass family law \(m=B\cdot E_{\mathrm{coh}}\cdot \varphi^{\,r+f}\) underlies matter-sector ladders; we do not use it in the gravity results reported here except for constants already visible in the ILG kernel.

\paragraph{ILG kernel (what the paper actually uses).}
Gravity enters through an \emph{effective, recognition-limited weight} \(w\) that modifies the Poisson/growth source. The cleaned kernel used in the main text is
\[
w(k,a)=1+C_\varphi\Bigl(\frac{a}{k\,\tau_0}\Bigr)^{\alpha_*},
\qquad
C_\varphi=\varphi^{-3/2},\quad \alpha_*=\tfrac12(1-\varphi^{-1}),\quad \varphi=\tfrac{1+\sqrt5}{2}.
\]
These numbers are fixed by identities (no fit knobs). All consequences in the paper (weak field, PPN bands, GW speed, lensing/time delay bands, FRW/growth statements) use this \(w\) and the identities above.

\paragraph{Scope and policy (no free parameters).}
\emph{Scope.} Derivations are parameter-free; presentation is classical with numeric mapping only. \emph{Anchors.} Exogenous constants are \([c,\hbar,G,\alpha_{\rm inv}]\); unit anchors \((\tau_0,\ell_0)\) fix \(c=\ell_0/\tau_0\). \emph{Globals.} Kernel exponents and amplitudes (\(\alpha_*,C_\varphi\)) are derived constants; global normalizations are set by definition (e.g.\ \(\lambda=1\) by normalization). \emph{Policy.} Per-system or per-galaxy tuning is forbidden; no parameter is fitted to a target dataset anywhere in this paper. (This is the policy the artifact enforces at the audit gates.)

\subsection{Machine-verified artifact (toolchain and checks)}
\paragraph{Pinned toolchain.}
The repository includes a \texttt{lean-toolchain} pin (Lean 4) and a locked \texttt{lake-manifest.json}. Build and minimal CI:
\begin{verbatim}
lake build
lake exe ci_checks
\end{verbatim}

\paragraph{How to verify (single-line reports used here).}
Each line emits a pass/fail certificate for the exact statement printed in the main text.
\begin{verbatim}
#eval IndisputableMonolith.URCAdapters.reality_master_report
#eval IndisputableMonolith.URCAdapters.k_gate_report
#eval IndisputableMonolith.URCAdapters.lambda_rec_identity_report
#eval IndisputableMonolith.URCAdapters.eight_tick_report
#eval IndisputableMonolith.URCAdapters.cone_bound_report
\end{verbatim}

Gravity-specific aggregated reports (see Appendix A for complete list):
\begin{verbatim}
#eval IndisputableMonolith.URCAdapters.ppn_aggregate_report
#eval IndisputableMonolith.URCAdapters.gw_speed_aggregate_report
#eval IndisputableMonolith.URCAdapters.lensing_aggregate_report
#eval IndisputableMonolith.URCAdapters.friedmannI_aggregate_report
#eval IndisputableMonolith.URCAdapters.compact_aggregate_report
\end{verbatim}

At acceptance, we will pin the commit hash and include an archival DOI for the snapshot used to generate this manuscript's checks.

\subsection{MP tautology (minimality, one line)}
Lean lemma \texttt{MPMinimal} formalizes that “nothing cannot recognize itself” is the weakest sufficient axiom for the instrument; here it serves only to ground the discrete calculus and conservation scaffolding used by the audit gates. \emph{machine-verified}

\section{Discussion}

\subsection{Why this is ``quantum gravity''}
The same instrument-level calculus that yields amplitudes and the Born rule \eqref{eq:born} also governs the gravity sector through the effective weight \(w\) that modifies sources in Poisson/growth (\S\!3). Unification happens at the instrument: one ledger, one cost, one bridge, one audit stack. “Quantum” here means that probabilities and interference structure arise from weights/amplitudes fixed by identities and audited by the K-gate and Planck-side normalization \eqref{eq:planck-id-proof}–\eqref{eq:k-gate-planck}; “gravity” is the sector where those same weights induce a specific, parameter-free effective kernel \(w(k,a)\) that reproduces GR at leading order while exposing deviations as banded, falsifiable statements—PPN \eqref{eq:ppn-linear-bounds}–\eqref{eq:ppn-solution-bands}, GW speed \eqref{eq:cT-equals-1}–\eqref{eq:gw-band}, lensing/time delay \eqref{eq:lensing-band-ILG}–\eqref{eq:time-delay-band-ILG}, and FRW/growth \eqref{eq:friedmannI}, \eqref{eq:growth-index-positive}. No extra quantization of the metric is assumed; the quantum and gravitational statements live on the same audit rails and share the same unit-free identities.

\subsection{Comparison to GR and to modified gravity}
In certified limits the framework matches GR: \(c_T^2=1\) \eqref{eq:cT-equals-1}; \(\gamma\to1\), \(\beta\to1\) within proved bands \eqref{eq:ppn-linear-bounds}–\eqref{eq:ppn-solution-bands}; the FRW link \(H^2=\rho_\psi\) with \(\rho_\psi\ge 0\) \eqref{eq:friedmannI}; and leading-order lensing/time-delay proxies \eqref{eq:lensing-band-ILG}–\eqref{eq:time-delay-band-ILG}. Where departures are allowed, they are not knobs to be tuned but \emph{inequalities to be tested}. This contrasts with many modified-gravity schemes that introduce sector-specific couplings or screening parameters fit to data. Here, constants are fixed by identities (e.g., \(\lambda_{\rm rec}\) via \eqref{eq:planck-id-proof}, \(c=\ell_0/\tau_0\) via \eqref{eq:speed-identity}); the kernel \(w(k,a)\) has no tunable parameters (\S\!3.2); and audits are global, units-aware, and single-inequality in form \eqref{eq:single-inequality-audit}. Empirically, this means the framework either survives a shared set of predeclared bands across systems or it fails crisply—no “per-galaxy” or “per-dataset” rescue fits.

\subsection{Limitations and planned upgrades}
Some statements in the gravity stack are marked \emph{scaffold/toy} and are used only to fence proxies with explicit bands (\S\!4.3). We list the limitations and the precise hardening steps, all within the current codebase and policy (no new parameters):
\begin{itemize}
  \item \textbf{Field equations (EL predicates).} Presently \(\mathrm{EL}_g\) and \(\mathrm{EL}_\psi\) serve as stubs in the GR-limit summary \eqref{eq:ELg-GR}–\eqref{eq:ELpsi-GR}. \emph{Upgrade:} derive the Euler–Lagrange equations from \(S_{\rm tot}[g,\psi;p]\) \eqref{eq:S-total-cov} and replace the predicates with explicit equations; retain the GR-limit vanishing \(T_{\mu\nu}\) \eqref{eq:Tmunu-GR}.
  \item \textbf{GW quadratic-action link.} The predicate fixing \(c_T^2=1\) is scaffolded. \emph{Upgrade:} compute the second-order action for tensor modes and prove the dispersion relation directly (no appeal to a proxy), preserving the band \eqref{eq:gw-band}.
  \item \textbf{Lensing/time-delay proxies.} Banded equalities \eqref{eq:lensing-band-ILG}–\eqref{eq:time-delay-band-ILG} currently close via a toy proxy aligned to the GR baseline. \emph{Upgrade:} rederive the lensing potential and delays from the modified Poisson equation with the fixed kernel \(w(k,a)\) (\S\!3.2), removing the proxy.
  \item \textbf{FRW beyond placeholders.} We use Friedmann I and nonnegativity \eqref{eq:friedmannI}. \emph{Upgrade:} derive continuity and Friedmann II from the ILG stress tensor; prove existence/regularity of FRW solutions given \(w\ge 0\), and extend the growth result \eqref{eq:growth-index-positive} to sharpened conditions.
  \item \textbf{Compact-object invariants.} Horizon and ringdown are proxy-based \eqref{eq:horizon-band}–\eqref{eq:ringdown-band}. \emph{Upgrade:} define horizons invariantly (MOTS/Killing horizon), compute surface gravity \(\kappa_H\), and derive quasinormal spectra; recast the bands in terms of \((r_H,\kappa_H,\omega_{\rm QNM})\) (§10.2).
  \item \textbf{Bands schema constants.} Some tolerance–parameter maps are toy proportionalities. \emph{Upgrade:} replace with constants from explicit linearizations (no tuning), and tighten wherever positivity/monotonicity lemmas allow.
  \item \textbf{Audit packaging.} The “How to verify” list (§13.2) names per-claim \#eval lines. \emph{Upgrade:} add aggregated reports (\texttt{ppn\_report}, \texttt{gw\_speed\_report}, \texttt{lensing\_report}, \texttt{friedmannI\_report}, \texttt{compact\_report}) so each subsection of this paper is auditable in one line without changing any mathematics.
\end{itemize}
None of these upgrades alter definitions or introduce parameters. They remove proxies, replace placeholders by derived invariants, and shrink bands where theorems allow—tightening the same audit rails that already govern the results displayed here.

\section{Future Work}

Near-term priorities focus on replacing scaffold components with full derivations while preserving the zero-parameter stance:

\paragraph{Near-term (derivations).}
Derive the Euler–Lagrange equations from $S_{\rm tot}[g,\psi;p]$ and replace the current EL predicates with explicit field equations. Compute the second-order action for tensor modes and prove $c_T^2=1$ directly from the quadratic expansion. Rederive lensing and time-delay formulas from the modified Poisson equation with the fixed kernel $w(k,a)$.

\paragraph{Medium-term (invariants).}
Replace compact-object proxies with curvature-invariant horizon definitions (MOTS or Killing horizons) and derive quasinormal-mode spectra from perturbation master equations. Prove Friedmann II and continuity from the ILG stress tensor. Extend growth results with sharpened positivity conditions.

\paragraph{Long-term (extensions).}
Extend the framework to full quantum back-reaction while maintaining audit gates. Develop sector-coupling theorems that unify matter, radiation, and gravity under the single measurement principle. Apply the verified scaffold to specific observational targets: strong-field binary mergers, primordial perturbations, and ultra-compact objects.

All upgrades will maintain the core policy: no per-system tuning, all constants fixed by identities, all claims machine-verified.

\section*{Data Availability}

All data, code, and formal proofs used in this work are openly available. The Lean verification artifact (IndisputableMonolith) is hosted at the repository referenced in the verification artifact note and will be archived with a permanent DOI upon acceptance. The artifact includes: (i) complete source code for all theorems and lemmas cited in the text, (ii) build scripts and CI configuration, (iii) single-line verification commands for each claim, and (iv) detailed documentation of the bridge between classical displays and formal statements. No proprietary software or restricted datasets were used in this work.

\section*{References}
% Self-contained reference list in numeric order (unsrtnat-like style)

\begin{thebibliography}{99}

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

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

\bibitem{Susskind1995}
L.~Susskind,
``The World as a Hologram,''
\emph{Journal of Mathematical Physics} \textbf{36}, 6377--6396 (1995).

\bibitem{ADM1962}
R.~Arnowitt, S.~Deser, and C.~W. Misner,
``The dynamics of general relativity,''
in \emph{Gravitation: An Introduction to Current Research} (ed. L. Witten),
Wiley, New York (1962). [Reprinted \emph{General Relativity and Gravitation} \textbf{40}, 1997--2027 (2008).]

\bibitem{ReggeWheeler1957}
T.~Regge and J.~A. Wheeler,
``Stability of a Schwarzschild singularity,''
\emph{Physical Review} \textbf{108}, 1063--1069 (1957).

\bibitem{Zerilli1970}
F.~J. Zerilli,
``Gravitational field of a particle falling in a Schwarzschild geometry analyzed in tensor harmonics,''
\emph{Physical Review D} \textbf{2}, 2141--2160 (1970).

\bibitem{Wald1984}
R.~M. Wald,
\emph{General Relativity},
University of Chicago Press (1984).

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

\bibitem{Weinberg1972}
S.~Weinberg,
\emph{Gravitation and Cosmology: Principles and Applications of the General Theory of Relativity},
Wiley (1972).

\bibitem{Will2014}
C.~M. Will,
``The Confrontation between General Relativity and Experiment,''
\emph{Living Reviews in Relativity} \textbf{17}, 4 (2014).

\bibitem{Cassini2003}
B.~Bertotti, L.~Iess, and P.~Tortora,
``A test of general relativity using radio links with the Cassini spacecraft,''
\emph{Nature} \textbf{425}, 374--376 (2003).

\bibitem{GW170817_PRL2017}
B.~P. Abbott et al. (LIGO Scientific Collaboration and Virgo Collaboration),
``GW170817: Observation of Gravitational Waves from a Binary Neutron Star Inspiral,''
\emph{Physical Review Letters} \textbf{119}, 161101 (2017).

\bibitem{BartelmannSchneider2001}
M.~Bartelmann and P.~Schneider,
``Weak gravitational lensing,''
\emph{Physics Reports} \textbf{340}, 291--472 (2001).

\bibitem{Planck2018}
Planck Collaboration,
``Planck 2018 results. VI. Cosmological parameters,''
\emph{Astronomy \& Astrophysics} \textbf{641}, A6 (2020).

\bibitem{PDG2024}
Particle Data Group,
``Review of Particle Physics,''
\emph{Progress of Theoretical and Experimental Physics} \textbf{2024}, 083C01 (2024).

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

\bibitem{EisensteinHu1998}
D.~J. Eisenstein and W.~Hu,
``Baryonic features in the matter transfer function,''
\emph{Astrophysical Journal} \textbf{496}, 605--614 (1998).

\bibitem{Eisenstein2005}
D.~J. Eisenstein et al.,
``Detection of the Baryon Acoustic Peak in the Large-Scale Correlation Function of SDSS Luminous Red Galaxies,''
\emph{Astrophysical Journal} \textbf{633}, 560--574 (2005).

\bibitem{DesbrunDEC2005}
M.~Desbrun, A.~N. Hirani, M.~Leok, and J.~E. Marsden,
``Discrete Exterior Calculus,'' (2005).

\bibitem{Savage1997Gray}
C.~Savage,
``A Survey of Combinatorial Gray Codes,''
\emph{SIAM Review} \textbf{39}(4), 605--629 (1997).

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

\bibitem{Landau1976}
L.~D. Landau and E.~M. Lifshitz,
\emph{Mechanics}, 3rd ed.,
Pergamon (1976).

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

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

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

\end{thebibliography}

\appendix

\section{Verify-it-yourself (one-click checks)}
\label{app:verify}
All proofs used in the main text are machine-checked. Build once, then run the single-line reports below. Each prints \texttt{OK} on success or fails deterministically.

\subsection*{Toolchain (pinned)}
\noindent\texttt{lake build}\\
\noindent\texttt{lake exe ci\_checks}

\subsection*{Master and core identities}
\noindent\texttt{\#eval IndisputableMonolith.URCAdapters.reality\_master\_report} \hfill \(\to\) \texttt{OK}\\
\texttt{\#eval IndisputableMonolith.URCAdapters.k\_gate\_report} \hfill \(\to\) \texttt{OK}\\
\texttt{\#eval IndisputableMonolith.URCAdapters.lambda\_rec\_identity\_report} \hfill \(\to\) \texttt{OK}\\
\texttt{\#eval IndisputableMonolith.URCAdapters.eight\_tick\_report} \hfill \(\to\) \texttt{OK}\\
\texttt{\#eval IndisputableMonolith.URCAdapters.cone\_bound\_report} \hfill \(\to\) \texttt{OK}\\
\texttt{\#eval IndisputableMonolith.URCAdapters.born\_rule\_report} \hfill \(\to\) \texttt{OK}

\subsection*{Time/weight audits used by ILG}
\noindent\texttt{\#eval IndisputableMonolith.URCAdapters.ilg\_time\_report} \hfill \(\to\) \texttt{OK}\\
\texttt{\#eval IndisputableMonolith.URCAdapters.ilg\_effective\_report} \hfill \(\to\) \texttt{OK}

\subsection*{Gravity-section aggregators (packaged checks)}
\noindent Aggregate reports that bundle the precise lemmas cited in the paper:
\begin{quote}\small\ttfamily
\#eval IndisputableMonolith.URCAdapters.ppn\_aggregate\_report \quad\% \(\gamma,\beta\) bands \(\to\) OK\\
\#eval IndisputableMonolith.URCAdapters.gw\_speed\_aggregate\_report \quad\% \(c_T^2=1\) band \(\to\) OK\\
\#eval IndisputableMonolith.URCAdapters.lensing\_aggregate\_report \quad\% lensing/time delay bands \(\to\) OK\\
\#eval IndisputableMonolith.URCAdapters.friedmannI\_aggregate\_report \quad\% \(H^2=\rho_\psi,\ \rho_\psi\ge 0\) \(\to\) OK\\
\#eval IndisputableMonolith.URCAdapters.compact\_aggregate\_report \quad\% horizon/ringdown proxies \(\to\) OK
\end{quote}
\noindent\emph{machine-verified}

\section{RS$\to$classical statements (quoted verbatim)}
\label{app:bridge-verbatim}
\subsection*{Bridge items used in this paper (from \texttt{@CLASSICAL\_BRIDGE\_TABLE})}
\begin{verbatim}
BRIDGE;CostFunctional;J(x)=0.5(x+1/x)-1;StationaryAction/Dirichlet;T5;Yes
BRIDGE;EightTick;min_period=2^D;minimal cell traversal;T6;Yes;D=3=>8
BRIDGE;CausalBound;c=l0/tau0;light_cone;proved(StepBounds);Yes
BRIDGE;LambdaRec;ledger-curvature extremum;Planck-normalization;Yes
BRIDGE;BornRule;exp(-C[gamma]) => |psi|^2;Born;path->wave link;Yes
BRIDGE;ILG;w(k,a) kernel;modified Poisson/growth;Yes;Global-only
\end{verbatim}

\subsection*{ILG kernel and usage (from \texttt{@ILG\_SPEC})}
\begin{verbatim}
ILG;kernel_kspace; w(k,a)=1+phi^(-3/2)*[a/(k tau0)]^alpha
ILG;poisson_modified; k^2 Phi = 4pi G a^2 rho_b w(k,a) delta_b
ILG;growth_equation; ddot(delta)+2H dot(delta)-4pi G a^2 rho_b w(k,a) delta=0
ILG;rotation_curves; v_model^2(r)=w(r)v_baryon^2(r)
ILG;weight_factor; w(r)=lambda*xi*n(r)*(T_dyn/tau0)^alpha*zeta(r)
ILG;time_kernel; w_t(r)=1+phi^(-5)[(T_dyn/T_ref)^alpha-1]
ILG;acc_kernel; w_g(r)=1+phi^(-5)[((g_bar+g_ext)/g_ref)^(-alpha)-(1+g_ext/g_ref)^(-alpha)]
ILG;xi_quantiles; xi=1+phi^(-5)*u_b^(1/2); bins=B=5
ILG;n_profile; n(r)=1+A[1-exp(-(r/r0)^p)]; (A,r0,p)=(7,8 kpc,1.6)
ILG;zeta_thickness; h_z/R_d=0.25; clip=[0.8,1.2]; global_only=true
ILG;g_ref; baryon_derived_single_value; frozen=true
ILG;geometry_policy; positions/inclinations=photometric_only
ILG;fairness; identical_masks+error_model across ILG/MOND/LCDM
\end{verbatim}
\noindent\emph{Source}

\section{Lean symbol index (gravity modules)}
\label{app:lean-index}
The following map lists the named lemmas and helpers cited in the paper. Paths are relative to \texttt{IndisputableMonolith/Relativity/ILG}.

\subsection*{Action}
\noindent\texttt{Action.lean}: \texttt{ILGParams}, \texttt{EHAction}, \texttt{PsiKinetic}, \texttt{PsiPotential}, \texttt{PsiAction}, \texttt{L\_kin}, \texttt{L\_mass}, \texttt{L\_pot}, \texttt{L\_coupling}, \texttt{L\_cov}, \texttt{S\_total\_cov}, \texttt{gr\_limit\_cov}.

\subsection*{Variation}
\noindent\texttt{Variation.lean}: \texttt{EL\_gr\_limit}, \texttt{dS\_zero\_gr\_limit}, \texttt{Tmunu\_gr\_limit\_zero}, \texttt{T00\_nonneg\_from\_metric\_stationarity}.

\subsection*{WeakField / Linearize}
\noindent\texttt{WeakField.lean}: \texttt{Perturbation}, \texttt{mkNewtonian\_gauge}, \texttt{v\_model2}, \texttt{v\_model2\_eps}, \texttt{v\_model2\_eps\_eval}, \texttt{v\_model2\_r}, \texttt{v\_model2\_r\_eval}.\\
\noindent\texttt{Linearize.lean}: \texttt{ModifiedPoisson}, \texttt{w\_lin}, \texttt{w\_eff}, \texttt{w\_of\_Phi}, \texttt{w\_r}, \texttt{w\_r\_eval}.

\subsection*{PPN}
\noindent\texttt{PPN.lean}: \texttt{ILG.PPN.gamma\_def}, \texttt{ILG.PPN.beta\_def}, \texttt{ILG.ppn\_gamma\_bound\_small}, \texttt{ILG.ppn\_beta\_bound\_small}.\\
\noindent\texttt{PPNDerive.lean}: \texttt{ILG.gamma\_band\_solution}, \texttt{ILG.beta\_band\_solution}.

\subsection*{GW}
\noindent\texttt{GW.lean}: \texttt{ILG.GW.QuadraticActionGW}, \texttt{ILG.GW.c\_T2}, \texttt{ILG.GW.cT\_band}, \texttt{ILG.GW.gw\_band}.

\subsection*{Lensing}
\noindent\texttt{Lensing.lean}: \texttt{ILG.lensing\_band}, \texttt{ILG.deflection}, \texttt{ILG.time\_delay\_band}, \texttt{ILG.deflection\_spherical}.

\subsection*{FRW / Growth}
\noindent\texttt{FRW.lean}: \texttt{ILG.frw\_background\_exists}, \texttt{ILG.FriedmannI}, \texttt{ILG.FriedmannI\_T\_equals\_rho}, \texttt{ILG.rho\_psi\_nonneg}, \texttt{ILG.FriedmannI\_gr\_limit}.\\
\noindent\texttt{Growth.lean}: \texttt{ILG.growth\_index\_pos\_of}, \texttt{ILG.sigma8\_of\_eval}, \texttt{ILG.growth\_from\_w}.

\subsection*{Compact}
\noindent\texttt{Compact.lean}: \texttt{ILG.Compact.SphericalAnsatz}, \texttt{ILG.Compact.horizon\_radius}, \texttt{ILG.Compact.baseline\_bh}, \texttt{ILG.Compact.ilg\_bh}, \texttt{ILG.Compact.horizon\_band}.\\
\noindent\texttt{BHDerive.lean}: \texttt{ILG.BHDerive.horizon\_proxy}, \texttt{ILG.BHDerive.horizon\_band}, \texttt{ILG.BHDerive.ringdown\_proxy}, \texttt{ILG.BHDeriveCert.verified\_any}.

\medskip
\noindent This index matches the symbols referenced in the main text; each appears as a proved proposition or as a fenced \texttt{scaffold/toy} placeholder flagged in §4.3 and upgraded in §10.2.



\end{document}
