Gravity Seven Gaps Exact Shell Gauge Uv Exact Path Class Unbounded Support

Every complexity shell is occupied

The declaration exactPathClass_unbounded_support establishes a simple but foundational fact about a discrete model of spacetime geometry: every complexity shell contains at least one configuration. In plain language, if you sort all possible discrete complexes, built from vertices, edges, and tetrahedra, by a measure of their complexity, then no matter how high you set the complexity level, there is always something there. The witness is a configuration of n isolated vertices, meaning n points with no edges or tetrahedra connecting them. This is a theorem, proved in the machine-checked library of formal theorems, with no unproved assumptions.

The complexity of a complex is defined as the largest of three numbers: its count of vertices, edges, and tetrahedra. The theorem states that for any natural number n, the set of equivalence classes of complexes with complexity exactly n has more than zero elements. This is not a claim about physics directly; it is a claim about the mathematical structure used in the framework's path-sum over discrete geometries. It guarantees that the sum over complexity shells does not silently skip a level, which would otherwise be a gap in the formal construction.

What the theorem does not claim is equally important. It does not say that the isolated-vertices configuration is physically meaningful, only that it exists in the mathematical set. It does not claim that the complexity measure is derived from physical principles; the measure is a modeling choice. And it does not claim anything about the continuum limit, the limit in which the discrete complexity cutoff is removed. That limit remains an open target, recorded in the framework's status structure but not proved.

In Recognition Science, this theorem is a small but necessary piece of a larger construction: the regulated path sum over discrete geometries. The path sum assigns a weight to each configuration and sums them, shell by shell. Without the unbounded support theorem, the sum could not be guaranteed to be well-defined at every level. With it, the framework can proceed to the next stage, which is proving that the regulated sum converges for any positive regulator strength.

/-- **THEOREM (S1d, unbounded support).**  EVERY shell is inhabited: the
`n`-isolated-vertices complex has complexity exactly `n`, so no shell is
eventually empty. -/
theorem exactPathClass_unbounded_support (n : ℕ) :
    0 < Nat.card (ExactPathClass n) :=
  Nat.card_pos

What this page does not claim

The theorem does not claim that the isolated-vertices configuration is physically meaningful. The theorem does not claim that the complexity measure is derived from physical principles. The theorem does not claim anything about the continuum limit.

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/ExactShellGaugeUV.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: