unit_double_toClass_eq
plain-language theorem explainer
The unit-edge and double-edge metric decorations of the one-tetrahedron complex determine the same triangulation class. Gravity and path-sum authors cite this as the kernel witness that combinatorial quotienting erases metric data. The proof is pure definitional equality: both decorations share the identical simplicial carrier, so their forgetful images coincide by reflexivity.
Claim. Let $U$ be the one-tetrahedron complex equipped with the unit edge-length decoration, and let $D$ be the same complex equipped with the edge-length-two decoration. Then the triangulation class of $U$ equals the triangulation class of $D$.
background
In the Seven Gaps P2.5 setting, a bounded complex records only cardinalities and incidence maps. Its quotient, the triangulation class at a fixed bound, therefore classifies combinatorial types rather than metric geometries. Metric decorations attach positive edge lengths to such a carrier; packaging carrier plus decoration yields a metric-decorated complex.
Two concrete decorations live on the nonempty one-tetrahedron witness: the unit decoration (all edges length one) and the double decoration (all edges length two). Both are positive and nondegenerate. The forgetful map sends a metric-decorated complex to the triangulation class of its underlying carrier. Because the two decorations share that carrier, they are candidates for a nontrivial kernel of the forgetful map.
The module's honesty boundary marks obstruction theorems as proved and the proposed metric-refinement family as model/API only; continuum construction from the recognition substrate remains open.
proof idea
One-line term proof by rfl. By definition both decorated complexes use the same simplicial carrier (oneTetComplex) and the same simpliciality certificate; only the metric field differs. The forgetful projection to triangulation class depends solely on that carrier, so the two images are definitionally equal.
why it matters
This equality is the positive half of the P2.5 carrier blocker. Downstream, metricForget_not_injective combines it with the inequality of the two decorated complexes to show the forgetful map from metric-decorated complexes to triangulation classes is not injective. The module doc states the consequence: no function of triangulation class alone can recover edge length or the Cayley-Menger observable for both decorations.
In the Recognition gravity stack this certifies that the existing path-sum carrier is too coarse for metric mesh refinement. The file then proposes MetricRefinementFamily as the missing carrier shape (finite decorated configuration spaces, mesh to zero, coarse projections, summable local action control), without claiming continuum convergence. Complexity-cutoff convergence remains a separate question from metric refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.