kappa_einstein_pos
plain-language theorem explainer
The lemma establishes that the Einstein coupling κ = 8πG/c⁴ is strictly positive in RS-native units. Researchers deriving the cubic bridge chain or the octave duality between ħ and gravitational coupling cite it to keep the linearization of the Regge action well-defined. The term-mode proof unfolds the definition and chains div_pos with mul_pos, Real.pi_pos, G_pos, and pow_pos on c_pos.
Claim. $0 < κ$ where $κ := 8πG/c^4$ is the Einstein gravitational coupling in Recognition Science units with $c=1$ and $G=φ^5/π$.
background
The Constants module sets the RS time quantum to the tick τ₀ = 1. Upstream lemmas supply c_pos (0 < c, speed of light in voxel/tick) and G_pos (0 < G). The definition kappa_einstein := 8 * Real.pi * G / (c^4) follows from the RS relation G = φ^5 / π and yields the value 8φ^5. The module isolates these constants from the quarantined CODATA block.
proof idea
The term proof unfolds kappa_einstein, applies div_pos to the fraction, then mul_pos to the numerator (norm_num for the constant 8, Real.pi_pos for π, G_pos for G), and pow_pos on the denominator using c_pos.
why it matters
kappa_einstein_pos is invoked by bridge_chain_complete to discharge ReggeDeficitLinearizationHypothesis and by hbar_eq_eight_div_kappa to obtain ħ = 8/κ. It closes the constants block that feeds the cubic bridge from RCL through J-uniqueness and φ to the Einstein equations in the simplicial ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.