componentComparison_of_genuine
plain-language theorem explainer
A genuine geometric component package on a 3D Regge triangulation is coerced into the existing Regge component-comparison interface by copying its area form and matching axioms. Anyone connecting the Cayley–Menger/Hessian computation to the weak-field conformal bridge cites this. The body is a pure structure projection: each comparison field is taken from the package.
Claim. Given a finite 3D Regge triangulation $K$ and a genuine component package $G$ on $K$ (weak-field data $W$, a symmetric nonnegative geometric area form, off-diagonal bilinear match to $-$area, and a Schläfli row-sum condition), there is an induced Regge component comparison on $W$ whose geometric area is exactly that of $G$.
background
This module bridges the genuine 3D Regge Hessian package to the already-proved weak-field conformal Regge reduction. A Triangulation3D is a finite abstract 3D Regge complex: vertex/edge/tet counts, edge endpoints, and tet vertex maps, with nondegenerate squared-edge data on each tetrahedron.
A genuine component package packages the output of the Cayley–Menger / dihedral / Hessian computation: weak-field Regge data $W$ on the vertices, a geometric area kernel on vertex pairs, symmetry and nonnegativity of that kernel, the off-diagonal identity that the bilinear coefficients of $W$ equal minus the geometric areas, and a Schläfli row-sum condition on $W$.
The target interface is the existing Regge component comparison used by the weak-field conformal bridge. Once that interface is inhabited, the Dirichlet-form reduction already proved in the weak-field module applies without redoing the geometric work.
proof idea
Definitional structure coercion, not a tactic proof. The comparison record is filled fieldwise from the genuine package: geometric area, its symmetry and nonnegativity, the off-diagonal bilinear match, and the Schläfli row-sum witness are copied verbatim. No new geometric identity is established here.
why it matters
In the Recognition gravity stack this is the adapter that lets the genuine 3D Hessian computation speak the language of the weak-field conformal Regge bridge. The module doc states the intent: the geometric side supplies a genuine component package; this definition turns it into ReggeComponentComparison and therefore into the Dirichlet-form reduction already available downstream.
The sibling reduction that applies the weak-field theorem to a genuine package depends on this coercion. Within the broader RS picture it sits on the gravity side of the discrete geometry program (Regge calculus in $D=3$), not on the T0–T8 forcing chain itself, but it is how continuum-style weak-field identities inherit from the discrete geometric computation rather than from an ad hoc ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.