kappa_einstein_pos
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 in Recognition Science
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.
scope and limits
- Does not compute the explicit value 8φ^5 (that follows from upstream constant derivations).
- Does not address empirical CODATA values (those live in the quarantined Codata submodule).
- Does not prove existence or uniqueness of solutions to the Einstein equations.
- Does not extend positivity to other couplings or dimensions beyond D=3.
Lean usage
rw [eq_div_iff (ne_of_gt kappa_einstein_pos)]formal statement (Lean)
459lemma kappa_einstein_pos : 0 < kappa_einstein := by
proof body
Term-mode proof.
460 unfold kappa_einstein
461 apply div_pos
462 · apply mul_pos
463 · apply mul_pos
464 · norm_num
465 · exact Real.pi_pos
466 · exact G_pos
467 · exact pow_pos c_pos 4
468
469/-!
470 ## CODATA / SI constants (quarantined)
471
472 The empirical SI/CODATA numeric constants live in
473 `IndisputableMonolith/Constants/Codata.lean` and are intentionally **excluded**
474 from the certified surface import-closure.
475
476 If you need them for numeric comparisons or empirical reports, import
477 `IndisputableMonolith.Constants.Codata` explicitly.
478-/
479
480/-- Minimal RS units used in Core. -/