Gravity Seven Gaps Simplicial Class Empty Complex Is Simplicial

The empty complex

A simplicial complex is a way of assembling geometric building blocks: points, line segments, triangles, and tetrahedra, with the rule that any face of a piece is itself present. The empty complex is the configuration with none of these pieces at all. The declaration emptyComplex_isSimplicial proves, in the framework's machine-checked library of formal theorems, that this empty configuration satisfies the definition of a simplicial complex.

The proof works by checking the four conditions that define the simplicial property in this framework. Since there are no edges, the conditions about edges having distinct endpoints and no duplicates hold vacuously. Since there are no tetrahedra, the conditions about tetrahedra having distinct vertices and having all their edges present also hold vacuously. The theorem establishes that the empty complex is simplicial for any bound on the number of vertices, edges, or tetrahedra.

This result matters because it guarantees that the class of simplicial complexes is never empty. A separate theorem, simplicialComplex_card_pos, uses this to prove that the number of simplicial complexes is always positive. The framework also constructs a nonempty example, the single tetrahedron with its six edges, so the positivity does not rest on the empty complex alone. This nonempty witness is what allows the framework to define a partition function over simplicial complexes without the risk of summing over nothing.

The declaration does not claim that the empty complex is a meaningful physical configuration, nor that it contributes to any physical sum. It only establishes a formal property: the empty complex belongs to the simplicial subclass. The framework's own status record notes that triangle closure is not expressible in this data structure, since face data is not carried. The empty complex being simplicial is a combinatorial fact, not a statement about gravity or path sums.

/-- The empty complex is (vacuously) simplicial. -/
theorem emptyComplex_isSimplicial (B : ℕ) : IsSimplicial (emptyComplex B) := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · intro e; exact e.elim0
  · intro e; exact e.elim0
  · intro t; exact t.elim0
  · intro t; exact t.elim0

/-- **THEOREM (positive count).**  The simplicial subclass is nonempty for
every size cap, so the restricted path sum has a nontrivial configuration
space. -/
theorem simplicialComplex_card_pos (B : ℕ) :
    0 < Fintype.card (SimplicialComplex B) :=
  Fintype.card_pos

/-- **THEOREM (non-vacuous simplicial witness).**  The single-tetrahedron
complex is simplicial: distinct edge endpoints, no multi-edges, injective
corners, and every corner pair realized by one of the six skeleton edges.
Kernel-checked by `decide` on the finite index types (`Fin 4`, `Fin 6`,
`Fin 1`); no `native_decide`. -/
theorem oneTetComplex_isSimplicial : IsSimplicial oneTetComplex := by
  decide

What this page does not claim

The empty complex represents a physical configuration in gravity. The empty complex contributes to the path-sum measure. Triangle closure is expressible in the current data structure.

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