Gravity Seven Gaps Simplicial Class

The simplicial subclass

In combinatorial geometry, a simplicial complex is a shape built from points, line segments, triangles, and their higher-dimensional counterparts, glued together so that every piece is a standard simplex. The simplicial class in the gravity seven gaps module is the collection of such well-formed 3-dimensional complexes inside a broader, messier configuration space. The broader space, called the bounded incidence configuration class, also admits degenerate edges, repeated vertices, multi-edges, and tetrahedra whose edges are missing from the edge list. The simplicial subclass carves out the configurations that respect the usual rules: no zero-length edges, no duplicate edges, four distinct vertices per tetrahedron, and every edge of a tetrahedron present in the complex.

This distinction matters because the larger class is what the path-sum measure sums over, but its unruly members complicate counting and normalization. The module proves that the simplicial subclass is a finite type with strictly positive cardinality, meaning it has at least one member. That non-emptiness is not left to the empty complex alone; the module constructs an explicit witness, the single tetrahedron with its full six edges, and proves it is simplicial. It also proves that any simplicial complex can be relaxed to a larger bound while staying simplicial, so the witness scales to every size bound of six or more.

In Recognition Science, this is a step toward a well-defined path-sum measure over gravity configurations. The framework models physical reality as a ledger, a discrete record of recognition events, and the path-sum measure assigns complex weights to configurations in that ledger. The simplicial subclass gives the measure a clean domain: a finite, non-empty set of bona fide triangulations. The module also records honest scope: it does not carry triangle face data, so it cannot express triangle closure, a property that would require that information.

The practical consequence is that the path-sum measure can be restricted to a well-behaved subclass without losing all configurations. The positivity theorem guarantees the subclass is never empty, and the explicit one-tetrahedron witness shows the measure has something to sum over at every size bound. This is groundwork: it does not yet compute any physical quantity, but it establishes that the simplicial configurations form a finite, non-empty domain for the measure.

/-- **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 (finiteness of the simplicial subclass).**  The simplicial
subclass inherits finiteness from the proved finiteness of the superclass
(`instFintypeBoundedComplex`) and decidability of the predicate. -/
instance instFintypeSimplicialComplex (B : ℕ) : Fintype (SimplicialComplex B) :=
  Subtype.fintype _

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

/-- Cap relaxation preserves the simplicial predicate (the predicate reads
only the incidence data, which `relax` preserves definitionally). -/
theorem relax_isSimplicial {B B' : ℕ} (h : B ≤ B') {K : BoundedComplex B}
    (hK : IsSimplicial K) : IsSimplicial (relax h K) :=
  hK

/-- Status flags (rfl-forced). -/
theorem simplicialClassStatus_flags :
    simplicialClassStatus.simplicial_predicate_decidable = true ∧
    simplicialClassStatus.subclass_fintype_proved = true ∧
    simplicialClassStatus.subclass_card_pos_proved = true ∧
    simplicialClassStatus.nonvacuous_witness_constructed = true ∧
    simplicialClassStatus.triangle_closure_expressible = false :=
  ⟨rfl, rfl, rfl, rfl, rfl⟩

What this page does not claim

The module does not compute any physical quantity or predict any measurement. The simplicial subclass is not claimed to be the only physically relevant configuration class. Triangle closure is not claimed to be 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: