genuineComponentPackage_of_concrete
plain-language theorem explainer
A finished concrete component comparison (weak-field data, independent dual weights, off-diagonal Hessian match, Schläfli row sum) assembles into a genuine geometric component package on a 3D Regge triangulation. Gravity workers cite it to lift a Cayley-Menger/Hessian computation into the package interface that Dirichlet reduction consumes. The body is a pure field reassembly: dual weights become geometric areas and the comparison identities are reused verbatim.
Claim. Let $K$ be a finite 3D Regge triangulation. Given a concrete component comparison $C$ on $K$ (weak-field Regge data $W$, independent dual weights $w$, the identity that off-diagonal bilinear coefficients of $W$ equal $-w$, and the Schläfli row-sum identity for $W$), there exists a genuine component package for $K$ whose weak-field data is $W$, whose geometric area is $w$ (symmetric and nonnegative), and whose off-diagonal match and Schläfli row-sum are those of $C$.
background
The module isolates the last step of the 3D Regge component program: once independent dual weights and the weak-field coefficient matrix are in hand, package them for the existing comparison interface. A Triangulation3D is a finite abstract 3D Regge complex (vertex/edge/tet counts, incidence, nondegenerate squared-edge data on each tetrahedron).
A concrete component comparison bundles weak-field Regge data $W$, an independent dual-weight pair on $K$, the off-diagonal identity bilinearCoefficient$(W,i,j)=-w(i,j)$ for $i\neq j$, and a Schläfli row-sum condition on $W$. The genuine component package is the geometric interface produced by the Cayley-Menger/dihedral/Hessian computation: the same $W$, a geometric area function with symmetry and nonnegativity, the off-diagonal match to that area, and the Schläfli row sum.
This definition is the forgetful map from the concrete comparison record onto that package type.
proof idea
Structure construction by field projection, not a tactic proof. Set the package weak-field data to $C.W$. Set geometric area to the dual weight of $C$, and import symmetry and nonnegativity from that dual-weight record. Copy the off-diagonal component match and the Schläfli row-sum hypothesis straight from $C$. No lemmas are applied; the types line up by construction of ConcreteComponentComparison and GenuineComponentPackage.
why it matters
This is the adapter that turns a finished concrete Hessian comparison into the package type the rest of the 3D Regge stack expects. Downstream, genuine_component_package_of_final uses it to discharge nonemptiness of the genuine package from the final arbitrary-triangulation target (under incidence consistency). Immediately after, genuine_component_dirichlet_reduction_from_final applies the existing Dirichlet reduction: once the package is built, the second-order Regge action equals half the Dirichlet form of the edge-area weights.
In the Recognition gravity line this sits under the $D=3$ spatial forcing (T8) and the discrete Regge route to the weak-field Laplacian. It does not invent new physics; it closes the bookkeeping gap between the concrete dual-weight computation and the package-shaped theorems already proved for genuine components.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.