singletonHinge_product
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.
claimLet $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 in Recognition Science
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$.
scope and limits
- Does not address higher-order $O(ε^3)$ corrections to the genuine Regge deficit.
- Does not apply to hinge data containing more than one edge.
- Does not establish global positivity or convergence of the summed functional.
- Does not depend on the concrete geometry beyond the singleton hinge structure.
formal statement (Lean)
179theorem singletonHinge_product {n : ℕ} (a : ℝ) (ha : 0 < a)
180 (ε : LogPotential n) (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
181 cubicArea (conformal_edge_length_field a ha ε) (singletonHinge i j w hw) *
182 cubicDeficit (conformal_edge_length_field a ha ε) (singletonHinge i j w hw)
183 = (jcost_to_regge_factor / 2) * w * (ε i - ε j) ^ 2 := by
proof body
Term-mode proof.
184 rw [cubicArea_singleton, cubicDeficit_singleton,
185 recoverEps_conformal a ha ε i, recoverEps_conformal a ha ε j]
186 ring
187
188/-! ## §5. The cubic hinge list via `Finset.univ.toList`
189
190Enumerate one hinge per ordered pair `(i, j) ∈ Fin n × Fin n`. Pairs with
191`i = j` contribute 0 because `(ε_i − ε_i)² = 0`. -/
192
193/-- The hinge list: one singleton hinge per ordered pair. -/