unitDecoration_firstEdgeLength
plain-language theorem explainer
On the one-tetrahedron carrier, the unit squared-edge decoration has first-edge length exactly 1. Gravity and discrete-geometry arguments cite this as the concrete evaluation of that metric observable. The proof is a one-line numerical unfolding of the definitions.
Claim. If $D$ is the unit squared-edge metric decoration of the one-tetrahedron complex (every squared edge equal to $1$), then the first-edge length $\sqrt{D(e_0)}$ equals $1$.
background
This module is the P2.5 metric-refinement carrier blocker in the Seven Gaps gravity stack. The combinatorial type TriangulationClass B only records cardinalities and incidence, so it forgets metric geometry. The file exhibits two positive nondegenerate metric decorations of the same one-tetrahedron witness that lie in one quotient class but disagree on edge lengths and on the Cayley-Menger volume observable.
A MetricDecoration stores squared edge lengths with a positivity certificate. The unit decoration sets every squared edge to $1$. The first-edge length is the genuine metric observable obtained by taking the positive square root of the stored squared length of edge $0$. That is the quantity evaluated here.
proof idea
One-line wrapper: unfold firstEdgeLength and unitDecoration, then close by norm_num. Under the unit decoration the squared first edge is $1$, so its square root is $1$.
why it matters
This evaluation is the unit half of the two-decoration witness that powers the P2.5 mesh blocker. Downstream, unitDecoration_ne_doubleDecoration uses it (with the parallel double-decoration evaluation) to separate the two decorations by first-edge length; oneTetClass_has_two_metric_decorations packages both lengths ($1$ and $2$) over a single simplicial carrier of complexity six; and no_class_only_mesh_recovers_both concludes that no function of the combinatorial class alone can recover both first-edge lengths.
In the module's honesty boundary this is a proved obstruction fact, not a continuum theorem. It forces any geometric path-sum carrier to carry metric decorations (as in the proposed MetricRefinementFamily) rather than only triangulation classes. Complexity-cutoff convergence remains distinct from metric mesh refinement; construction of the family from the recognition substrate stays open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.