rs_kappa_pos
plain-language theorem explainer
rs_kappa_pos proves positivity of the RS Regge constant. Discrete gravity researchers cite it to confirm the sign of the effective gravitational coupling inherited from the defect-to-metric map. The proof is a one-line wrapper that unfolds the definition and applies mul_pos together with pow_pos on the known positivity of phi.
Claim. $0 < 8 phi^5$, where $phi$ denotes the golden-ratio fixed point of the Recognition Science forcing chain.
background
The ReggeCalculus module equips the RS lattice with exact simplicial geometry. Edge lengths derive from the J-cost defect field, and curvature concentrates on codimension-2 hinges via deficit angles. The constant rs_kappa is introduced so that the discrete Regge action $S_{Regge} = sum_h A_h delta_h$ reproduces the continuum Einstein-Hilbert term with coefficient $kappa/2$ in the long-wavelength limit.
proof idea
One-line wrapper that unfolds rs_kappa to the expression 8 * phi^5, then applies mul_pos (with 8 shown positive by norm_num) and pow_pos (using phi_pos) to conclude strict positivity.
why it matters
The result supplies the kappa_positive field inside regge_calculus_cert, which certifies the full Regge framework for the RS lattice. It aligns the discrete action with the continuum limit required by the T5-T8 forcing chain and the phi-ladder mass formula, ensuring the gravitational coupling remains positive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.