trace
plain-language theorem explainer
Defines the Euclidean trace of a spatial symmetric 3-tensor as the sum of its three diagonal entries. Used throughout the weak-field metric-from-defect construction whenever the linearized GR trace (and trace-reversed perturbation) is needed. The body is a direct three-term sum on the stored components.
Claim. For a symmetric spatial 2-tensor $t$ in three dimensions, $\mathrm{tr}(t) := t_{00} + t_{11} + t_{22}$.
background
Module Step 2 builds the metric perturbation $h_{\mu\nu}$ from the J-cost defect field on the lattice. In the weak-field picture each voxel carries $J(x)=\tfrac12(x+x^{-1})-1\ge 0$; nonzero defect density sources curvature via $g=\eta+h$, with $h$ proportional to integrated defect density and $\kappa=8\varphi^5$ from ZeroParameterGravity.
A SymmetricTensor D is a symmetric matrix of reals indexed by Fin D. Here $D=3$ is the spatial slice (indices ${0,1,2}$ in the Fin encoding). Linearized GR needs the ordinary trace of $h$ to form the trace-reversed perturbation $\bar h = h - \tfrac12\eta,\mathrm{tr}(h)$ that enters the harmonic-gauge wave equation $\nabla^2\bar h=-2\kappa T$, with defect density identified as $T^{00}$.
Upstream cost and defect machinery (J-cost, ledger defect functional, recognition-event cost) supply the scalar source; this definition only packages the spatial contraction used when that source is turned into a tensor perturbation.
proof idea
Pure definition: evaluate the three diagonal components of the stored matrix and add them. No lemmas, no tactics; the symmetry proof field of SymmetricTensor is unused because the trace only reads the diagonal.
why it matters
Local sibling theorems (metric_perturbation_from_defect, metric_perturbation_symmetric, weak_field_condition, MetricFromDefectCert) need a concrete spatial trace to match the linearized-GR convention stated in the module doc. Downstream, cost and gauge-orbit material (le_of_trace_le, cost_at_neg, nontrivial_is_signedPower, GaugeOrbitIsSignOrOddPowerFamily) and cosmogenesis trace certificates reuse the same contraction language when comparing principal-value traces $v+v^{-1}$ or certifying ledger traces; the gravity module is the geometric home of the 3D spatial case.
In the Recognition forcing chain this sits under emergent geometry after T5 (J-uniqueness) and T8 ($D=3$): once spatial dimension is fixed, the trace is the unique isotropic contraction that feeds the weak-field Einstein equation with defect density as stress-energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.