IndisputableMonolith.Gravity.SevenGaps.SimplicialClass
Defines the simplicial-complex configuration class used in the Seven Gaps gravity lane: unordered edge pairs, the IsSimplicial predicate, finite SimplicialComplex carriers, and explicit one-tetrahedron examples. Downstream shell and path-sum modules import it as the combinatorial substrate. The file is mostly definitions plus short Fintype and positivity lemmas.
claimA finite simplicial complex on a vertex set is a finite collection of unordered edges that is closed under the simplicial incidence rules used in the Seven Gaps path-sum setup. The module supplies the unordered-pair relation on ordered vertex pairs, the predicate $\mathrm{IsSimplicial}$, the type $\mathrm{SimplicialComplex}$, the empty complex, a one-tetrahedron complex with its six edges, and a relaxation map that preserves simpliciality.
background
Seven Gaps Lane 2 builds a proved path-sum measure $Z_{\mathrm{RS}}$ over bounded incidence configurations. The upstream module PathSumMeasure introduces the scoped class BoundedComplex and proves it is a Fintype via an explicit coding equivalence, with the honesty note that BoundedComplex carries arbitrary bounded incidence data.
This module specializes that combinatorial layer to simplicial complexes: edges are unordered pairs of vertices (via an equality that identifies $(i,j)$ with $(j,i)$), and IsSimplicial encodes the incidence constraints needed so that path sums and shell quotients see only well-formed complexes. Concrete generators include the empty complex and a single tetrahedron (six edges), which seed existence statements used later when shells must contain at least one tet-bearing configuration.
Notation stays RS-native and finite: complexes are Fintype carriers, so cardinality and positivity lemmas are available without classical choice beyond Mathlib.
proof idea
Definition-heavy module. Unordered-pair equality is a short Prop on ordered pairs. IsSimplicial and SimplicialComplex package the incidence data; Fintype instances follow from finite vertex/edge carriers. Empty and one-tet complexes are explicit constructions with direct simpliciality proofs. The relax map is shown to preserve IsSimplicial. Cardinality positivity and exists_simplicial_with_tet are elementary existence/card arguments on those constructions. No deep analytic content lives here.
why it matters in Recognition Science
ExactShellGaugeUV imports this module to organize quotient-class path-sum configuration space into exact complexity shells and to prove Gaussian-UV-regularized shell path sums $\sum e^{-\rho n^2}$ converge for every $\rho>0$. Without a clean simplicial class (Fintype, nonempty tet examples, relaxation), the shell stratification has no combinatorial carrier.
In the broader Recognition gravity program this is scaffolding for the discrete geometry behind the path-sum measure of $Z_{\mathrm{RS}}$, not a forcing-chain (T0–T8) step. It closes the gap between abstract BoundedComplex incidence data and the concrete simplicial complexes that shell and UV modules quantify over.
scope and limits
- Does not define or prove the path-sum measure $Z_{\mathrm{RS}}$ itself.
- Does not introduce complexity shells or Gaussian UV regulators.
- Does not claim geometric realization in continuum $\mathbb{R}^3$ or metric curvature.
- Does not bound physical constants ($G$, $\alpha$, masses) or invoke the phi-ladder.
- Does not prove uniqueness of the simplicial presentation among all BoundedComplex data.
used by (1)
depends on (1)
declarations in this module (17)
-
def
sameUnorderedPair -
def
IsSimplicial -
abbrev
SimplicialComplex -
instance
instFintypeSimplicialComplex -
theorem
emptyComplex_isSimplicial -
theorem
simplicialComplex_card_pos -
def
relax -
theorem
relax_isSimplicial -
def
tetEdges -
def
oneTetComplex -
theorem
oneTetComplex_isSimplicial -
theorem
exists_simplicial_with_tet -
def
Zsimp -
theorem
Zsimp_norm_le_card -
structure
SimplicialClassStatus -
def
simplicialClassStatus -
theorem
simplicialClassStatus_flags