ReggeComponentComparison
plain-language theorem explainer
Names the missing component-level match between the Regge second-variation matrix and geometric face weights: off diagonal, M_ij equals minus the hinge-dual area, with Schläfli row-sum closure on the diagonal. Anyone reducing the weak-field conformal Regge action to a geometric Dirichlet form cites this interface. It is a pure data package (no proof body); concrete meshes inhabit it by supplying areas and verifying the match.
Claim. For weak-field Regge linearization data $W$ on $n$ vertices, a component comparison consists of a symmetric nonnegative weight matrix $A_{ij}$ (intended geometric area of the face dual to edge $\langle i,j\rangle$) such that the bilinear coefficients satisfy $M_{ij}=-A_{ij}$ whenever $i\neq j$, and the Schläfli row-sum condition $\sum_j M_{ij}=0$ holds for every vertex $i$.
background
The module develops the algebraic core of the weak-field conformal reduction of the Regge action. With the conformal edge ansatz $\ell_{ij}=\ell_0\exp((\xi_i+\xi_j)/2)$, the second-order piece of $S=(1/\kappa)\sum_h A_h\delta_h$ becomes a bilinear form in the vertex potentials $\xi$. The structural lemma already proved in-file turns any symmetric zero-row-sum matrix $M$ into a Dirichlet form: $\sum_{i,j}M_{ij}\xi_i\xi_j=-\tfrac12\sum_{i,j}M_{ij}(\xi_i-\xi_j)^2$.
WeakFieldReggeData packages the first-order responses: hinge-area coefficients dArea and deficit coefficients dDeficit under conformal perturbations. Their entrywise product is the bilinear coefficient matrix $M_{ij}=\mathrm{dArea}{ij}\cdot\mathrm{dDeficit}{ij}$ that multiplies the quadratic terms in $S^{(2)}$. The Schläfli-derived row-sum property asserts $\sum_j M_{ij}=0$ on a flat background, which is exactly the zero-row-sum hypothesis the Laplacian identity needs.
What remains geometric (and outside pure algebra) is to identify those $M_{ij}$ with minus the actual face areas used by the continuum J-cost Dirichlet energy. That identification is the content packaged here.
proof idea
No proof: this is a structure definition, a theorem-shaped interface. An inhabitant must supply a geometric area matrix (symmetric and nonnegative), prove the off-diagonal identity $M_{ij}=-A_{ij}$ against bilinearCoefficient W, and attach a proof of SchlaefliRowSum W. Downstream constructors such as laplacianReggeData_componentComparison fill the fields by taking $A$ as the given weight matrix and discharging the match from the Laplacian-form coefficient package; genuine 3D packages copy their precomputed geometric areas and match lemmas into the same slots.
why it matters
This is the named target for Philip's $M_{ij}$ versus $\mathrm{area}(f_{ij})$ question in the gravity paper's Regge reduction. Once inhabited, componentComparison_gives_geometric_dirichlet converts the second-order Regge action into $\tfrac12$ times the Dirichlet form on the supplied geometric weights, which is the exact formal shape of the missing comparison.
Downstream, laplacianReggeData_componentComparison closes the interface for the graph-Laplacian coefficient package the current bridge uses; concreteReggeComponentComparison feeds a concrete Freudenthal star into that path; and componentComparison_of_genuine lifts any genuine 3D component package into the same type. The structure therefore sits between the fully proved algebraic §§1–2 of the module and the still-open Cayley–Menger/dihedral computation for arbitrary Regge meshes. It does not itself invoke T0–T8 or the RCL; it is the geometric hinge that lets the discrete Regge $S^{(2)}$ land on the continuum Dirichlet energy used elsewhere in the Recognition gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.