Gravity Seven Gaps Metric Refinement Carrier Blocker One Tet Class Has Two Metri

The metric obstruction

A metric decoration is a choice of positive edge lengths on a geometric object, the kind of assignment that lets you measure distances and angles. The declaration oneTetClass_has_two_metric_decorations shows that one specific tetrahedron, a shape with six edges, admits two such assignments that are genuinely different but that the framework's current ledger, its discrete record of combinatorial types, cannot tell apart. In the first assignment every edge has length 1; in the second every edge has length 2. Both are valid, non-degenerate metrics on the same underlying tetrahedron.

The result proves that these two assignments are distinct as metric objects: the first edge differs (length 1 versus length 2), and a standard geometric observable called the Cayley-Menger invariant, which encodes volume information from edge lengths, differs as well (4 versus 256). Yet when the framework forgets the metric and keeps only the combinatorial type, the two collapse to the same entry in the ledger. The formal statement records the full witness: the tetrahedron is simplicial, has complexity 6, and there exist two decorations with the stated differing edge lengths and observables.

The consequence is a proved obstruction. No function defined only on the combinatorial class can recover both edge lengths or both Cayley-Menger values, because the class does not carry the metric information. The forgetful map from metric-decorated complexes to the quotient class is explicitly non-injective. This is not a failure of the framework but a precise certificate that the current carrier, the object type that carries the geometry, is too coarse for metric questions. The framework's own library proves this in a machine-checked way.

In Recognition Science, this result motivates a proposed remedy: a structure called MetricRefinementFamily, a carrier shape with finite metric-decorated configuration spaces, a mesh tending to zero, and coarse projections. It does not assume convergence of the path sum; it is just enough to define a geometric finite-level path sum and state a continuum-limit proposition. The construction of such a family from the recognition substrate, the derivation of its measure and action, and the geometric continuum result all remain open targets, not achievements.

/-- Both decorations live over one genuine simplicial carrier of exact
combinatorial complexity six, but have different edge and volume data. -/
theorem oneTetClass_has_two_metric_decorations :
    IsSimplicial oneTetComplex ∧
      complexity oneTetComplex = 6 ∧
      ∃ D₁ D₂ : MetricDecoration oneTetComplex,
        D₁ ≠ D₂ ∧
        firstEdgeLength D₁ = 1 ∧ firstEdgeLength D₂ = 2 ∧
        cayleyMengerObservable D₁ = 4 ∧
          cayleyMengerObservable D₂ = 256 := by
  refine ⟨oneTetComplex_isSimplicial, rfl,
    unitDecoration, doubleDecoration, unitDecoration_ne_doubleDecoration,
    unitDecoration_firstEdgeLength, doubleDecoration_firstEdgeLength,
    unitDecoration_cayleyMenger, doubleDecoration_cayleyMenger⟩

theorem unitDecoration_firstEdgeLength :
    firstEdgeLength unitDecoration = 1 := by
  norm_num [firstEdgeLength, unitDecoration]

theorem doubleDecoration_firstEdgeLength :
    firstEdgeLength doubleDecoration = 2 := by
  norm_num [firstEdgeLength, doubleDecoration]

theorem unitDecoration_cayleyMenger :
    cayleyMengerObservable unitDecoration = 4 := by
  norm_num [cayleyMengerObservable, unitDecoration, cm3]

theorem doubleDecoration_cayleyMenger :
    cayleyMengerObservable doubleDecoration = 256 := by
  norm_num [cayleyMengerObservable, doubleDecoration, cm3]

/-- **P2.5 MESH BLOCKER.** No function of the current combinatorial quotient
class alone can recover the first-edge length of both admissible metric
decorations. -/
theorem no_class_only_mesh_recovers_both
    (mesh : TriangulationClass 6 → ℝ) :
    ¬ (mesh oneTetClass = firstEdgeLength unitDecoration ∧
      mesh oneTetClass = firstEdgeLength doubleDecoration) := by
  rw [unitDecoration_firstEdgeLength, doubleDecoration_firstEdgeLength]
  rintro ⟨h₁, h₂⟩
  linarith

/-- The same obstruction holds for an action-relevant Cayley-Menger
observable, not only for a chosen edge coordinate. -/
theorem no_class_only_cayleyMenger_recovers_both
    (observable : TriangulationClass 6 → ℝ) :
    ¬ (observable oneTetClass = cayleyMengerObservable unitDecoration ∧
      observable oneTetClass = cayleyMengerObservable doubleDecoration) := by
  rw [unitDecoration_cayleyMenger, doubleDecoration_cayleyMenger]
  rintro ⟨h₁, h₂⟩
  linarith

/-- **CARRIER BLOCKER.** The current `TriangulationClass` quotient forgets
physical metric data: its forgetful map from decorated simplicial geometries
is not injective. -/
theorem metricForget_not_injective :
    ¬ Function.Injective
      (MetricDecoratedComplex.toClass :
        MetricDecoratedComplex 6 → TriangulationClass 6) := by
  intro hinj
  exact unitMetricOneTet_ne_doubleMetricOneTet
    (hinj unit_double_toClass_eq)

What this page does not claim

It does not claim that the two metric decorations represent different physical spacetimes; they are the same combinatorial tetrahedron with different edge lengths. It does not claim that the MetricRefinementFamily exists; it is a proposed carrier interface, not a constructed object. It does not claim that a continuum limit of the path sum exists, only that the family is sufficient to state the proposition.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/MetricRefinementCarrierBlocker.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: