unitDecoration_cayleyMenger
plain-language theorem explainer
On the unit squared-edge decoration of the one-tetrahedron carrier, the Cayley-Menger observable equals 4. Discrete-gravity and RS gap-audit workers cite this when separating combinatorial triangulation classes from metric data. The proof is a one-line numerical evaluation of the Cayley-Menger polynomial after unfolding the unit decoration and the observable definition.
Claim. For the metric decoration of the one-tetrahedron complex in which every squared edge length equals $1$, the Cayley-Menger observable (the Cayley-Menger polynomial in the six squared edge lengths) equals $4$.
background
Module P2.5 treats the metric-refinement carrier blocker. The bounded-complex carrier records only cardinalities and incidence; its triangulation-class quotient therefore identifies combinatorial types, not metric geometries. The obstruction is witnessed on the existing one-tetrahedron simplicial complex by two positive nondegenerate metric decorations in the same class whose edge and volume data differ.
A metric decoration assigns a positive squared length to each edge of that complex. The unit decoration sets every squared edge to $1$. The Cayley-Menger observable of a decoration is the explicit degree-three Cayley-Menger polynomial cm3 in the six squared edge lengths; on realizable tetrahedra it equals $288$ times squared volume and feeds the Regge metric API.
This lemma records the concrete numerical value of that observable on the unit decoration, so later comparison with the double decoration (edge length two) is a pure equality of reals.
proof idea
One-line wrapper: unfold the observable (as cm3 of the decoration's squared-edge map), unfold the unit decoration (constant map to $1$), and discharge the resulting rational arithmetic by norm_num against the expanded Cayley-Menger polynomial.
why it matters
Supplies the unit side of the numerical mismatch used by the parent obstruction theorems. oneTetClass_has_two_metric_decorations packages both decorations over one genuine complexity-six carrier with distinct edge and volume data. no_class_only_cayleyMenger_recovers_both then rewrites both sides and shows no real-valued function of the triangulation class alone can equal both Cayley-Menger values, so the forgetful map from metric-decorated complexes to the current quotient is non-injective for an action-relevant observable, not only for a chosen edge coordinate.
In the Seven Gaps ledger this is a proved kernel certificate for P2.5: combinatorial class data cannot carry metric refinement. The module's honesty boundary keeps construction of a full MetricRefinementFamily from the recognition substrate, and the geometric continuum theorem, open; complexity-cutoff convergence remains distinct from metric mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.