concreteComponentComparisonOfIncidence
plain-language theorem explainer
Packages canonical incidence-based weak-field Regge data and independent dual hinge weights into one concrete component comparison for any incidence-consistent 3D triangulation. Gravity workers proving the Regge Hessian component theorem cite this record. It is a structure constructor that wires four already-established pieces (weak-field data, dual weights, off-diagonal match, Schläfli row sum) into a single package.
Claim. For any 3D triangulation $K$ that is incidence-consistent, form a concrete component comparison whose weak-field Regge data $W$ is the canonical incidence/Laplacian second-order data on the vertices of $K$, whose dual weights are the independent dual weights of that incidence structure, whose off-diagonal bilinear coefficients satisfy $B_W(i,j)=-w_{\mathrm{dual}}(i,j)$ for $i\neq j$, and whose row sums obey the Schläfli identity.
background
This module finishes the 3D Regge component comparison target. It separates the independent dual-weight construction from the weak-field coefficient matrix, then records the package that turns that geometric computation into a component comparison.
A ConcreteComponentComparison on a triangulation $K$ is a four-field record: weak-field Regge data $W$ on the vertex set, an independent dual-weight assignment on edge pairs (hinges), the matching identity that every off-diagonal bilinear coefficient of $W$ equals the negative dual weight, and the Schläfli row-sum condition on $W$. The dual weights come from incidence geometry; the weak-field data is the canonical second-order Regge Hessian built from those same incidence weights.
Incidence consistency of $K$ is the hypothesis that licenses both the dual-weight construction and the canonical weak-field data. Sibling lemmas already prove the off-diagonal match and the Schläfli row sum for that canonical data.
proof idea
Pure structure assembly, not a tactic proof. The weak-field field is filled by the canonical incidence weak-field data; the dual field by the independent dual weights of a consistent triangulation. The two propositional fields are discharged by the already-proved off-diagonal component match and the Schläfli row-sum lemma for that same canonical data. No new algebra is done here.
why it matters
This is the concrete witness that finalReggeComponentTarget applies: that theorem simply introduces an arbitrary incidence-consistent triangulation and returns this package, thereby discharging the arbitrary-triangulation component target for canonical incidence/Laplacian second-order Regge data.
In the Recognition gravity stack the component comparison is the bridge from discrete Regge geometry (hinge dual weights, Schläfli identities) to the continuum weak-field Hessian that feeds the continuum limit. The ambient setting is three spatial dimensions, matching the T8 forcing step $D=3$. The construction stays inside the genuine Regge Hessian rather than an ad-hoc continuum surrogate, so downstream continuum-limit and component theorems inherit a fully geometric discrete source.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.