doubleMetricOneTet
plain-language theorem explainer
Packages the regular tetrahedron of edge length two as a metric-decorated complex on the single-tetrahedron carrier at cap 6. Cited as the second witness that two distinct positive metrics share one combinatorial class. Construction is a three-field structure instance: carrier, simpliciality proof, and constant squared-edge decoration 4.
Claim. Let $K$ be the single-tetrahedron bounded complex at cap $B=6$ (4 vertices, 6 edges, 1 tetrahedron). Define the metric-decorated complex whose carrier is $K$, whose simpliciality is that of $K$, and whose metric assigns squared edge length $4$ to every edge (regular tetrahedron of edge length $2$).
background
Module P2.5 isolates a carrier obstruction for gravity path sums. PathSumMeasure.BoundedComplex B stores only cardinalities and incidence; its quotient TriangulationClass B therefore classifies combinatorial types, not metric geometries. Mesh-sensitive observables (edge lengths, Cayley-Menger volume data) cannot be recovered from the class alone.
A MetricDecoratedComplex B is the minimal fix proposed here: a bounded complex, a proof it is simplicial, and a MetricDecoration (positive squared edge lengths on the 1-skeleton). The forgetful map toClass drops the metric and returns the combinatorial quotient class.
Upstream, oneTetComplex is the nonempty simplicial witness (4 vertices, complete 6-edge skeleton, one tetrahedron), proved simplicial by finite decide. doubleDecoration is the constant squared-edge map sqEdge ≡ 4 on that carrier, i.e. a regular tetrahedron of edge length two.
proof idea
Definitional structure instance, not a proof. The three fields of MetricDecoratedComplex 6 are filled by oneTetComplex (carrier), the existing theorem oneTetComplex_isSimplicial, and doubleDecoration (constant squared edge length 4). No tactics beyond whatever those components already use.
why it matters
This is the second of two concrete metric decorations on the same one-tetrahedron carrier. Together with the unit-edge decoration it feeds unitMetricOneTet_ne_doubleMetricOneTet (the two decorated complexes are unequal) and unit_double_toClass_eq (they share the same toClass). Those two facts are the kernel certificate that the forgetful map from metric-decorated geometries to TriangulationClass 6 is non-injective: edge lengths and Cayley-Menger observables differ while the combinatorial class does not.
In the Seven Gaps gravity program this is the P2.5 carrier blocker: no function of triangulation class alone can recover mesh-sensitive data. The module then proposes MetricRefinementFamily as the missing carrier shape. Open items remain construction from the recognition substrate, the measure and action, and the geometric continuum theorem. No full-theory flag moves; complexity-cutoff convergence stays distinct from metric mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.