flat_metric_spatial
plain-language theorem explainer
The spatial part of the flat Minkowski background in three dimensions, realized as the Kronecker delta packaged as a symmetric 2-tensor. Anyone assembling weak-field metric perturbations from J-cost defect density cites this as the unperturbed geometry eta_ij. The definition sets diagonal components to 1 and off-diagonal to 0; symmetry is a one-line simp on equality commutativity.
Claim. The flat spatial metric $\eta_{ij}$ in three dimensions is the Kronecker delta $\delta_{ij}$: components equal $1$ when $i=j$ and $0$ otherwise, forming a symmetric real $3\times 3$ 2-tensor.
background
This module (Step 2 of the gravity chain) builds the metric perturbation $h_{\mu\nu}$ from the J-cost defect field on the lattice. In the weak-field picture, $g_{\mu\nu}=\eta_{\mu\nu}+h_{\mu\nu}$, with $h$ proportional to integrated defect density and proportionality constant $\kappa=8\phi^5$ from ZeroParameterGravity. Defect density plays the role of the stress-energy source $T^{00}$.
A SymmetricTensor D is a real bilinear form on $\mathrm{Fin},D$ forced to be symmetric in its two indices. For the spatial sector one takes $D=3$ (indices ${1,2,3}$ in the usual $3+1$ split). The companion trace sums the three diagonal entries.
The J-cost itself is $J(x)=\frac12(x+x^{-1})-1\ge 0$; vanishing defect density is the flat-space baseline against which curvature is measured.
proof idea
Structure instance, not a tactic proof of a proposition. Components are defined pointwise by the Kronecker rule if i = j then 1 else 0. The required symmetry field is discharged by intro i j; simp [eq_comm], which rewrites the two sides of the equality under swapped indices and closes by definitional equality of the conditional.
why it matters
Supplies the background $\eta_{ij}$ that every subsequent construction in MetricFromDefect perturbs. Downstream siblings such as metric_perturbation_from_defect, zero_defect_flat_space, and weak_field_small_perturbation treat this object as the unperturbed spatial geometry: zero defect yields exactly this flat tensor, and the linearized Einstein equation is written relative to it.
In the Recognition forcing chain, spatial dimension $D=3$ is forced at T8, so fixing the tensor rank to 3 is not an arbitrary modeling choice. The module also ties the source strength to $\kappa=8\phi^5$, connecting ledger strain to the same $\phi$ that appears in the mass ladder and the eight-tick octave. No parent theorem currently lists this def in used_by, but it is the reference geometry for the whole weak-field certificate MetricFromDefectCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.