cubicArea
cubicArea supplies the hinge-area term in the linearized Regge action for the cubic lattice. It is cited by proofs discharging the ReggeDeficitLinearizationHypothesis and by the construction of cubicDeficitFunctional. The definition proceeds by case analysis on the hinge datum: it returns half the normalized J-cost factor times the edge weight when the hinge is a singleton edge and zero otherwise.
claimLet $L$ be an edge-length field on $n$ vertices and $h$ a hinge datum. Define the cubic area by $A(h) = (8phi^5/2)w$ if $h$ consists of a single edge with weight $w$, and $A(h)=0$ otherwise.
background
In the Recognition Science framework the cubic lattice discharge module constructs a deficit-angle functional realizing the leading-order Regge linearization. EdgeLengthField is the structure recording conformal edge lengths derived from log-potentials, with canonical form $L_{ij}=a exp((eps_i+eps_j)/2)$. HingeDatum encodes a hinge as an edge list together with a weight function on those edges. The module discharges the linearization hypothesis for the RS-canonical cubic lattice by pairing the deficit (cubicDeficit) with this area. Upstream, jcost_to_regge_factor supplies the normalization kappa=8 phi^5 that matches J''(1)=1 to the Regge coefficient 1/(8 pi G).
proof idea
The definition is a direct match on the edges field of the hinge datum. When the list is exactly one pair (i,j) it returns jcost_to_regge_factor times the weight of that pair divided by two; all other cases return zero. This is the one-line case distinction implementing the area contribution for singleton hinges.
why it matters in Recognition Science
cubicArea is the area component of the DeficitAngleFunctional used in regge_sum_cubicHinges, which shows the Regge sum equals (kappa/2) times the weighted sum of squared potential differences. It fills the area slot in the discharge of the ReggeDeficitLinearizationHypothesis from EdgeLengthFromPsi, enabling the paper's Theorem 5.1 (field-curvature identity) to be proved exactly for the leading-order functional. The construction is Phase A of the four-phase program; higher-order corrections are deferred to Phase D.
scope and limits
- Does not incorporate higher-order cubic or quartic corrections to the Regge deficit.
- Does not apply to non-singleton hinges or general simplicial complexes.
- Does not compute the full curvature scalar, only the hinge-area contribution to the action.
- Does not depend on the specific value of the base spacing beyond the conformal field.
formal statement (Lean)
122def cubicArea {n : ℕ} (_L : EdgeLengthField n) (h : HingeDatum n) : ℝ :=
proof body
Definition body.
123 match h.edges with
124 | [(i, j)] => jcost_to_regge_factor * h.weight (i, j) / 2
125 | _ => 0
126
127/-- Value of `cubicDeficit` on a singleton hinge. -/