MetricRefinementFamily
plain-language theorem explainer
A structure packing the minimal geometric-refinement carrier for path sums: finite metric-decorated configuration spaces at each level, a mesh tending to zero, coarse projections between levels, and a summable bound on adjacent-level action increments. Gravity and continuum-limit work cite it when replacing bare complexity cutoffs by genuine mesh refinement. It is pure interface data, not a proved construction.
Claim. A metric-refinement family consists of: finite configuration types $\mathrm{Config}(n)$ for each level $n$; a strictly monotone combinatorial capacity $\mathrm{cap}(n)$; a map sending each configuration to a metric-decorated simplicial complex of capacity $\mathrm{cap}(n)$; coarsening maps $\mathrm{Config}(n+1)\to\mathrm{Config}(n)$; a positive mesh $h_n\to 0$ that upper-bounds every edge length and is attained; a real action on configurations; and a nonnegative summable sequence $\varepsilon_n$ controlling $|S_{n+1}(c)-S_n(\mathrm{coarsen}\,c)|\le\varepsilon_n$.
background
Module P2.5 isolates a carrier obstruction in the Seven Gaps gravity stack. The existing path-sum substrate BoundedComplex B records only cardinalities and incidence; its quotient TriangulationClass B therefore equates combinatorial types, not metric geometries. The module exhibits a concrete witness: one tetrahedron class admits two positive nondegenerate metric decorations with distinct edge lengths and distinct Cayley-Menger values, so no function of the bare quotient recovers mesh-sensitive observables.
A metric-decorated complex is the smallest object that pairs a bounded simplicial carrier with edge-square metric data, so mesh and Cayley-Menger can be evaluated. The present structure upgrades that static decoration to a refinement sequence: levels, coarsening, mesh to zero, and local action-step control. The module header stresses that complexity-cutoff convergence is not the same as metric mesh refinement, and that construction of such a family from the recognition substrate remains open.
proof idea
No proof body: this is a structure definition (API/model). Fields are declared as data and Prop constraints only. Finite configuration spaces, strict monotonicity of capacity, positivity and attainment of the mesh, mesh tending to zero in the filter topology, nonnegativity and summability of the step-error sequence, and the pointwise action-increment bound are all part of the interface contract rather than derived lemmas. Downstream code supplies instances or treats the structure as a hypothesis package.
why it matters
This is the missing carrier shape named in the P2.5 honesty boundary: enough geometry to define finite-level path sums and state a continuum-limit proposition, without assuming that limit. Downstream, metricZ builds the level-$n$ path sum $\sum_c \mu_n(c),e^{i S_n(c)}$ once an external measure is supplied (P2.2 obligation kept separate). HasGeometricZRSContinuumLimit is the open target proposition that those partial sums tend to some $L\in\mathbb{C}$.
In the Recognition gravity program this separates combinatorial census cutoffs from genuine geometric refinement toward a continuum $Z_{\mathrm{RS}}$. It does not close the open construction from the recognition substrate, nor the derivation of measure and action; it only makes those obligations well-typed. No full-theory flag moves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.