DefectField
plain-language theorem explainer
Packages a nonnegative scalar field on R^3 as the J-cost defect density that sources curvature in Recognition Science gravity. Downstream metric-perturbation constructions take this as input and build the weak-field h_mu_nu proportional to kappa times density. The structure is a plain data bundle: a density map plus a pointwise nonnegativity proof obligation.
Claim. A defect field is a pair $(\rho, p)$ where $\rho : \mathbb{R}^3 \to \mathbb{R}$ is a scalar density and $p$ asserts $\rho(x,y,z) \ge 0$ at every point. In RS this $\rho$ is the J-cost defect density; vanishing $\rho$ means flat space.
background
Module Step 2 builds linearized gravity from ledger defects. Each voxel carries a J-cost $J(x) = \tfrac12(x+x^{-1})-1 \ge 0$; regions of high defect density strain the ledger and curve the emergent metric $g = \eta + h$. The coupling is $\kappa = 8\varphi^5$ from ZeroParameterGravity.
Upstream, defect is identified with $J$ on positive reals (LawOfExistence), spatial dimension is forced to $D=3$ (T8/GapDerivation, AlphaDerivation), and the per-step weight $\rho=\varphi^{-1}$ appears in MeasureForcing. Here the continuum density field is the continuum stand-in for that discrete defect source: in RS it plays the role of $T^{00}$ in the linearized Einstein equation.
The structure only records the density map and nonnegativity. Poisson sourcing $\nabla^2\Phi = \kappa,\rho$ and the Newtonian ansatz $h_{00}=-2\Phi$, $h_{ij}=-2\Phi\delta_{ij}$ live in sibling definitions that consume a DefectField.
proof idea
No proof body: this is a structure declaration. It bundles a real-valued ternary density function with a universal nonnegativity hypothesis. Downstream defs pattern-match on the density field and use the nonnegativity witness only when needed for inequalities; symmetry and proportionality lemmas about $h_{\mu\nu}$ do not reopen the structure definition itself.
why it matters
This is the typed carrier for the claim that spacetime curvature is sourced by J-cost defect density rather than by an independent stress-energy tensor. Every sibling in MetricFromDefect consumes it: metric_perturbation_from_defect builds the diagonal $h_{ij}\propto -\kappa\rho$; zero_defect_flat_space shows vanishing density yields $h=0$; perturbation_proportional_to_kappa pins the $\kappa=8\varphi^5$ factor; weak_field_condition / weak_field_small_perturbation encode $|h|\ll 1$ as $\kappa\rho\ll 1$.
In the forcing chain this sits after T5 (J uniqueness), T6 ($\varphi$), and T8 ($D=3$), and after the zero-parameter gravity coupling. It is definitional scaffolding for the RS reading of linearized GR: defect density IS $T^{00}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.