concreteReggeComponentComparison
plain-language theorem explainer
Packages the weak-field Regge component comparison for a finite flat-sector star whose hinge weights are the regular triangular areas. Anyone connecting discrete second-order Regge action to the geometric Dirichlet form cites this object. It is a one-line specialization of the Laplacian comparison lemma to the concrete symmetric nonnegative area-weight matrix.
Claim. Given a concrete local Regge star $S$ (positive background edge length and nonnegative hinge area), the weak-field Regge data built from $S$ carries a component comparison: its coefficient matrix is the graph Laplacian of the geometric area weights $A_{ij}$ (off-diagonal $M_{ij}=-A_{ij}$, every row sums to zero).
background
The module supplies a first fully concrete finite model for the weak-field Regge bridge: a local star with fixed background edge length and hinge area, rather than a general Cayley-Menger triangulation. The Cayley-Menger stack already knows regular tetrahedron data and dihedral angles, but not yet full edge-length derivatives for arbitrary hinges, so the comparison is closed only for this regular flat-sector package.
A concrete star records positive edgeLength0 and nonnegative hingeArea0. The area-weight matrix is zero on the diagonal and equal to the background hinge area off-diagonal; it is symmetric and entrywise nonnegative. Weak-field Regge data from that star is the graph-Laplacian package already consumed by the bridge: off-diagonal coefficients equal minus the area weights, rows sum to zero.
Upstream, the general Laplacian comparison lemma turns any such symmetric nonnegative weight matrix into a ReggeComponentComparison witness. This definition simply feeds the concrete weights into that interface.
proof idea
One-line wrapper. Apply the general lemma that builds a component comparison from Laplacian Regge data, passing the concrete area-weight matrix together with its symmetry and nonnegativity proofs. No new geometric identities are proved here.
why it matters
This is the exact interface object the weak-field bridge consumes without new geometric axioms. Downstream, concreteReggeSecondVariation_eq_jcostDirichlet unfolds it to conclude that the second-order Regge action on an 8-tick log potential equals half the Dirichlet form of the concrete area weights: the geometric content of the component comparison in the regular flat sector.
In the Recognition geometry stack this is the first closed finite model linking Freudenthal-local Regge data to the J-cost / Dirichlet side of the weak-field conformal bridge. It does not finish the full Cayley-Menger derivative program; it fixes the target any future general dihedral-derivative computation must hit. Landmarks touched are the discrete geometric side of the weak-field gravity bridge (eight-tick register as the potential domain), not the T5–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.