IndisputableMonolith.Gravity.SevenGaps.MetricRefinementCarrierBlocker
Defines positive squared-edge metric decorations on a fixed combinatorial carrier (BoundedComplex), without changing the carrier. Unit and double decorations yield unequal first-edge lengths and Cayley-Menger observables on one tetrahedron class. Gravity and discrete-QG workers cite it as a carrier-vs-metric separation lemma in the Seven Gaps campaign. The argument is by explicit decoration constructors and direct evaluation of the two observables.
claimA metric decoration is positive squared-edge data on a fixed combinatorial carrier $B$ (a $\mathrm{BoundedComplex}$). The unit and double decorations $u$ and $d$ satisfy $\ell_1(u)\neq\ell_1(d)$ and $CM(u)\neq CM(d)$ for the first-edge length and Cayley-Menger observables, so a single tetrahedron class admits at least two inequivalent metric refinements.
background
The QG Seven Gaps campaign separates combinatorial carriers from continuum and Lorentzian structure. Upstream modules supply causal (CDT-style) tetrahedron and 4-simplex classes with spacelike/timelike edge typing and a kinematical Wick rotation in 3D and 4D. Those objects fix incidence and causal type; they do not yet pin numerical edge lengths.
This module adds metric refinement as an extra layer: positive squared lengths on the edges of an existing BoundedComplex. The carrier stays exactly that complex; only the decoration changes. Two canonical decorations (unit and double) and two observables (first-edge length, Cayley-Menger) make the separation concrete.
A parallel blocker track (phased quotient continuum cutoff) isolates analytic obligations for path-sum limits. Here the obligation is geometric: metric data must not be smuggled into the combinatorial type.
proof idea
Definition module with short evaluation lemmas, not a deep derivation. It introduces MetricDecoration and MetricDecoratedComplex, then the constructors unitDecoration and doubleDecoration on the fixed carrier. firstEdgeLength and cayleyMengerObservable are read off the decoration. Four one-line evaluations compute those observables on unit and double data; inequality lemmas compare the results; the headline fact packages that one tetrahedron class carries two distinct metric decorations.
why it matters in Recognition Science
Feeds the Full Theory Ledger (Phase 0c), the machine-checked benchmark board for the full quantum-gravity campaign: ledger flags flip only when pillar targets are kernel-checked and critic-passed. The module blocks conflating combinatorial carrier identity with metric geometry, a prerequisite for honest continuum and Lorentzian lifts in the Seven Gaps stack.
It sits beside CausalSimplexWick / CausalSimplex4D (causal simplex classes and kinematical Wick rotation) and the Zq continuum blocker. Those fix causal typing and path-sum cutoffs; this one fixes that squared-edge data can refine a carrier without changing it. Downstream ledger aggregation treats that separation as a named pillar input rather than an informal remark.
scope and limits
- Does not construct a continuum limit or prove metric convergence of complexes.
- Does not assign physical units or couple decorations to Einstein dynamics.
- Does not classify all decorations; only unit vs double on one tet class.
- Does not alter BoundedComplex incidence or causal edge typing.
- Does not discharge phased-quotient or Wick-rotation ledger flags by itself.
used by (1)
depends on (3)
declarations in this module (25)
-
structure
MetricDecoration -
structure
MetricDecoratedComplex -
def
unitDecoration -
def
doubleDecoration -
def
firstEdgeLength -
def
cayleyMengerObservable -
theorem
unitDecoration_firstEdgeLength -
theorem
doubleDecoration_firstEdgeLength -
theorem
unitDecoration_cayleyMenger -
theorem
doubleDecoration_cayleyMenger -
theorem
unitDecoration_ne_doubleDecoration -
theorem
oneTetClass_has_two_metric_decorations -
def
oneTetClass -
class
alone -
theorem
no_class_only_mesh_recovers_both -
theorem
no_class_only_cayleyMenger_recovers_both -
def
unitMetricOneTet -
def
doubleMetricOneTet -
theorem
unitMetricOneTet_ne_doubleMetricOneTet -
theorem
unit_double_toClass_eq -
theorem
metricForget_not_injective -
theorem
causalPent_metric_observable_varies -
structure
MetricRefinementFamily -
def
metricZ -
def
HasGeometricZRSContinuumLimit