independentDualWeightsOfConsistent
plain-language theorem explainer
From an incidence-consistent 3D Regge triangulation one obtains independent dual weights by summing canonical edge-pair incidence weights over all edges. Anyone assembling the weak-field Regge coefficient comparison cites this packaging. The construction is a structure instance that reuses the geometry-layer symmetry and nonnegativity lemmas for the canonical dual weight.
Claim. Given a finite 3D Regge triangulation $K$ that is incidence-consistent, the vertex-pair map $w(i,j) = \sum_e w_{\mathrm{edge}}(i,j;e)$ built from the canonical edge-pair incidence weights is an independent dual-weight assignment on $K$: $w(i,j)=w(j,i)$ and $w(i,j)\ge 0$ for all vertices $i,j$.
background
The module isolates independent dual-weight data from the weak-field coefficient matrix, then records the comparison that turns the geometric computation into a Regge component comparison. A Triangulation3D is a finite 3D Regge complex: vertex, edge, and tetrahedron counts, edge endpoint maps, and tetrahedron vertex maps, with nondegenerate squared-edge data on each tet.
Independent dual weights are a structure on vertex pairs: a real weight function that is symmetric and nonnegative. They are geometric data, not defined by negating a Regge coefficient matrix. The geometry layer supplies the canonical dual weight under an incidence-consistency hypothesis: for each vertex pair it sums the canonical edge-pair weight over all edges of $K$. Upstream lemmas already prove that this sum is symmetric and nonnegative.
proof idea
One-line structure constructor. The weight field is set to canonicalDualWeight K hK. Symmetry is discharged by canonicalDualWeight_symm, and nonnegativity by canonicalDualWeight_nonneg. No new arithmetic is performed here; the def only packages the geometry-layer dual weight into the independent-dual-weights interface required downstream.
why it matters
This packaging is the dual half of the concrete component comparison. Downstream, concreteComponentComparisonOfIncidence pairs canonical weak-field data with these dual weights and records the off-diagonal match. The match theorem states that the bilinear coefficient of the canonical weak-field data equals the negative of this dual weight on $i\neq j$.
In the Recognition gravity stack, that comparison is the bridge from incidence geometry of a 3D Regge triangulation to the component-level weak-field identity. The module doc frames the whole file as the final Regge component comparison target: separate dual weights from the coefficient matrix, then prove they match. Without this def, the comparison structure has no dual field to attach.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.