cubicArea_nonneg
plain-language theorem explainer
The cubic area functional is nonnegative for any edge length field and hinge datum on the simplicial ledger. A physicist linearizing Regge calculus on cubic lattices cites it to confirm the area term remains a valid positive measure in the deficit functional. The proof reduces by case analysis on the hinge edge list to nonnegativity of the J-cost normalization factor times the hinge weight.
Claim. For any natural number $n$, edge length field $L$ on $n$ vertices, and hinge datum $h$, the hinge area in the cubic deficit functional satisfies $0$ ≤ area of $L$ and $h$.
background
This declaration belongs to the module that discharges the Regge deficit linearization hypothesis for the RS-canonical cubic lattice. The cubic deficit functional implements the leading-order Regge linearization: deficit at a hinge is the squared log-potential difference, while area at the hinge is given by (κ/2) times the weight, with κ the J-cost normalization factor. The local theoretical setting is Phase A of the four-phase program to promote the draft paper's Theorem 5.1 (field-curvature identity) from a pattern-matching argument to a genuine Lean theorem. Upstream, the normalization factor is defined as 8 φ^5 and proved positive, supplying the key positivity ingredient.
proof idea
The proof unfolds cubicArea then cases on the hinge edge list. The empty list and lists of length two or more simplify directly to zero by simp. The single-edge case obtains the pair (i,j), then applies mul_nonneg to the nonnegativity of jcost_to_regge_factor (from le_of_lt on its positivity theorem) and the nonnegativity of the hinge weight.
why it matters
This supplies the area_pos field inside the cubicDeficitFunctional definition of the DeficitAngleFunctional. It completes the exact linearization identity for the leading-order functional on the cubic lattice, which is the content needed for the paper's Theorem 5.1 via field_curvature_identity_under_linearization. The result anchors the area term to the Recognition Science normalization κ = 8 φ^5 that matches J-cost action to Regge action, consistent with the phi-ladder and eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.