rs_conservation_holds
plain-language theorem explainer
The declaration establishes that the Recognition Science coupling constant equal to eight times phi to the fifth power is nonzero. Researchers verifying conservation of the stress-energy tensor in the derived gravity theory would cite this step to confirm the matter coupling axiom. The proof is a direct term-mode application of positivity for multiplication and exponentiation.
Claim. $8 phi^5 neq 0$
background
The stress-energy tensor is obtained by varying the matter action with respect to the metric. Conservation nabla^mu T_mu nu = 0 follows from the contracted Bianchi identity nabla^mu G_mu nu = 0 together with the Einstein field equations G_mu nu = kappa T_mu nu - Lambda g_mu nu, using metric compatibility nabla^mu g_mu nu = 0. The module proves Axiom 3 on matter coupling by showing the full chain reduces to kappa nabla^mu T_mu nu = 0 and hence the desired conservation when kappa is nonzero. The coupling is fixed at kappa = 8 phi^5 in the native units of the framework.
proof idea
The proof is a one-line term proof. It applies ne_of_gt to the product of two positive reals, where eight is shown positive by numerical normalization and phi to the fifth power is shown positive by the known positivity of phi.
why it matters
This supplies the kappa_nonzero field inside the stress_energy_cert certificate. It thereby closes the conservation chain that links the geometric Bianchi identity to matter conservation through the Einstein field equations. The step aligns with the framework derivation of constants from the single functional equation, where phi is the self-similar fixed point and the eight-tick octave fixes the coupling scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.