finalReggeComponentTarget
plain-language theorem explainer
For every incidence-consistent 3D triangulation, a concrete Regge component comparison exists, built from canonical incidence weights and independent dual weights. Discrete-gravity workers matching weak-field Laplacian data to dual hinge structure would cite this. The proof is a one-line packaging of the already-constructed comparison into a nonempty existence claim.
Claim. For every three-dimensional triangulation $K$ that is incidence-consistent, there exists a concrete component comparison for $K$: canonical weak-field data and independent dual weights whose off-diagonal bilinear coefficients match the dual-weight components.
background
This module sits in the discrete-gravity layer: it separates the independent dual-weight construction on a 3D triangulation from the weak-field coefficient matrix, then records that the geometric computation yields a full component comparison package.
A triangulation $K$ is incidence-consistent when its edge/vertex incidence data support well-defined dual weights (edge-pair incidence weights and vertex-pair hinge weights, both symmetric, the latter nonnegative). From that data one builds canonical weak-field data whose bilinear coefficient matrix and row-sum structure are fixed by the incidence Laplacian, together with independent dual weights.
The target proposition asserts that every such $K$ admits a nonempty package of type concrete component comparison: weak-field data, dual weights, and an off-diagonal component-match identity. That package is the bridge from pure combinatorial geometry to the second-order Regge comparison used downstream in the gravity analysis.
proof idea
One-line wrapper. Introduce an arbitrary incidence-consistent triangulation $K$, then supply as witness the already-defined concrete comparison built from canonical incidence weights. That constructor assembles canonical weak-field data, independent dual weights from consistency, and the off-diagonal component-match lemma; wrapping it in a singleton proves nonemptiness of the comparison type.
why it matters
Discharges the arbitrary-triangulation component target for canonical incidence/Laplacian second-order Regge data, exactly the statement the module was written to record. In the Recognition framework this is the 3D discrete-gravity step that turns combinatorial dual weights into a genuine Regge component comparison, aligning with the forced spatial dimension $D=3$ (T8) and the eight-tick geometric setting.
No downstream consumers are wired yet in the graph; the declaration is the terminal existence theorem of this proof module. It closes the scaffolding path from incidence geometry to ReggeComponentComparison without adding new analytic hypotheses beyond incidence consistency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.