doubleDecoration_firstEdgeLength
plain-language theorem explainer
The double metric decoration of the one-tetrahedron carrier has first-edge length exactly 2. Anyone citing the P2.5 mesh blocker or the two-decoration witness needs this evaluation. The proof is a one-line numerical unfolding of the squared-edge datum under square root.
Claim. If $D$ is the metric decoration of the one-tetrahedron complex that assigns squared edge length $4$ to every edge, then the first-edge length observable of $D$ equals $2$.
background
In the Seven Gaps P2.5 setting, PathSumMeasure.BoundedComplex and its quotient TriangulationClass record only cardinalities and incidence. Metric geometry is external. A MetricDecoration on a fixed simplicial carrier stores a positive squared-edge map; the double decoration is the constant map with value 4 (regular tetrahedron of edge length two on the same one-tet carrier).
The first-edge length is the genuine metric observable obtained by taking the positive square root of the squared length of edge 0. It is not a combinatorial invariant of the triangulation class. The module builds a concrete kernel certificate that two distinct positive decorations sit over one class and disagree on this observable (and on the Cayley-Menger volume observable).
proof idea
One-line wrapper: unfold the definitions of first-edge length and of the double decoration, then discharge the resulting numerical identity $\sqrt{4}=2$ by norm_num. No lemmas beyond definitional reduction are required.
why it matters
This evaluation is the second half of the numerical witness pair (unit decoration gives length 1; double decoration gives length 2). Downstream it is rewritten into unitDecoration_ne_doubleDecoration (the two decorations are unequal), into oneTetClass_has_two_metric_decorations (same carrier, complexity six, distinct edge and volume data), and into the P2.5 mesh blocker no_class_only_mesh_recovers_both: no function of the combinatorial class alone can return both edge lengths. That blocker is the concrete kernel certificate that the forgetful map from metric-decorated complexes to TriangulationClass 6 is non-injective, so a metric-refinement carrier (MetricRefinementFamily) is required before a geometric continuum limit can even be stated. The result is pure obstruction bookkeeping; construction of the family from the recognition substrate remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.