singletonHinge_product
plain-language theorem explainer
The identity equates the product of cubic area and cubic deficit at a singleton hinge on the conformal edge-length field to (κ/2) w (ε_i − ε_j)^2. Researchers deriving the exact Regge sum over cubic hinges cite it when discharging the linearization hypothesis. The proof is a direct algebraic reduction that applies the singleton evaluations of area and deficit, recovers the potential values, and simplifies by ring.
Claim. Let $L$ be the conformal edge-length field induced by log-potential $ε$ on $n$ vertices with scale $a > 0$. For the singleton hinge between vertices $i$ and $j$ with weight $w ≥ 0$, the product of its area under $L$ and its deficit under $L$ equals $(κ/2) w (ε_i − ε_j)^2$, where $κ = jcost_to_regge_factor$.
background
In the cubic lattice setting a WeightedLedgerGraph on $n$ vertices carries nearest-neighbor weights. The conformal_edge_length_field constructs edge lengths from a LogPotential $ε : Fin n → ℝ$ via the recognition cost. cubicArea returns $(κ/2) · w$ on a singleton hinge and zero otherwise; cubicDeficit returns the squared potential difference on the same hinge. jcost_to_regge_factor is the constant $8 φ^5$ that matches the second derivative of the J-cost to the Regge normalization (from ContinuumBridge). The module discharges ReggeDeficitLinearizationHypothesis exactly for the quadratic truncation of the deficit, supplying the leading-order identity needed for the paper's Theorem 5.1.
proof idea
The proof is a one-line wrapper that rewrites the left-hand side with cubicArea_singleton and cubicDeficit_singleton, substitutes the recovered values via recoverEps_conformal at $i$ and $j$, and finishes with the ring tactic.
why it matters
This local identity is the building block for regge_sum_cubicHinges, which converts the total Regge sum over cubicHinges into $(κ/2)$ times the weighted sum of squared potential differences. It completes the exact linearization step in the discharge of ReggeDeficitLinearizationHypothesis, allowing the field-curvature identity of paper Theorem 5.1 to be invoked. Within Recognition Science it links the J-cost action (T5 J-uniqueness, RCL) to the Regge action on the cubic lattice with $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.