rs_conservation
plain-language theorem explainer
The RS Einstein-field data package obeys the conservation-law side condition because its coupling is κ = 8φ⁵ > 0. Anyone assembling the full GR certificate cites this. The proof is a short positivity check after unfolding the data and κ definitions.
Claim. The Recognition Science Einstein-field data satisfy the conservation-law predicate: with coupling $\kappa = 8\phi^{5}$, one has $\kappa \neq 0$ (equivalently $\kappa > 0$).
background
Module FullEFE derives the sourced nonlinear Einstein equations from the RS discrete ledger, conditional on Regge-to-Einstein-Hilbert continuum convergence. The eight-step chain ends with Bianchi identity implying $\nabla^{\mu}T_{\mu\nu}=0$ and with a derived coupling $\kappa=8\phi^{5}$ (not fitted).
In RS units the golden ratio $\phi$ is forced as the self-similar fixed point (T6); the same $\phi$ fixes native constants such as $\hbar=\phi^{-5}$ and $G=\phi^{5}/\pi$. Here $\kappa=8\phi^{5}$ is the Einstein coupling packaged in rs_efe_data. The conservation-law predicate on that package is the algebraic side condition that $\kappa$ is nonzero, so the contracted Bianchi identity can enforce stress-energy conservation once matter is coupled.
Upstream cost and recognizer material (J-cost on recognition events, multiplicative recognizers) sits behind the lattice action that produces Regge calculus and eventually $\kappa$; this lemma only needs the explicit $\phi$-formula and $\phi>0$.
proof idea
Term-mode proof. Unfold the conservation-law predicate together with the RS EFE data package and the definition $\kappa=8\phi^{5}$. Goal reduces to $8\phi^{5}\neq 0$. Apply ne_of_gt to a strict positivity witness: mul_pos of the literal $0<8$ (norm_num) and pow_pos phi_pos 5 (positive base to a natural power). No Bianchi or continuum argument is invoked.
why it matters
Closes the conservation slot of the master Full GR certificate: full_gr_certificate sets conservation := rs_conservation alongside dimension, derived-$\kappa$, and $\kappa>0$ fields. In the module chain this is step 7-8 material: Bianchi gives $\nabla^{\mu}T_{\mu\nu}=0$ once the coupling is nonzero, and $\kappa=8\phi^{5}$ is the RS-native value (primer constants, T6 $\phi$).
The certificate doc lists "kappa > 0 (conservation)" among the unconditionally proved items, separate from still-external full nonlinear Regge$\to$EH convergence. Without this positivity fact the sourced EFE package would not be admissible as a conservation-compatible Einstein theory inside the RS ledger story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.