IndependentDualWeights
plain-language theorem explainer
Independent dual weights on a finite 3D Regge triangulation are a symmetric, nonnegative real assignment to ordered vertex pairs. They are pure geometric data, not obtained by negating the weak-field Regge coefficient matrix. Anyone comparing the Regge Hessian off-diagonals to hinge/incidence geometry cites this bundle. The declaration is a structure package: three fields, no proof obligations beyond the field types.
Claim. Fix a finite 3D Regge triangulation $K$ with vertex set $V$. An independent dual-weight assignment on $K$ is a map $w:V\times V\to\mathbb{R}$ such that $w(i,j)=w(j,i)$ for all vertices $i,j$ and $w(i,j)\ge 0$ for all $i,j$.
background
The ambient setting is the final Regge component-comparison target: separate geometric dual weights from the weak-field coefficient matrix, then prove they match off-diagonal (up to sign) and that the matrix obeys the Schläfli row-sum identity.
A Triangulation3D is a finite abstract 3D Regge complex: vertex/edge/tetrahedron counts, edge endpoint pairs, and four vertices per tetrahedron, together with nondegenerate squared-edge data on each tet. Dual weights live on unordered vertex pairs and encode hinge/incidence geometry of that complex.
The point of packaging symmetry and nonnegativity alone is to keep the dual side independent of the Regge Hessian. Downstream constructions fill weight from incidence hinge weights or from the canonical geometry-layer dual weight on an incidence-consistent chart; the comparison structure then asserts equality with the negated bilinear coefficients.
proof idea
No proof body: this is a structure definition. It packages a real bilinear form on the finite vertex index type together with two propositional fields (symmetry and nonnegativity). Inhabitants are built later by supplying an explicit weight function and discharging those two properties from geometry-layer lemmas.
why it matters
This is the dual half of the concrete component-comparison package. ConcreteComponentComparison pairs weak-field Regge data with an IndependentDualWeights witness and requires off-diagonal match bilinearCoefficient W i j = - dual.weight i j plus the Schläfli row sum. Two constructors feed it: incidence hinge weights under an incidence-geometry hypothesis, and canonical dual weights under incidence consistency.
In the broader gravity thread this keeps the geometric side of the 3D Regge component theorem cleanly factored from the Hessian side, so the comparison theorem is a genuine equality of two independently defined objects rather than a tautology from defining dual weights as negated coefficients. It sits in the discrete-gravity / Regge-calculus layer that supports continuum and weak-field limits in the Recognition gravity stack; it does not itself invoke the T0–T8 forcing chain or the J-cost identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.