cubicArea_singleton
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address hinges containing multiple edges.
- Does not compute the full nonlinear Regge deficit angle.
- Does not depend on the concrete form of the edge-length field beyond its type.
- Does not establish nonnegativity of the area functional.
Lean usage
rw [cubicArea_singleton, cubicDeficit_singleton]formal statement (Lean)
138theorem cubicArea_singleton {n : ℕ} (L : EdgeLengthField n)
139 (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) :
140 cubicArea L (singletonHinge i j w hw)
141 = jcost_to_regge_factor * w / 2 := by
proof body
Term-mode proof.
142 show (match (singletonHinge i j w hw).edges with
143 | [(i', j')] =>
144 jcost_to_regge_factor * (singletonHinge i j w hw).weight (i', j') / 2
145 | _ => 0) = _
146 rw [singletonHinge_edges]
147 simp only
148 rw [singletonHinge_weight]
149
150/-- `cubicArea` is nonnegative. -/