weak_field_small_perturbation
plain-language theorem explainer
Under the weak-field hypothesis on a J-cost defect field, the absolute value of the time-time metric perturbation stays strictly below one at every radius. Gravity and linearized-GR workers cite this to justify the Newtonian-limit reading of the RS defect-to-metric map. The proof rewrites the (0,0) component as −κρ, pulls out positivity of κ, and multiplies the density bound by κ.
Claim. Let $d$ be a nonnegative J-cost defect density field satisfying the weak-field condition (pointwise $|\rho_d| < 1/\kappa$ with $\kappa = \kappa_{\mathrm{RS}} > 0$). Then for every radius $r \in \mathbb{R}$, the time-time component of the induced metric perturbation obeys $\bigl|h_{00}(r)\bigr| < 1$.
background
This module builds Step 2 of the RS gravity stack: spacetime geometry as a metric perturbation sourced by ledger defects. Each voxel carries a J-cost $J(x) = \tfrac12(x+x^{-1})-1 \ge 0$; a region of high defect density is ledger strain, and that strain curves the emergent metric via $g_{\mu\nu} = \eta_{\mu\nu} + h_{\mu\nu}$.
A DefectField packages a nonnegative density $\rho(x,y,z)$. The induced perturbation is diagonal in the present model: $h_{ii} = -\kappa_{\mathrm{RS}},\rho$ on the diagonal and zero off it, with coupling $\kappa_{\mathrm{RS}} = 8\varphi^5$ from ZeroParameterGravity (Newtonian limit $h_{00} = -2\Phi$). The sibling lemma perturbation_proportional_to_kappa records exactly $h_{00}(r) = -\kappa_{\mathrm{RS}},\rho(r,0,0)$.
The weak-field condition is the pointwise density bound $|\rho| < 1/\kappa_{\mathrm{RS}}$, the RS stand-in for $|h| \ll 1$ in linearized GR. Zero defect recovers flat space; nonzero defect is identified with the stress-energy source $T^{00}$.
proof idea
Rewrite the $(0,0)$ component via perturbation_proportional_to_kappa, obtaining $-\kappa_{\mathrm{RS}},\rho$. Positivity of $\kappa_{\mathrm{RS}}$ (from ZeroParameterGravity) and the absolute-value identity $|-\kappa\rho| = \kappa|\rho|$ (via abs_neg, abs_mul, abs_of_pos) reduce the goal to $\kappa|\rho| < 1$.
Apply the weak-field hypothesis at $(r,0,0)$ to get $|\rho| < 1/\kappa$. Multiply both sides by $\kappa > 0$ (mul_lt_mul_of_pos_left), then simplify $\kappa\cdot(1/\kappa) = 1$ by field_simp.
why it matters
Linearized gravity is only trustworthy when $|h_{\mu\nu}| \ll 1$. This theorem closes that gate for the RS defect-to-metric map: whenever the defect density obeys the weak-field bound, the constructed $h_{00}$ is automatically a small perturbation, so the Newtonian reading $h_{00} = -2\Phi$ and the identification of defect density with $T^{00}$ stay inside the linearized regime.
It sits in the Gravity.MetricFromDefect development that derives geometry from J-cost strain, with coupling fixed by the zero-parameter gravity constant $\kappa = 8\varphi^5$ (tied to the RS constants $G = \varphi^5/\pi$ and the forcing chain's $\varphi$). No downstream consumers are wired yet; the immediate role is local certification inside MetricFromDefectCert and the weak-field section of the module. Used_by is empty, so this is presently a leaf lemma rather than a bridge into a larger proved theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.