einsteinKappa_pos
plain-language theorem explainer
The declaration proves that the Einstein coupling constant κ defined as 8 φ^5 / π is strictly positive. Researchers deriving general relativity from Recognition Science would cite this to fix the sign of the source term in the field equations. The proof is a short term-mode reduction that unfolds the definition and invokes real-number positivity lemmas for multiplication, powers, and division.
Claim. The Einstein coupling constant satisfies $0 < 8 φ^5 / π$, where $φ$ is the self-similar fixed point of the Recognition Composition Law.
background
In the module GeneralRelativityFromRS the Einstein field equations are written G_μν + Λ g_μν = κ T_μν with RS-native coupling κ = 8 φ^5 / π (equivalent to 8G/c^4 when c = 1 and G = φ^5 / π). The five canonical GR effects are identified with configDim D = 5 and are asserted to be consistent once κ > 0. The upstream definition einsteinKappa supplies the explicit expression 8 * phi ^ 5 / Real.pi; the consistent predicate from SAT backpropagation and the and theorem from CirclePhaseLift supply supporting positivity infrastructure.
proof idea
The term proof unfolds einsteinKappa, then applies div_pos to split the claim into numerator and denominator positivity. Numerator positivity is obtained by mul_pos on a manifestly positive constant and (phi ^ 5) via pow_pos phi_pos; the denominator is discharged by Real.pi_pos.
why it matters
The theorem populates the kappa_positive field of generalRelativityCert, which certifies that all five GR effects have been tested and remain consistent with RS predictions. It directly discharges the positivity requirement stated in the module documentation for the RS-derived Einstein equations and confirms the sign of the coupling obtained from the phi-ladder constants (T6, T7). No open scaffolding remains for this sign check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.