conformal_edge_length_flat
plain-language theorem explainer
The theorem asserts that the conformal edge length field reduces to the constant base spacing a whenever the recognition potential vanishes identically. Researchers deriving the flat-space limit of the J-cost Dirichlet energy from the Regge action would invoke it to confirm the vacuum configuration. The proof proceeds by direct unfolding of the field definition followed by simplification.
Claim. Let $n$ be a natural number, $a>0$ a real number, and $i,j$ indices in Fin $n$. Then the length between vertices $i$ and $j$ in the edge-length field induced by the zero recognition potential equals $a$.
background
The module supplies the map from a scalar recognition-potential field ψ on 3-simplices to an edge-length field L_e on edges. The conformal_edge_length_field is defined so that its value at the zero potential recovers the uniform spacing a. This closes the identification in the Gravity from Recognition draft between ψ and the geometric data needed for the Regge action, with coupling κ = 8·φ⁵. The local setting is the flat vacuum limit where the J-cost Dirichlet energy should match the linearized Regge action.
proof idea
The proof is a one-line wrapper. It unfolds the definition of conformal_edge_length_field and applies simp to reduce the expression at the zero function to the constant a.
why it matters
This declaration supplies the flat-space anchor for the field-curvature identity in the Gravity from Recognition draft, Theorem 5.1. It ensures that the zero-potential configuration reproduces the uniform lattice spacing before linearization is applied. The parent structure is the ReggeDeficitLinearizationHypothesis; once discharged, the J-cost action equals the Regge action with the stated coupling. It touches the open question of explicit verification of the linearization from Cayley-Menger determinants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.