is
plain-language theorem explainer
EdgeLengthFromPsi.is supplies the map from recognition potential ψ on simplices to edge-length field L_e together with the linearization hypothesis that equates J-cost Dirichlet energy to the Regge action. A discrete-gravity researcher would cite it to convert the tautological bridge in ContinuumBridge into a genuine theorem. The current implementation is a sorry stub awaiting discharge of the named linearization hypothesis.
Claim. Let ε_i = ln ψ(σ_i) be the log-potential on simplices. Under the Regge-deficit linearization hypothesis, the J-cost action equals (1/κ) times the Regge action, where κ = 8 φ^5 and the linearized deficit angles are linear combinations of differences ε_i − ε_j.
background
The module works inside a finite ledger of n simplices whose edges carry a symmetric non-negative adjacency matrix. A log-potential assignment ε : Fin n → ℝ is defined by ε i = ln ψ(σ_i); this object already appears in the Laplacian action of ContinuumBridge. The module doc states that ContinuumBridge proves jcost_action = (1/κ) regge_action only by defining the Regge side as κ times the Laplacian side, which is tautological until the map from ψ to actual edge lengths L_e is supplied together with the linearization rule.
proof idea
The proof is a sorry stub. The intended discharge is either an algebraic identity obtained by unfolding the definitions of jcost_action and regge_action or an application of the ReggeDeficitLinearizationHypothesis once that Prop is proved from the cited Regge-calculus literature.
why it matters
The declaration packages the missing geometric map required by Theorem 5.1 (field-curvature identity) of the Gravity from Recognition draft. It feeds downstream results in Action.EulerLagrange (Christoffel symbols and geodesic equations) and in Acoustics (optimal T60 and hearing-loss penalties). The open question it touches is explicit verification of the linearization hypothesis via Cayley-Menger determinants or the classical references Piran-Williams 1986 and Cheeger-Müller-Schrader 1984.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.