metric_from_defect_cert
plain-language theorem explainer
Packages the two core properties of the RS metric perturbation into a single certificate: symmetry of h_ij and proportionality of h_00 to the J-cost defect density with factor kappa_rs. Gravity authors cite it when they need a single witness that the defect-to-metric map obeys linearized-GR bookkeeping. The proof is a pure structure constructor filling both fields from prior lemmas.
Claim. There exists a certificate asserting that, for every defect field $d$ and radius $r$, the metric perturbation $h$ built from $d$ is symmetric ($h_{ij}=h_{ji}$) and its time-time component satisfies $h_{00}=-\kappa_{\mathrm{RS}}\,\rho_d(r)$, where $\kappa_{\mathrm{RS}}$ is the RS gravitational coupling.
background
This module (Step 2 of the gravity chain) constructs the linearized metric perturbation $h_{\mu\nu}$ from the J-cost defect field on the lattice. Each voxel carries a nonnegative cost $J(x)=\tfrac12(x+x^{-1})-1$; regions of high defect density act as strain, and the emergent geometry is $g=\eta+h$ with $h$ proportional to that density.
The proportionality constant is $\kappa_{\mathrm{RS}}=8\phi^5$ from ZeroParameterGravity. In the linearized convention used here, $h$ must be symmetric and the source of the Poisson equation is identified with the defect density itself (playing the role of $T^{00}$).
The certificate structure MetricFromDefectCert records exactly those two algebraic obligations. Upstream lemmas already prove them separately: symmetry holds by construction of the symmetric-tensor carrier, and the $(0,0)$ component expands by definition to $-\kappa_{\mathrm{RS}}$ times density.
proof idea
Term-mode structure inhabitant. The two fields of the certificate are filled by direct application of the named lemmas: metric_perturbation_symmetric supplies the $\forall d,r,i,j$ symmetry identity, and perturbation_proportional_to_kappa supplies the $\forall d,r$ identity $h_{00}=-\kappa_{\mathrm{RS}}\rho_d$. No further rewriting or case analysis is required.
why it matters
Closes the local certificate for Step 2 of the RS gravity program: spacetime geometry emerges from ledger defects with the correct linearized bookkeeping. The coupling $\kappa_{\mathrm{RS}}=8\phi^5$ ties the construction to the zero-parameter gravity layer and, through $\phi$, to the forcing chain (T5 J-uniqueness, T6 golden fixed point). Downstream consumers (none yet wired in this graph) would use the certificate as a single hypothesis when deriving weak-field curvature or matching the Newtonian limit. It does not yet touch the full Einstein equation or strong-field regime; it only locks the algebraic skeleton of $h$ from defect density.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.