weak_field_condition
plain-language theorem explainer
The weak-field regime is the pointwise bound that defect density stays strictly below the reciprocal of the RS gravitational coupling κ = 8φ⁵. Anyone deriving linearized metric perturbations from ledger defects cites this predicate as the hypothesis that |h| remains small. It is a pure definition of a Prop, not a proved statement.
Claim. A defect field $d$ (nonnegative density $\rho:\mathbb{R}^3\to\mathbb{R}$) is in the weak-field regime when $|\rho(x,y,z)| < 1/\kappa_{\mathrm{RS}}$ at every point, where $\kappa_{\mathrm{RS}} = 8\varphi^5$ is the Recognition Science Einstein coupling.
background
Module Step 2 builds the metric perturbation $h_{\mu\nu}$ from the J-cost defect field on the lattice. Each voxel carries a nonnegative defect $J(x)=\tfrac12(x+x^{-1})-1$; high defect density is ledger strain that curves emergent spacetime via $g=\eta+h$.
A DefectField is a nonnegative density $\rho:\mathbb{R}^3\to\mathbb{R}$. Zero density means flat space. The coupling is the derived constant $\kappa_{\mathrm{RS}}=8\varphi^5$ from ZeroParameterGravity (not a free parameter). In the Newtonian limit one takes $h_{00}=-2\Phi$ and $h_{ij}=-2\Phi\delta_{ij}$ with $\Phi$ sourced by $\rho$, and $h$ proportional to $\kappa\rho$.
Linearized GR needs $|h_{\mu\nu}|\ll 1$. The doc-comment states the matching density bound: $\kappa\rho\ll 1$. This definition packages that inequality as a reusable hypothesis.
proof idea
Definitional: the predicate is the universal quantification $\forall x,y,z,;|d.\mathrm{density},x,y,z|<1/\kappa_{\mathrm{RS}}$. No tactics or lemmas; the body is the Prop itself. Downstream proofs rewrite the metric components via proportionality to $\kappa$ and discharge the bound with this hypothesis plus $\kappa>0$.
why it matters
Feeds the theorem weak_field_small_perturbation, which concludes that the $(0,0)$ component of the defect-sourced metric perturbation has absolute value strictly less than 1 under this hypothesis. That is the formal bridge from ledger defect density to the linearized-gravity small-$h$ regime in the MetricFromDefect development.
In the broader RS gravity picture, curvature is not postulated: it is induced by J-cost defects with fixed coupling $\kappa=8\varphi^5$ (tied to the $\varphi$-ladder and zero-parameter gravity). The weak-field condition is the precise density threshold that keeps the emergent geometry inside the linear approximation, so Newtonian and post-Newtonian comparisons remain valid. It does not itself force $D=3$ or the eight-tick structure; those sit upstream in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.