unitDecoration_ne_doubleDecoration
plain-language theorem explainer
The unit-edge and double-edge metric decorations on the one-tetrahedron carrier are unequal as functions. Anyone citing the P2.5 kernel certificate (two metrics over one triangulation class) needs this separation. The proof is a short congruence on first-edge length followed by numerical contradiction (1 ≠ 2).
Claim. The unit-edge metric decoration on the one-tetrahedron complex is not equal to the double-edge decoration (squared edge lengths constantly $4$). In particular they are distinct elements of the space of positive squared-edge assignments on that carrier.
background
Module P2.5 isolates a carrier obstruction for gravity path sums. BoundedComplex B and its quotient TriangulationClass B record only cardinalities and incidence, so they identify combinatorial types, not metric geometries. The forgetful map from metric-decorated complexes to that quotient is therefore a candidate kernel source.
A MetricDecoration on a fixed carrier assigns a positive squared length to each edge. Two concrete decorations live on oneTetComplex: the unit decoration (squared edges $1$) and the double decoration (squared edges $4$, regular tetrahedron of edge length two). The observable firstEdgeLength reads the positive square root of the first edge's squared length, so it is a genuine metric quantity, not a combinatorial one.
Complexity of a bounded complex is the max of vertex, edge, and tetrahedron counts (the shell coordinate). The one-tet witness has complexity six and is simplicial; the module uses it as the concrete kernel certificate that class data alone cannot recover edge or Cayley-Menger observables.
proof idea
Term-style proof by contradiction. Assume the two decorations are equal as functions. Apply congruence of firstEdgeLength to that equality. Rewrite with the evaluation lemmas unitDecoration_firstEdgeLength (value $1$) and doubleDecoration_firstEdgeLength (value $2$). Close by norm_num, which discharges $1 = 2$. No further structure on the carrier is needed beyond those two evaluation facts.
why it matters
This is the atomic inequality behind the P2.5 obstruction. Downstream, oneTetClass_has_two_metric_decorations packages it with simpliciality and complexity six to exhibit two decorations over one genuine carrier with different edge and volume data. unitMetricOneTet_ne_doubleMetricOneTet lifts the same separation to fully packaged metric-decorated complexes at cap $6$.
In the Seven Gaps program this shows that no function of TriangulationClass 6 alone can recover first-edge length (or the Cayley-Menger observable) for both decorations: the forgetful map is explicitly non-injective. The module's honesty boundary keeps the obstruction as THEOREM while MetricRefinementFamily remains MODEL/API; construction from the recognition substrate and the geometric continuum limit stay OPEN. Complexity-cutoff convergence is deliberately separated from metric mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.