rs_edge_length_pos
plain-language theorem explainer
Positivity of the RS edge length is established whenever the lattice spacing a and metric component g are both strictly positive. Discrete gravity researchers in the Recognition Science programme cite the result to guarantee that all simplicial edge lengths remain in the positive reals during lattice constructions. The argument reduces immediately to the standard multiplication-positivity lemma applied to the input hypotheses together with the square-root positivity fact.
Claim. Let $a > 0$ and $g > 0$. Then $0 < a sqrt(g)$, where $a sqrt(g)$ is the edge length obtained from the J-cost defect field via the RS mapping $L_e = a sqrt(g_component)$.
background
The ReggeCalculus module formalizes exact nonlinear Regge calculus on the RS lattice, replacing the linearized deficit-angle ansatz with the full simplicial machinery. Curvature concentrates on codimension-2 hinges, and the Regge action is the sum over hinges of area times deficit angle. Edge lengths are extracted from the defect functional, which equals the J-cost J(x) for positive arguments, via the explicit mapping $L_e = a sqrt(g_component)$ where g_component encodes the metric perturbation induced by defect density.
proof idea
The proof is a one-line wrapper that applies the mul_pos lemma to the hypothesis ha together with the result of Real.sqrt_pos.mpr applied to hg.
why it matters
The result secures the basic positivity requirement for constructing the Regge action on the RS lattice and for passing to the continuum limit in which the discrete action recovers the Einstein-Hilbert term with stiffness kappa equal to 8 phi^5. It closes a foundational well-posedness check consistent with the forcing chain landmarks T5 through T8 and the Recognition Composition Law. No direct downstream uses appear in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.