Gravity Seven Gaps Simplicial Class Exists Simplicial With Tet

The non-empty simplicial class

In the Recognition Science framework's study of gravity, a central object is a ledger: a discrete record of events. For the path-sum measure, the ledger takes the form of a bounded incidence configuration, a finite bookkeeping of vertices, edges, and tetrahedra. The framework's library of formal theorems, a machine-checked collection, proves a specific existence statement about this class.

The declaration exists_simplicial_with_tet proves that, for any bound B of at least 6, there exists a bounded incidence configuration that is simplicial and contains at least one tetrahedron. The proof is constructive: it exhibits the single tetrahedron with its full set of six edges as the witness. This is not a vacuous statement about the empty complex; it guarantees a non-trivial member of the class.

The simplicial conditions are precise. The configuration must have no degenerate edges (distinct endpoints), no multi-edges (each edge is a unique unordered pair), each tetrahedron must have four distinct vertices, and the skeleton must be closed (every vertex pair of a tetrahedron is realized by an edge). The proof that this witness is simplicial is a finite combinatorial check, carried out by the `decide` tactic.

This existence result is a stepping stone. It ensures the simplicial subclass is not empty, which is a prerequisite for the positivity of its cardinality and for defining the restricted path-sum measure Zsimp over this subclass. The theorem itself, however, does not claim that this measure is physically realized, nor does it assert anything about the triangle faces of the tetrahedra. The framework's data structure for bounded complexes does not carry face data, so triangle closure is not expressible in this setting; the declaration simplicialClassStatus records this as an honest scope limitation.

/-- **THEOREM.**  Every cap `B ≥ 6` admits a genuinely 3-dimensional
simplicial configuration (one tetrahedron, full skeleton): the subclass
positivity is not carried by the empty complex alone. -/
theorem exists_simplicial_with_tet (B : ℕ) (hB : 6 ≤ B) :
    ∃ K : SimplicialComplex B, 0 < K.1.nT :=
  ⟨⟨relax hB oneTetComplex, relax_isSimplicial hB oneTetComplex_isSimplicial⟩,
    Nat.one_pos⟩

/-- The single-tetrahedron complex at the minimal cap: 4 vertices, 6 edges
(the complete 1-skeleton), 1 tetrahedron. -/
def oneTetComplex : BoundedComplex 6 where
  nV := 4
  nE := 6
  nT := 1
  hV := by omega
  hE := le_refl 6
  hT := by omega
  edgeVerts := tetEdges
  tetVerts := fun _ i => i

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

/-- **The simplicial predicate** on a bounded incidence configuration:
no degenerate edges, no multi-edges, injective tetrahedron corners, and
skeleton closure (every corner pair of every tet is an edge of the
complex). -/
def IsSimplicial {B : ℕ} (K : BoundedComplex B) : Prop :=
  (∀ e : Fin K.nE, (K.edgeVerts e).1 ≠ (K.edgeVerts e).2) ∧
  (∀ e e' : Fin K.nE,
    sameUnorderedPair (K.edgeVerts e) (K.edgeVerts e') → e = e') ∧
  (∀ t : Fin K.nT, Function.Injective (K.tetVerts t)) ∧
  (∀ (t : Fin K.nT) (i j : Fin 4), i ≠ j →
    ∃ e : Fin K.nE,
      sameUnorderedPair (K.edgeVerts e) (K.tetVerts t i, K.tetVerts t j))

/-- The Phase-0b status record. -/
def simplicialClassStatus : SimplicialClassStatus where
  simplicial_predicate_decidable := true
  subclass_fintype_proved := true
  subclass_card_pos_proved := true
  nonvacuous_witness_constructed := true
  triangle_closure_expressible := false

What this page does not claim

The theorem does not claim that the simplicial class is the physically realized one, only that it is non-empty. The theorem does not claim anything about triangle faces, as the data structure cannot express them. The theorem does not prove that every simplicial complex is a tetrahedron.

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: