ConcreteComponentComparison
plain-language theorem explainer
Packages a weak-field Regge coefficient matrix on a 3D triangulation together with independently computed dual vertex-pair weights, requiring off-diagonal match (bilinear coeff equals minus dual weight) and the Schläfli row-sum identity. Gravity workers cite it as the concrete witness that geometric dual weights reproduce the genuine Regge Hessian components. It is a pure data structure, not a proved equality.
Claim. For a finite 3D Regge triangulation $K$, a concrete component comparison consists of weak-field Regge data $W$ on the vertices of $K$, an independent dual weight $w$ on vertex pairs (symmetric and nonnegative, not defined by negating the Hessian), the off-diagonal identity $B_W(i,j)=-w(i,j)$ for all $i\neq j$, and the Schläfli row-sum condition on $W$.
background
The module isolates the final comparison target for arbitrary 3D Regge triangulations: independent dual weights versus the weak-field coefficient matrix, then the theorem that turns the geometric computation into a component comparison.
A Triangulation3D is a finite abstract 3D Regge complex (vertex, edge, tetrahedron counts, incidence maps, nondegenerate squared-edge data on each tet). IndependentDualWeights attaches a symmetric nonnegative real weight to every vertex pair; the doc stresses these are geometric data, not defined by negating the Regge coefficient matrix. Weak-field Regge data supply the bilinear coefficient matrix of the second-order action; the Schläfli row-sum condition is the discrete identity that makes that matrix a pure Dirichlet form on edge areas.
Upstream, incidence-consistent triangulations yield canonical weak-field data and dual weights whose off-diagonal match is already proved as a sibling lemma, so this structure is the bundle those constructions inhabit.
proof idea
No proof body: this is a structure definition. It records four fields (weak-field data, independent dual weights, the off-diagonal component-match proposition, and the Schläfli row-sum proposition). Inhabitation is supplied downstream by concreteComponentComparisonOfIncidence, which fills the fields from canonical incidence weights, independent dual weights of a consistent triangulation, the off-diagonal match lemma, and the corresponding row-sum fact.
why it matters
This is the final arbitrary-triangulation component theorem target. FinalReggeComponentTarget is exactly the proposition that every incidence-consistent triangulation admits a nonempty instance of this structure. From any such instance, genuineComponentPackage_of_concrete builds the existing genuine component package (weak-field data plus geometric area equal to the dual weight), and genuine_component_dirichlet_reduction_from_final immediately recovers the second-order Regge action as one-half the Dirichlet form on edge areas.
In the Recognition gravity stack this closes the gap between pure geometric dual weights on a 3D Regge complex and the weak-field Hessian components needed for the continuum Dirichlet reduction, without defining the dual by fiat as minus the bilinear coefficient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.