Gravity Seven Gaps Path Sum Measure Bounded Complex Card Pos

A finite count of configurations

A bounded complex is a finite combinatorial description of a spacetime: a list of vertices, edges, and tetrahedra, together with the incidence maps that say which edge connects which vertices and which tetrahedron uses which four vertices. The bound is a cap on the number of each, so the whole collection of such complexes at a fixed scale is a finite set. The declaration boundedComplex_card_pos proves the cardinality of that set is strictly positive: there is at least one such complex, the empty one.

That finiteness is the foundation for a path-sum measure. The measure assigns to each labeled complex a weight equal to one over the size of its automorphism group, the number of relabelings that leave the complex unchanged. Because the collection is finite, the sum of these weights over all complexes is a finite sum, and the measure is well-defined. The positivity of the cardinality is the trivial but necessary fact that the sum is not over an empty set.

In Recognition Science, this is the scoped configuration class for a path-sum measure of gravity. The framework models spacetime configurations as combinatorial and equilateral at a fixed lattice scale, with all geometric data carried by the incidence maps. The finiteness proof discharges a count-finiteness assumption that was previously postulated in the family of admissible triangulations. The sharper exponential-growth semantics for exact simplicial classes remains open.

The declaration does not claim that the bound is sharp, that the configurations satisfy any simplicial constraints, or that the continuum limit of the path sum exists. It is a finiteness statement, not a derivation of the measure's physical content.

/-- The scoped class has at least one element (the empty complex). -/
theorem boundedComplex_card_pos (B : ℕ) : 0 < Fintype.card (BoundedComplex B) :=
  Fintype.card_pos

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

/-- The growth base of the proved family is the derived cardinal. -/
theorem provedFamily_growthBase_derived (B : ℕ) :
    (provedFamily B).growthBase = (Fintype.card (BoundedComplex B) : ℝ) := rfl

What this page does not claim

The bound is not claimed to be sharp or optimal. The configurations are not claimed to satisfy simplicial constraints. The continuum limit of the path sum is not claimed to exist.

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: