SymmetricTensor
plain-language theorem explainer
A D-dimensional symmetric bilinear form packaged as a matrix of reals with the symmetry axiom built in. Gravity constructions in this module use it for the spatial flat metric, the defect-sourced perturbation h_ij, and the trace. The declaration is pure data: two fields, no proof obligations beyond the symmetry Prop.
Claim. A symmetric 2-tensor in $D$ dimensions is a map $T : \{0,\ldots,D-1\}^2 \to \mathbb{R}$ such that $T_{ij} = T_{ji}$ for all indices $i,j$.
background
This module builds linearized gravity from Recognition Science ledger defects. Each voxel carries a nonnegative J-cost $J(x) = \tfrac12(x+x^{-1})-1$; regions of high defect density source metric strain via $g = \eta + h$, with coupling $\kappa = 8\varphi^5$ from ZeroParameterGravity.
The ambient spatial dimension is the forced value $D = 3$ (T8 in the forcing chain; also T9 linking). Indices therefore run over a 3-element finite type. The structure is the minimal carrier for any spatial 2-tensor that must stay symmetric: the flat Euclidean $\eta_{ij} = \delta_{ij}$, the Newtonian perturbation $h_{ij}$, and their traces.
In the linearized GR convention used here, $h_{\mu\nu}$ is symmetric, the trace-reversed $\bar h$ enters the harmonic-gauge wave equation, and the RS defect density plays the role of $T^{00}$.
proof idea
No proof body: this is a structure declaration. It packages a component map Fin D → Fin D → ℝ together with the propositional field asserting symmetry under index swap. Inhabitants discharge symmetry by a one-line simp [eq_comm] (as in the flat metric and defect-sourced perturbation constructors).
why it matters
SymmetricTensor is the shared type for every spatial metric object in MetricFromDefect. Downstream, flat_metric_spatial builds $\eta_{ij} = \delta_{ij}$ as an instance on $D=3$; metric_perturbation_from_defect builds the diagonal Newtonian $h_{ij} \propto -\kappa,\rho$; and trace sums the three diagonal entries for the linearized trace-reversal step.
That chain is Step 2 of the gravity program: geometry emerges from J-cost defect density, with $\kappa = 8\varphi^5$ fixed by zero-parameter gravity. The structure enforces the GR requirement $h_{\mu\nu}=h_{\nu\mu}$ at the type level before any weak-field or Poisson identities are stated. It sits under the T8 forcing of $D=3$ and feeds the certification bundle MetricFromDefectCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.