firstEdgeLength
plain-language theorem explainer
Extracts the Euclidean length of edge 0 from a positive squared-edge decoration of the one-tetrahedron complex. Gravity and discrete-geometry work cite it as the simplest mesh-sensitive observable that distinguishes unit and double decorations. The body is a one-line square root of the stored squared length at Fin-index 0.
Claim. For a metric decoration $D$ of the fixed one-tetrahedron complex (positive squared lengths on each of its six edges), the first-edge length is $\sqrt{D(e_0)}$, where $e_0$ is the edge indexed by $0\in\mathrm{Fin}\,6$.
background
Module P2.5 (metric-refinement carrier blocker) shows that the existing combinatorial quotient TriangulationClass only sees cardinalities and incidence, not metric geometry. A BoundedComplex carries edge count and incidence maps; a MetricDecoration on such a carrier is a map from edges to positive reals giving squared edge lengths, so the carrier stays combinatorial while the decoration supplies genuine metric data.
The witness complex is the nonempty one-tetrahedron simplicial complex with six edges. Two concrete decorations (unit and double) live on that same carrier and same quotient class but differ in edge lengths and in the Cayley-Menger volume observable. First-edge length is the elementary readout used to make that distinction quantitative: it takes the positive square root of the stored squared length on edge 0, so it is a true length rather than a squared datum.
Spatial dimension $D=3$ (forced in the T8/T9 chain) underlies the tetrahedral geometry, but this definition itself only needs the edge set of the one-tet complex.
proof idea
Pure definition, not a proved statement. Evaluate the decoration's squared-edge map at the canonical first edge (cast of $0:\mathrm{Fin},6$ into the complex's edge index type) and take the real square root. Positivity of squared edges in the decoration structure guarantees the root is well-defined and positive.
why it matters
This is the mesh-sensitive observable that drives the P2.5 obstruction. Downstream, unitDecoration_firstEdgeLength and doubleDecoration_firstEdgeLength evaluate it to $1$ and $2$; unitDecoration_ne_doubleDecoration uses the mismatch to prove the two decorations are unequal; oneTetClass_has_two_metric_decorations packages both decorations over one simplicial carrier of complexity six; and no_class_only_mesh_recovers_both is the mesh blocker: no function of the triangulation class alone can recover both first-edge lengths.
In the Seven Gaps gravity program this certifies that the forgetful map from metric-decorated complexes to the current combinatorial quotient is non-injective. The module then proposes MetricRefinementFamily as the missing carrier shape (finite decorated configs, mesh to zero, coarse projections, local action control). Open: building such a family from the recognition substrate and proving geometric continuum limits. Complexity-cutoff convergence remains distinct from metric mesh refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.