genuine_component_package_of_final
plain-language theorem explainer
Given that every incidence-consistent 3D Regge triangulation admits a concrete component comparison, every such triangulation also admits a genuine geometric component package (weak-field data, geometric areas, off-diagonal match). Discrete-gravity workers matching the weak-field Hessian would cite this bridge. The proof unpacks the target hypothesis and converts via the existing concrete-to-genuine lemma.
Claim. If every incidence-consistent 3D Regge triangulation $K$ admits a nonempty concrete component comparison, then for every such $K$ the genuine geometric component package is nonempty.
background
A 3D Regge triangulation is finite abstract incidence data (vertices, edges, tetrahedra) with a nondegenerate squared-edge tuple on every tetrahedron. Incidence consistency adds global squared edges, local-to-global edge-endpoint agreement up to orientation, and a local closed-form Schläfli identity so global curvature identities need no caller-supplied Schläfli data.
The module separates independent dual-weight construction from the weak-field coefficient matrix, then records how that geometric computation becomes a Regge component comparison. The genuine component package is the Cayley-Menger/dihedral/Hessian output: weak-field Regge data, a symmetric nonnegative geometric-area matrix on vertex pairs, and an off-diagonal component match.
The final component target is the proposition that every consistent triangulation yields a nonempty concrete component comparison. This theorem turns that target into existence of the genuine package.
proof idea
Introduce an arbitrary triangulation $K$ and an incidence-consistency witness. Apply the final-target hypothesis at $(K,hK)$ and destructure the resulting nonempty concrete comparison to a witness $C$. Feed $C$ to the conversion lemma that builds a genuine component package from concrete data, and re-wrap as Nonempty. Pure unpack-and-convert; no new geometry.
why it matters
Discharge step from a completed concrete construction to the interface type expected by the 3D Regge component theorem. The module frames this as the bridge that turns dual-weight geometry into ReggeComponentComparison; the following doc-comment notes that once the final package exists, the existing Dirichlet reduction applies immediately.
In the RS gravity stack this sits on the discrete curvature side of the $D=3$ scaffold (forcing step T8) and the eight-tick octave (T7), where weak-field hinge data must match geometric areas from Cayley-Menger. No used_by edges are wired yet, so the lemma is presently a terminal bridge awaiting the Dirichlet call site rather than an already-consumed parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.