zero_defect_flat_space
plain-language theorem explainer
Identically zero J-cost defect density forces the induced metric perturbation to vanish, recovering flat space. Gravity and RS-emergence authors cite it as the source-free sanity check for the defect-to-metric map. The proof is a one-tactic simplification: unfold the perturbation definition and the RS coupling κ.
Claim. For every real radius $r$, if the defect field has density identically zero (and is nonnegative), then the $(0,0)$ component of the metric perturbation induced by that field at $r$ equals $0$.
background
Module Step 2 builds linearized geometry from ledger strain. Each lattice point carries a J-cost defect $J(x)=\frac12(x+x^{-1})-1\ge 0$; a region of high defect density is strained ledger, and that strain sources curvature via $g_{\mu\nu}=\eta_{\mu\nu}+h_{\mu\nu}$.
A DefectField is a nonnegative density $\rho:\mathbb{R}^3\to\mathbb{R}$. The induced perturbation is defined componentwise: diagonal entries equal $-\kappa_{\mathrm{RS}},\rho(r,0,0)$ and off-diagonal entries vanish, with RS coupling $\kappa_{\mathrm{RS}}=8\phi^5$ from ZeroParameterGravity (derived, not fitted). In the Newtonian reading this is $h_{00}=-2\Phi$ with Poisson source $\nabla^2\Phi=\kappa\rho$.
Zero density is the empty-source case: the structure packages the constant-zero function together with the trivial nonnegativity witness.
proof idea
Construct the zero defect field as the constant density $0$ with le_refl on nonnegativity. Apply simp to the definition of the metric perturbation and to kappa_rs. The diagonal formula multiplies $\kappa_{\mathrm{RS}}$ by the density evaluated at $(r,0,0)$; that density is definitionally $0$, so the $(0,0)$ component reduces to $0$.
why it matters
Closes the flat-space boundary condition for the defect-to-metric bridge: no ledger strain means $h=0$, matching linearized GR with $T=0$. The module picture identifies defect density with the stress-energy source $T^{00}$; this theorem is the corresponding vacuum check before weak-field and proportionality lemmas in the same file.
It sits under the RS gravity program that takes $\kappa=8\phi^5$ from ZeroParameterGravity rather than fitting $G$. No downstream consumers are wired yet; the natural parents are the weak-field small-perturbation statements and the metric-from-defect certificate in this module. Framework landmarks: $\phi$-native coupling and the emergence of geometry from J-cost defects on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.