cubicArea_singleton
plain-language theorem explainer
The declaration states that cubicArea applied to a singleton hinge datum returns exactly half the J-cost normalization factor times the hinge weight. Researchers discharging the Regge linearization hypothesis on the cubic lattice cite this when reducing area-deficit products at individual edges. The proof is a direct term reduction that substitutes the edge list and weight function of the singleton hinge into the match expression inside cubicArea.
Claim. Let $L$ be an edge-length field on $n$ vertices. For indices $i,j$ and weight $wgeq 0$, if $H$ is the singleton hinge datum carrying the ordered edge $(i,j)$ with that weight, then the cubic area of $H$ equals $frac{kappa w}{2}$, where $kappa=8phi^5$ is the normalization factor relating J-cost to the Regge action.
background
The cubic lattice discharge module constructs a deficit functional that realizes the leading-order Regge linearization: deficit at a hinge equals the squared log-potential difference, while area at the hinge is normalized by the J-cost factor. A singleton hinge datum is the basic building block that carries exactly one ordered edge together with its nonnegative weight. The J-cost to Regge factor is defined as $kappa:=8phi^5$, chosen so that the second derivative of the J-cost at unity matches the Regge normalization $1/(8pi G)$.
proof idea
The proof is a term-mode reduction. It rewrites the hinge datum via singletonHinge_edges to expose the singleton edge list, then applies singletonHinge_weight to substitute the explicit weight value, collapsing the match expression inside cubicArea directly to the scalar $kappa w/2$.
why it matters
This identity is invoked inside singletonHinge_product to obtain the exact area-deficit product $(kappa/2)w(eps_i-eps_j)^2$ on the conformal edge-length field. That product supplies the key term in cubic_linearization_discharge, which unconditionally establishes the ReggeDeficitLinearizationHypothesis for the cubic lattice and thereby completes Phase A of the program leading to the paper's Theorem 5.1 on the field-curvature identity. The construction sits inside the Recognition Science derivation of the Regge action from the J-uniqueness axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.