Gravity Seven Gaps Path Sum Measure Triangulation Class Finite

A finite class of shapes

In combinatorial geometry, a triangulation is a way to divide a space into simplexes: triangles in two dimensions, tetrahedra in three. When the space is a finite piece of a lattice, the number of possible triangulations is itself finite, because there are only finitely many ways to connect a fixed set of points. The declaration triangulationClass_finite in the Recognition Science library proves exactly this finiteness for a specific, bounded class of configurations.

The class in question, called BoundedComplex, contains combinatorial data: counts of vertices, edges, and tetrahedra, plus the incidence maps that say which vertices belong to which edges and tetrahedra. It is bounded in the sense that all counts are capped by a natural number B. The theorem establishes that this class is a finite type, meaning there are finitely many such configurations. It then goes further: it shows that the quotient of this class by relabeling isomorphism, called TriangulationClass, is also finite. Relabeling means renaming the vertices, edges, and tetrahedra; two configurations that differ only by such a renaming are considered the same class.

Why does finiteness matter? In the framework of Recognition Science, a discrete gravity path sum is defined as a sum over all triangulations of a weight, with each configuration weighted by a symmetry factor. A finite sum is well-defined and converges trivially. The theorem provides the mathematical foundation for this sum: it guarantees that the sum over the labeled class is finite, and that the sum over the relabeled class is finite as well. This is a necessary condition for any discrete path integral to make sense.

The theorem does not claim that the class contains only simplicial complexes. The bounded class is a superclass: it contains all bounded triangulations, but also configurations that do not satisfy the full simplicial constraints, such as edges that share more than two faces. Finiteness of the superclass implies finiteness of any subclass, but the sharper exponential-growth semantics for exact simplicial classes remains open. The theorem also does not derive the continuum limit of the path sum as B tends to infinity; that limit is recorded as open in the library's status flags.

In Recognition Science, this finiteness result is a proved theorem, not a postulate. It is part of a larger effort to place discrete gravity on a rigorous footing. The practical consequence is that a path-sum measure over triangulations is mathematically legitimate: the sums are finite, the weights are bounded, and the measure respects relabeling symmetry. This is a necessary step, but it is not the final step; the continuum limit and the physical interpretation of the measure remain targets for future work.

/-- **THEOREM (count-finiteness).**  The scoped class of bounded
combinatorial triangulations is a finite type.  This is the proved
replacement for the assumed `growthBase` field. -/
instance instFintypeBoundedComplex (B : ℕ) : Fintype (BoundedComplex B) :=
  Fintype.ofEquiv (CodeType B) (codeEquiv B).symm

/-- **THEOREM (quotient finiteness).**  The set of combinatorially distinct
bounded triangulations is finite. -/
theorem triangulationClass_finite (B : ℕ) : Finite (TriangulationClass B) :=
  Quotient.finite _

/-- **THEOREM (UV-finiteness bound).**  For any weight of modulus at most 1,
`‖Z‖ ≤ card (BoundedComplex B)`: the path sum is finite with an explicit
proved bound, replacing the assumed `growthBase^N` count. -/
theorem Z_norm_le_card (B : ℕ) (w : BoundedComplex B → ℂ)
    (hw : ∀ K, ‖w K‖ ≤ 1) :
    ‖Z B w‖ ≤ (Fintype.card (BoundedComplex B) : ℝ) := by
  unfold Z
  calc ‖∑ K : BoundedComplex B, (mu K : ℂ) * w K‖
      ≤ ∑ K : BoundedComplex B, ‖(mu K : ℂ) * w K‖ := norm_sum_le _ _
    _ ≤ ∑ _K : BoundedComplex B, (1 : ℝ) := by
        refine Finset.sum_le_sum fun K _ => ?_
        rw [norm_mul, Complex.norm_real, Real.norm_eq_abs, abs_of_pos (mu_pos K)]
        calc mu K * ‖w K‖
            ≤ 1 * 1 := mul_le_mul (mu_le_one K) (hw K) (norm_nonneg _) zero_le_one
          _ = 1 := one_mul 1
    _ = (Fintype.card (BoundedComplex B) : ℝ) := by
        rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]

What this page does not claim

The theorem does not claim that the bounded class contains only simplicial complexes. The theorem does not derive the continuum limit of the path sum. The theorem does not prove that the measure is derived from substrate structure; that remains open.

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