MetricDecoratedComplex
plain-language theorem explainer
A metric-decorated simplicial complex packages a bounded combinatorial carrier, a simpliciality witness, and positive squared-edge lengths. Gravity and continuum-limit work cite it as the minimal object on which mesh-sensitive observables (edge lengths, Cayley–Menger) can be evaluated. It is a plain structure definition, not a proved statement.
Claim. For a natural number bound $B$, a metric-decorated complex consists of a bounded complex $K$ of capacity at most $B$, a proof that $K$ is simplicial, and a metric decoration: a map from edges of $K$ to strictly positive real squared lengths. Forgetting the metric yields the combinatorial triangulation class of $K$ in the relabeling quotient.
background
The Seven Gaps P2.5 module isolates a carrier obstruction for geometric continuum limits. PathSumMeasure.BoundedComplex B records only cardinalities and incidence; its quotient TriangulationClass B therefore identifies combinatorial types, not metric geometries. Mesh-sensitive quantities cannot live on that quotient alone.
A MetricDecoration on a fixed carrier $K$ is positive squared-edge data sqEdge : Fin K.nE → ℝ with 0 < sqEdge e for every edge. The present structure pairs that decoration with the carrier and a simpliciality proof, giving the smallest configuration on which edge-length and Cayley–Menger observables make sense.
The module already has a nonempty simplicial witness (one tetrahedron at cap 6). Two different positive decorations on that same carrier land in one quotient class but disagree on observables, which is the concrete kernel of the forgetful map.
proof idea
No proof: this is a structure declaration. Fields are carrier : BoundedComplex B, simplicial : IsSimplicial carrier, and metric : MetricDecoration carrier. The companion forgetful map sends a decorated complex to the relabeling quotient class of its carrier via Quotient.mk (relabelSetoid B) G.carrier. Downstream constructions fill the three fields (e.g. unit and double edge-length decorations on oneTetComplex).
why it matters
This is the MODEL/API carrier for the P2.5 metric-refinement blocker. Downstream, unitMetricOneTet and doubleMetricOneTet inhabit it; their inequality yields metricForget_not_injective, which the full-theory ledger records as gap2_metric_carrier_blocker_certified: the forgetful map from metric-decorated complexes at $B=6$ to TriangulationClass 6 is not injective.
MetricRefinementFamily then uses MetricDecoratedComplex (cap n) as the type of finite-level configurations, so mesh-to-zero sequences and local action-step control can be stated without pretending the bare combinatorial quotient remembers geometry.
In the Recognition gravity stack this separates complexity-cutoff path sums from genuine metric mesh refinement. Open items remain: building such a family from the recognition substrate, deriving measure and action, and proving the geometric continuum theorem. No full-theory flag is flipped by introducing the type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.