Gravity Seven Gaps Metric Refinement Carrier Blocker

The metric refinement carrier blocker

Recognition Science models physical structure from a discrete record of events, a ledger. Its current library represents a space as a simplicial complex, a shape built from triangles and their higher-dimensional cousins, with a quotient that identifies complexes which are the same up to relabeling. This quotient captures only combinatorial type: which pieces touch which, not how long the edges are. The metric refinement carrier blocker is a module in the framework's machine-checked library of formal theorems that exposes exactly what this omission costs.

The module proves a concrete obstruction. Take the simplest nonempty simplicial complex, a single tetrahedron. The library's quotient identifies two metric decorations of this tetrahedron: one where every edge has length 1, and one where every edge has length 2. Both land in the same quotient class, yet their edge lengths and their Cayley-Menger observable, a number that encodes the tetrahedron's volume, differ: 4 versus 256. The theorem metricForget_not_injective states that the map from metric-decorated complexes to the quotient is not injective. Consequently, no function on the quotient alone can recover either observable for both decorations. The combinatorial record is blind to geometry.

The blocker's second half proposes a carrier to repair this blindness. The structure MetricRefinementFamily supplies finite metric-decorated configuration spaces, a mesh that genuinely tends to zero, coarse projections, and control over local action steps. It does not assume the path sum converges. With a measure supplied separately, it is just enough to define the geometric finite-level path sum and state its continuum-limit proposition. This is a minimal proposed interface, not a finished construction.

In Recognition Science, the framework proves the obstruction and the witness results as theorems. The carrier interface is a model, a definitional choice. Building such a family from the recognition substrate, deriving its measure and action, and proving the geometric continuum theorem all remain open targets. The module changes what the framework can claim: it cannot yet derive gravity from the ledger alone, but it has a precise, kernel-checked statement of the gap it must cross.

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

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

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

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

The module does not prove that a metric refinement family exists. It does not derive the measure or action for the path sum. It does not claim the continuum limit is the Einstein-Hilbert action.

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: