rs_edge_length
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute dihedral angles or deficit angles from the lengths.
- Does not specify how the metric component g arises from the defect density.
- Does not extend to the full 4-simplex edge set or the complete action.
- Does not address convergence of the discrete action to the Einstein-Hilbert action.
Lean usage
theorem rs_edge_length_pos (a : ℝ) (g : ℝ) (ha : 0 < a) (hg : 0 < g) : 0 < rs_edge_length a g := mul_pos ha (Real.sqrt_pos.mpr hg)formal statement (Lean)
206noncomputable def rs_edge_length (a : ℝ) (g_component : ℝ) : ℝ :=
proof body
Definition body.
207 a * Real.sqrt g_component
208