Gravity Seven Gaps Metric Refinement Carrier Blocker Double Decoration First Edg

Two edge lengths, one shape

A tetrahedron is a pyramid with four triangular faces. In the Recognition Science framework, a recognition event is a discrete record of what the universe counted as one thing; the framework's library is a machine-checked collection of formal theorems. The declaration doubleDecoration_firstEdgeLength proves a small but important fact about two such tetrahedra: one with all squared edge lengths equal to 1, and another with all squared edge lengths equal to 4. Their first edge lengths, the square roots of these values, are therefore 1 and 2 respectively.

The two tetrahedra are not the same object. The declaration unitDecoration_ne_doubleDecoration proves they differ, and their Cayley-Menger observables, a measure of volume, are 4 and 256. This matters because the framework's TriangulationClass quotient identifies combinatorial types, not metric geometries. Two metric decorations can land in the same class while carrying different edge lengths and volumes. The theorem metricForget_not_injective proves this forgetful map is not injective: distinct metric-decorated complexes can collapse to the same combinatorial type.

The consequence is a blocker. No function on the combinatorial class alone can recover the first edge length for both decorations, as no_class_only_mesh_recovers_both proves. The same holds for the Cayley-Menger observable. This obstruction is a P2.5 gap in the framework's gravity program, and it motivates the proposed MetricRefinementFamily carrier, a structure that carries metric data and mesh refinement to define a geometric path sum.

What the declaration does not claim: it does not prove that the two tetrahedra have different combinatorial types, only different metrics. It does not construct a MetricRefinementFamily from the recognition substrate, nor does it prove a continuum limit exists. Those remain open targets. The declaration is a precise witness to a specific obstruction, not a solution to it.

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

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

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

What this page does not claim

The two tetrahedra have different combinatorial types; they are the same simplicial complex with different metrics. A MetricRefinementFamily has been constructed from the recognition substrate. The continuum limit of the geometric path sum exists.

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: