MetricFromDefectCert
plain-language theorem explainer
Certificate packaging two structural facts about the RS metric perturbation: index symmetry of h_μν, and the Newtonian relation h_00 = −κ ρ with κ = 8φ⁵. Anyone auditing the linearized-emergence step from ledger defects to geometry would cite it. The structure is a pure interface; the inhabiting instance simply wires the two already-proved component lemmas.
Claim. A certificate asserting that for every J-cost defect field $d$ and radial parameter $r$, the induced metric perturbation $h_{\mu\nu}(d,r)$ is symmetric ($h_{ij}=h_{ji}$), and its time-time component obeys $h_{00}=-\kappa_{\mathrm{RS}}\,\rho_d(r)$ where $\kappa_{\mathrm{RS}}=8\phi^5$ and $\rho_d$ is the defect density of $d$.
background
Module setting is Step 2 of the RS gravity stack: spacetime geometry in the weak-field limit is read off from the distribution of ledger defects. Each voxel carries a nonnegative J-cost $J(x)=\tfrac12(x+x^{-1})-1$; a region of high defect density is treated as strain in the ledger, and that strain sources the metric perturbation via $g_{\mu\nu}=\eta_{\mu\nu}+h_{\mu\nu}$.
A DefectField is a nonnegative density $\rho:\mathbb{R}^3\to\mathbb{R}{\ge 0}$. The map metric_perturbation_from_defect builds a symmetric rank-2 tensor whose diagonal entries equal $-\kappa{\mathrm{RS}}\rho$ and whose off-diagonal entries vanish, with coupling $\kappa_{\mathrm{RS}}=8\phi^5$ taken from ZeroParameterGravity (derived, not fitted). In the Newtonian limit this is the standard $h_{00}=-2\Phi$ with Poisson source $\nabla^2\Phi=\kappa\rho$.
Linearized GR conventions in the module: $h$ must be symmetric; the defect density plays the role of $T^{00}$.
proof idea
No proof body: this is a structure (certificate interface), not a theorem. It declares two fields that any inhabiting instance must supply: (i) pointwise symmetry of the components of metric_perturbation_from_defect, and (ii) the identity that the $(0,0)$ component equals $-\kappa_{\mathrm{RS}}$ times the defect density. Both obligations are discharged downstream by the one-line constructor metric_from_defect_cert, which plugs in the already-proved lemmas metric_perturbation_symmetric and perturbation_proportional_to_kappa.
why it matters
Closes the certificate layer of "metric from defect" so downstream gravity results can assume symmetry and the $\kappa$-proportional Newtonian source without reopening the definitions. The sole direct consumer is metric_from_defect_cert, which inhabits the structure. Framework landmarks: $\kappa=8\phi^5$ is the RS Einstein coupling from ZeroParameterGravity; the construction sits on the T5 J-cost and the $\phi$-ladder constants. It does not yet reach the full linearized EFE or harmonic-gauge wave operator; those are later steps that will quote this certificate for the algebraic shape of $h_{\mu\nu}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.