rs_edge_length
plain-language theorem explainer
Edge lengths on the RS lattice are obtained by scaling the base spacing a with the square root of the metric component g_component. This construction is invoked when proving that lengths stay positive for positive inputs in discrete gravity calculations. The definition reduces to a direct product with the real square root.
Claim. The RS edge length is given by $L_e = a sqrt(g)$, where $a$ is the lattice spacing and $g$ is the metric component fixed by the J-cost defect field.
background
The module develops Regge calculus for the Recognition Science lattice, treating spacetime as a piecewise flat simplicial complex on Z^3 x Z. Curvature resides at codimension-2 hinges, and the action sums area times deficit angle over all hinges. Edge lengths follow from the J-cost defect field that determines the perturbation h in the metric g = eta + h.
proof idea
The definition is a one-line algebraic expression: the spacing multiplied by the square root of the metric component.
why it matters
This definition supplies the lengths needed to evaluate the Regge action in the discrete gravity sector. It is invoked by the positivity theorem for edge lengths, whose documentation states that the RS Regge action inherits kappa = 8 phi^5 from the defect-to-metric mapping. Within the framework it realizes the defect-to-metric map, supporting the passage to the continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.