EdgeLengthField
plain-language theorem explainer
The EdgeLengthField structure encodes a conformal edge-length assignment on an n-vertex graph via base spacing a > 0 and a symmetric positive length matrix L. Researchers formalizing discrete gravity or the Regge action in Recognition Science cite it when mapping scalar log-potentials to geometric edge data for the field-curvature identity. The declaration is a plain structure record with no proof obligations, directly supplying the data type used by recoverEps and cubic deficit functions.
Claim. A conformal edge-length field on an $n$-vertex graph is a record consisting of a base spacing $a > 0$ together with a function $L : [n] × [n] → ℝ$ satisfying $L(i,j) = L(j,i) > 0$ for all $i,j$, where the canonical form is $L(i,j) = a · exp((ε_i + ε_j)/2)$ for vertex log-potentials ε (reducing to the constant $a$ when ε ≡ 0).
background
This module supplies the map from a scalar recognition-potential field ψ on 3-simplices to an edge-length field L_e on the graph, closing the identification between J-cost Dirichlet energy and the linearized Regge action. The EdgeLengthField records the base spacing together with the length matrix obeying symmetry and positivity; the canonical ansatz is L_{ij} = a · exp((ε_i + ε_j)/2), the standard conformal rescaling convention for identifying the recognition potential with a scalar metric perturbation. The local theoretical setting is the Gravity from Recognition draft Theorem 5.1 (field-curvature identity with coupling κ = 8 φ^5), where the J-cost action is to match the Regge action once the linearization hypothesis is discharged.
proof idea
The declaration is a structure definition that directly records the base spacing, its positivity proof, the length function, and the two axioms of symmetry and positivity. No lemmas or tactics are applied; it functions as the data type for downstream operations such as recoverEps (which extracts ε_i via log(L_{ii}/a)) and the cubic deficit calculations.
why it matters
This definition supplies the geometric data type required to make the field-curvature identity a genuine theorem rather than a tautology. It is used by the cubic deficit discharge theorems (cubicArea, cubicDeficit, recoverEps) and by the cubic simplicial equivalence results. It fills the explicit gap identified in the module documentation between the J-cost action and the Regge action, modulo the ReggeDeficitLinearizationHypothesis. In the broader framework it supports the emergence of spatial geometry (D = 3) from the recognition potential on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.