oneTetClass
plain-language theorem explainer
Names the combinatorial triangulation class of a single tetrahedron at bound six: the image of the one-tet complex under the relabeling quotient. Gravity and discrete-path-sum work cite it as the shared class of two inequivalent metric decorations. The body is a one-line quotient constructor application.
Claim. Write $[T_1]$ for the class of the single-tetrahedron complex in the quotient of bounded simplicial complexes of combinatorial capacity $6$ by combinatorial relabeling. Thus $[T_1]$ is an element of the triangulation-class space at bound $6$.
background
In the Seven Gaps P2.5 setting, a bounded complex records only cardinalities and incidence maps. Its quotient by relabeling therefore classifies combinatorial types, not metric geometries. The module builds a concrete kernel certificate of that obstruction.
The existing nonempty simplicial witness is the one-tetrahedron complex at capacity six. Metric decorations assign positive edge lengths to that complex; two standard decorations (unit and double) live on the same combinatorial type but disagree on edge lengths and on the Cayley–Menger volume observable.
This definition simply packages that witness as a point of the triangulation-class space, so later statements can quantify over functions of the class alone.
proof idea
Definitional one-liner: form the equivalence class of the one-tetrahedron complex under the relabeling setoid at bound six via the standard quotient constructor. No lemmas are applied beyond the quotient API.
why it matters
Supplies the common class argument for the two P2.5 mesh-blocker theorems: no function of the combinatorial class alone recovers first-edge length for both unit and double decorations, and likewise no such function recovers both Cayley–Menger values. Those results certify that the forgetful map from metric-decorated complexes to the current quotient is non-injective.
In the Recognition gravity stack this is the combinatorial half of the metric-refinement carrier gap: path-sum measures on bare triangulation classes cannot see mesh scale. The module’s honesty boundary keeps construction of a genuine MetricRefinementFamily (finite decorated configs, mesh to zero, summable local action) open; this class is only the obstruction witness, not that carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.