conformal_edge_length_field
plain-language theorem explainer
This definition supplies the canonical conformal map sending a log-potential assignment ε on n vertices to an edge-length field whose lengths are L_ij = a exp((ε_i + ε_j)/2). Workers on the Regge side of the Recognition Science bridge cite it when converting the J-cost Dirichlet energy into a linearized Regge sum. The construction is a direct structure literal that inherits symmetry from commutativity of addition and positivity from the exponential.
Claim. Let $a > 0$ be a base spacing and let $ε : Fin n → ℝ$ be a log-potential assignment. The conformal edge-length field is the structure with base spacing $a$, length function $L(i,j) = a · exp((ε_i + ε_j)/2)$, symmetry $L(i,j) = L(j,i)$, and positivity $L(i,j) > 0$.
background
The module supplies the missing map from a scalar recognition-potential field ψ on simplices to the edge lengths required for a Regge action. LogPotential is the abbrev Fin n → ℝ with ε_i = ln ψ(σ_i), the same object used by laplacian_action in ContinuumBridge. EdgeLengthField is the structure recording base_spacing, a symmetric positive length function on ordered pairs of vertices, and the two required proofs.
proof idea
One-line wrapper that applies the EdgeLengthField structure constructor. The length function is defined by the exponential formula, symmetry follows from ring on addition, and positivity follows from mul_pos ha (Real.exp_pos _).
why it matters
This definition supplies the explicit map from ψ to L_e that turns the tautological action equality in ContinuumBridge into the field-curvature identity. It is invoked directly by field_curvature_identity_einstein, flat_regge_sum_zero, bridge_chain_complete, and the cubic variants. In the Recognition framework it realizes the linearization step of Theorem 5.1 in the Gravity from Recognition draft, connecting the J-cost to the Regge sum under the Einstein coupling 8 φ^5. The remaining open question is discharge of ReggeDeficitLinearizationHypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.