alone
plain-language theorem explainer
On the one-tetrahedron combinatorial type, two admissible metric decorations share the same triangulation class yet disagree on first-edge length. Therefore no map out of the bare triangulation-class carrier can recover that length for both decorations. Gravity and path-sum authors cite this as the concrete P2.5 kernel certificate that metric data is not a function of incidence alone. The content is a definitional carrier interface plus witness packaging, not a deep derivation.
Claim. There exist two admissible metric decorations of the same one-tetrahedron complex, lying in one triangulation class at a fixed cap, whose first-edge lengths differ. Hence no function of the triangulation class alone can return the first-edge length of both decorations.
background
The Seven Gaps P2.5 module isolates a carrier mismatch in discrete gravity. A BoundedComplex records only vertex/edge/triangle counts and incidence; its quotient TriangulationClass therefore classifies combinatorial type, not metric geometry. Metric data must be supplied by a separate decoration.
A metric decoration assigns positive edge lengths subject to nondegeneracy (tetrahedron inequalities / positive Cayley–Menger content). Two standard decorations on the nonempty witness complex are the unit decoration and the double decoration: they scale the first edge differently, so both the first-edge length observable and the Cayley–Menger volume observable split.
Upstream scaffolding supplies the bare edge complex and admissibility predicates used to state positivity. The local honesty boundary is explicit: obstruction and witness facts are theorems; the decorated-complex and refinement-family interfaces are proposed API; constructing a refinement family from the recognition substrate and proving continuum convergence remain open.
proof idea
No tactic proof is attached: the declaration is definitional carrier packaging around already-proved sibling witnesses. Those siblings exhibit two decorations on the one-tet complex, compute their first-edge lengths, prove the lengths differ, and show both decorations land in the same triangulation class. The present item records the resulting reading: any functional depending only on the class is constant on that pair, so it cannot equal both edge lengths. Related siblings run the same argument for the Cayley–Menger observable and package non-injectivity of the forgetful map from metric-decorated complexes to the quotient.
why it matters
In the Recognition gravity stack this is the concrete kernel certificate for gap P2.5: path-sum carriers built only from TriangulationClass cannot see mesh geometry. It motivates the proposed MetricRefinementFamily interface later in the same module (finite decorated configuration spaces, mesh tending to zero, coarse projections, summable local action-step control) without assuming path-sum convergence.
Downstream, a corrected metric carrier is a prerequisite for geometric continuum limits that feed constants and cosmology layers (alpha-band calibration, FRW entropy bookkeeping, ledger-level Sakharov asymmetry). The module stresses that complexity-cutoff convergence is a different question from metric mesh refinement; this blocker closes only the “class alone recovers length” route. Open: build the family from the recognition substrate, derive its measure and action, and prove the geometric continuum theorem. No full-theory flag moves here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.