canonicalWeakFieldData_offDiag_component_match
plain-language theorem explainer
For any incidence-consistent 3D triangulation, off-diagonal entries of the canonical weak-field bilinear coefficient matrix equal the negatives of the independent dual weights on distinct vertex pairs. Discrete-gravity workers cite this when packaging incidence data into a concrete Regge component comparison. The argument is a definitional rewrite of the bilinear coefficient, then the geometric off-diagonal Hessian identity.
Claim. Let $K$ be an incidence-consistent 3D triangulation and let $i,j$ be distinct vertices of $K$. Then the bilinear coefficient of the canonical weak-field data built from $K$ at $(i,j)$ equals the negative of the independent dual weight of that pair: $\mathrm{bilin}(W_{\mathrm{can}})_{ij} = - w_{\mathrm{dual}}(i,j)$.
background
This module separates the independent dual-weight construction from the weak-field coefficient matrix and records the comparison that turns the geometric Regge computation into a concrete component comparison.
A 3D triangulation $K$ carries vertices, edges, and hinges with incidence data. Incidence consistency requires those relations to be coherent. From such data one builds canonical weak-field data (a bilinear coefficient matrix on vertices) and independent dual weights (a symmetric weight on vertex pairs dual to the Regge action).
Upstream geometry already proves that off-diagonal entries of the canonical Regge Hessian equal the negatives of the canonical dual weights: $\mathrm{Hess}_{ij}=-w(i,j)$ for $i\neq j$. The present statement is the gravity-side packaging of that identity under the weak-field data constructor from incidence.
proof idea
Short term-mode proof. Rewrite the left-hand side by the lemma that the bilinear coefficient of canonical weak-field data of incidence is the canonical Regge Hessian. Then apply the geometric identity that the off-diagonal canonical Regge Hessian equals the negative dual weight (proved by unfolding the Hessian and simplifying with $i\neq j$). No further arithmetic is needed; the dual-weight side matches by construction of the consistent dual-weight package.
why it matters
Feeds the concrete component comparison of incidence, which packages weak-field data, dual weights, and this off-diagonal match into a single comparison structure. That structure is the module's final Regge component comparison target: it turns the genuine Regge Hessian into the form required by the gravity-side component theorem.
In the Recognition Science gravity program, matching weak-field bilinear coefficients to dual weights is the discrete-geometry step linking Regge calculus on 3D triangulations to the continuum weak-field limit. It sits downstream of the incidence-consistent dual-weight construction. It does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or RS-native constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$); those enter only if the continuum limit is later identified with RS gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.