Gravity Seven Gaps Metric Refinement Carrier Blocker Unit Decoration Ne Double D

Two metric decorations

In geometry, a simplicial complex is a shape built from points, line segments, triangles, and their higher-dimensional cousins. The Recognition Science framework's machine-checked library of formal theorems works with a version that records only how these pieces connect, not their sizes. The declaration unitDecoration_ne_doubleDecoration proves a basic fact about this setup: two specific ways of assigning lengths to the edges of a single tetrahedron are not the same.

The first decoration gives every edge a squared length of 1, so each edge has length 1. The second gives every edge a squared length of 4, so each edge has length 2. The theorem states that these two metric decorations are unequal. The proof is direct: if they were equal, then their first edge lengths would have to match, but one is 1 and the other is 2. This is a THEOREM in the framework's library, meaning it is proved with no unverified assumptions.

This fact matters because the framework's current quotient, which identifies complexes up to relabeling, cannot tell these two decorations apart. Both map to the same equivalence class. The theorem therefore supports a larger point: the quotient alone lacks the information needed to recover metric observables like edge length or the Cayley-Menger determinant, a quantity computed from edge lengths. A separate structure, called a metric refinement family, is proposed as the missing carrier of this geometric data.

The declaration does not claim that these two decorations represent physically different spacetimes, nor does it assert that the proposed metric refinement family actually exists or can be constructed from the recognition substrate. It is a precise, local statement about two formal objects being distinct, used as a building block for a broader obstruction result.

/-- The two metric decorations are distinct, witnessed by their first edge
lengths. -/
theorem unitDecoration_ne_doubleDecoration :
    unitDecoration ≠ doubleDecoration := by
  intro h
  have hobs := congrArg firstEdgeLength h
  rw [unitDecoration_firstEdgeLength, doubleDecoration_firstEdgeLength] at hobs
  norm_num at hobs

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

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

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

What this page does not claim

The two decorations represent physically distinct spacetimes. A metric refinement family has been constructed. The continuum limit of the 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: