Gravity Seven Gaps Metric Refinement Carrier Blocker No Class Only Mesh Recovers

The mesh obstruction

The declaration no_class_only_mesh_recovers_both proves a precise limitation: if you know only the combinatorial type of a geometric object, you cannot recover its metric size. The proof works with a simple tetrahedron, a four-point shape with six edges. The framework's library, a machine-checked collection of formal theorems, decorates this tetrahedron in two ways: one where every edge has squared length 1, and another where every edge has squared length 4. These are genuinely different metric objects, as their first edge lengths differ (1 versus 2) and their Cayley-Menger observable, a number computed from edge lengths that determines volume, differs (4 versus 256).

Yet both decorations map to the same combinatorial class, meaning they are the same shape up to relabeling. The theorem states that no function from the combinatorial class to real numbers can equal the first edge length for both decorations simultaneously. The proof is a simple contradiction: such a function would have to return both 1 and 2 for the same input. A companion theorem shows the same for the Cayley-Menger observable, which would have to return both 4 and 256. The forgetful map from metric-decorated complexes to combinatorial classes is therefore provably non-injective: distinct metric objects collapse to the same class.

The framework then supplies the missing carrier shape, MetricRefinementFamily, a structure that adds metric data to combinatorial complexes. It provides finite metric-decorated configuration spaces, a genuine mesh tending to zero, coarse projections, and summable local action-step control. This family does not assume convergence of the path sum; with a measure supplied separately, it is just enough to define the geometric finite-level path sum and state its continuum-limit proposition.

What this declaration does not claim is equally important. It does not prove that such a metric refinement family can be constructed from the recognition substrate, nor that its measure and action can be derived. Those remain open targets. It also does not change any full-theory flag, and complexity-cutoff convergence remains distinct from metric mesh refinement. The theorem is a blocker certificate: it shows why the combinatorial quotient alone is insufficient, and what additional structure is needed to proceed.

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

/-- Minimal metric-refinement and action-control data needed to replace a
bare complexity cutoff by a geometric refinement sequence.

`Config n` is the finite metric-decorated configuration space at level `n`.
`coarsen` identifies the adjacent-level histories whose action increments are
controlled. `mesh_tendsto_zero` is geometric refinement; `cap_strictMono`
separately records increasing combinatorial capacity. The summable
`actionStepError` is a local quantitative premise, not the desired path-sum
convergence conclusion. -/
structure MetricRefinementFamily where
  Config : ℕ → Type
  finiteConfig : ∀ n, Fintype (Config n)
  cap : ℕ → ℕ
  cap_strictMono : StrictMono cap
  decorated : ∀ n, Config n → MetricDecoratedComplex (cap n)
  coarsen : ∀ n, Config (n + 1) → Config n
  mesh : ℕ → ℝ
  mesh_pos : ∀ n, 0 < mesh n
  edgeLength_le_mesh :
    ∀ n (c : Config n) (e : Fin (decorated n c).carrier.nE),
      Real.sqrt ((decorated n c).metric.sqEdge e) ≤ mesh n
  mesh_attained :
    ∀ n, ∃ c : Config n, ∃ e : Fin (decorated n c).carrier.nE,
      Real.sqrt ((decorated n c).metric.sqEdge e) = mesh n
  mesh_tendsto_zero :
    Filter.Tendsto mesh Filter.atTop (nhds 0)
  action : ∀ n, Config n → ℝ
  actionStepError : ℕ → ℝ
  actionStepError_nonneg : ∀ n, 0 ≤ actionStepError n
  actionStepError_summable : Summable actionStepError
  action_step_control :
    ∀ n (c : Config (n + 1)),
      |action (n + 1) c - action n (coarsen n c)| ≤ actionStepError n

What this page does not claim

No metric refinement family has been constructed from the recognition substrate. No measure or action has been derived for such a family. The geometric continuum theorem has not been proved. Complexity-cutoff convergence is not the same as metric mesh refinement.

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: