edgeLengthFromPsiCert
plain-language theorem explainer
The edge length certificate asserts that the conformal edge-length field induced by a log-potential satisfies the exact bridge between the J-cost Laplacian action and the Regge sum under the linearization hypothesis on deficit angles. Researchers deriving gravity from a recognition functional would invoke it to replace the tautological action equality with a geometrically grounded map from potential to edge lengths. The proof proceeds by term construction, supplying each field of the certificate structure via direct application of the curvature
Claim. Let $D$ be a deficit-angle functional, $a>0$, hinges a list of hinge data, $G$ a weighted ledger graph, and assume the Regge deficit linearization hypothesis holds. Then for every log-potential $ε$, the Laplacian action of $G$ on $ε$ equals $(1/jcost_to_regge_factor)$ times the Regge sum of $D$ on the conformal edge-length field generated by $a$ and $ε$. The certificate also asserts the flat Regge sum identity, the flat J-cost property, and the flat log-potential map.
background
The module supplies the map from the recognition potential $ψ$ (or its log $ε$) on 3-simplices to an edge-length field $L_e$ on the edges of a simplicial complex, closing the identification needed for the Regge action. A SimplicialLedger is a nonempty collection of 3-simplices forming a manifold covering. The J-cost is the Dirichlet energy of the recognition functional $J$, the Laplacian action is its quadratic form on log-potentials, and the Regge sum is the discretized curvature action summed over hinges. The ContinuumBridge module proves the action equality only by definition, rendering it tautological; this module supplies the missing geometric map and linearization rule packaged as the ReggeDeficitLinearizationHypothesis. Upstream results include the curvature identity under linearization and the flat Regge sum lemma.
proof idea
The proof is a term-mode record construction for the EdgeLengthFromPsiCert structure. It populates the bridge field by direct application of field_curvature_identity_under_linearization, the flat_regge field by regge_sum_flat_under_linearization, the flat_jcost field by laplacian_action_flat, and the psi_flat field by logPotentialOf_flat.
why it matters
This declaration completes the bridge from the recognition potential to the Regge action in the Gravity from Recognition draft, Theorem 5.1 (Field-Curvature Identity). It identifies the normalization factor with the Einstein coupling, showing that $κ$ is derived rather than fitted. In the Recognition Science framework it connects J-uniqueness (T5) and the forcing chain to the emergence of three-dimensional geometry and the gravitational constant. The linearization hypothesis remains open and must be discharged via Piran-Williams, Brewin, or Cheeger-Müller-Schrader before the identification becomes unconditional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.