Gravity Seven Gaps Metric Refinement Carrier Blocker Unit Metric One Tet Ne Doub

Two shapes, one shadow

A tetrahedron is the simplest three-dimensional shape: four triangular faces, six edges, four vertices. In the framework's ledger, a discrete record of events, a tetrahedron can be described in two ways. One description records only how its pieces connect, the combinatorial type. The other records actual sizes, the metric data, such as edge lengths. The declaration unitMetricOneTet_ne_doubleMetricOneTet proves that two specific tetrahedra, one with all edges of length 1 and one with all edges of length 2, are different objects when their metric data is included.

The proof is a machine-checked result in the framework's library of formal statements. It works by showing that the two tetrahedra have different first edge lengths, 1 versus 2, and different Cayley-Menger observables, a number computed from edge lengths that determines volume, 4 versus 256. Because these numbers differ, the two metric-decorated complexes cannot be the same. The result also proves that these two distinct tetrahedra map to the same combinatorial class, the same shadow, when metric data is forgotten. This is the key obstruction: any function that sees only the combinatorial class cannot recover both edge lengths or both volumes.

The result establishes a concrete limitation of the current combinatorial carrier in the framework's gravity program. The carrier, called BoundedComplex, records only cardinalities and incidence maps, so its quotient identifies combinatorial types, not metric geometries. The result shows this forgetful map is explicitly non-injective: two different metric geometries collapse to one combinatorial class. No function on the quotient alone can distinguish them, which means the current carrier cannot support metric-dependent observables like volume or action.

The framework responds by proposing a new carrier shape, MetricRefinementFamily, which includes finite metric-decorated configuration spaces, a mesh tending to zero, and summable local action-step control. This family is just enough to define a geometric finite-level path sum and state its continuum-limit proposition, assuming a measure is supplied separately. However, constructing such a family from the recognition substrate, deriving its measure and action, and proving the geometric continuum result remain open targets. The result does not claim convergence of the path sum, and no full-theory flag is changed.

theorem unitMetricOneTet_ne_doubleMetricOneTet :
    unitMetricOneTet ≠ doubleMetricOneTet := by
  intro h
  have hsig := congrArg
    (fun G : MetricDecoratedComplex 6 =>
      (⟨G.carrier, G.metric⟩ : Σ K : BoundedComplex 6, MetricDecoration K)) h
  simp only [Sigma.mk.injEq] at hsig
  exact unitDecoration_ne_doubleDecoration (eq_of_heq hsig.2)

theorem unit_double_toClass_eq :
    unitMetricOneTet.toClass = doubleMetricOneTet.toClass := rfl

/-- **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)

/-- **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)

/-- 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

What this page does not claim

This result does not claim that the two tetrahedra are combinatorially different; they are the same combinatorial type. This result does not claim that the path sum converges or that a continuum limit exists. This result does not claim that the proposed MetricRefinementFamily has been constructed from the recognition substrate.

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: