Gravity Seven Gaps Simplicial Class Zsimp Norm Le Card

The simplicial bound

A simplicial complex is a collection of points, line segments, triangles, and their higher-dimensional cousins, glued together so that any two pieces meet along a whole face. The declaration Zsimp_norm_le_card concerns a special kind of sum over such complexes, and it proves a simple bound: if each individual complex contributes at most one unit of weight, then the total sum cannot exceed the number of complexes being summed.

In the Recognition Science framework, this sum is a partition function, a weighted count over configurations that physicists use to summarize how much each possible state contributes. The theorem restricts attention to the simplicial subclass: complexes with no degenerate edges, no repeated edges, four distinct vertices per tetrahedron, and a closed skeleton where every vertex pair in a tetrahedron is realized by an edge. These are exactly the well-formed triangular building blocks one expects from an abstract simplicial 3-complex.

The bound itself is a triangle inequality applied to a finite sum. The framework's machine-checked library of formal theorems proves that the absolute value of the sum is at most the number of simplicial complexes in the finite type, given that each weight has norm at most one. This is a statement about the size of a sum, not about any particular physical value.

What the theorem does not claim is just as important. The underlying data structure carries vertices, edges, and tetrahedra, but not triangle faces. Triangle closure, the condition that every triangle face of a tetrahedron is present, is therefore not expressible in this setting. The framework records this honestly in a status flag set to false, making clear that the simplicial class here is a combinatorial subclass, not the full geometric notion.

For the reader, the consequence is a clean guarantee: within this subclass, the partition function cannot blow up beyond the count of its terms. The bound is a stepping stone, not a destination. It establishes a finite ceiling for a weighted sum over well-formed complexes, and it names the missing triangle condition as the next target for the framework's development.

/-- **THEOREM (UV-finiteness of the simplicial path sum).**  For unit-modulus
weights the restricted path sum is bounded by the simplicial configuration
count. -/
theorem Zsimp_norm_le_card (B : ℕ) (w : BoundedComplex B → ℂ)
    (hw : ∀ K, ‖w K‖ ≤ 1) :
    ‖Zsimp B w‖ ≤ (Fintype.card (SimplicialComplex B) : ℝ) := by
  unfold Zsimp
  calc ‖∑ K : SimplicialComplex B, (mu K.1 : ℂ) * w K.1‖
      ≤ ∑ K : SimplicialComplex B, ‖(mu K.1 : ℂ) * w K.1‖ := norm_sum_le _ _
    _ ≤ ∑ _K : SimplicialComplex 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.1)]
        calc mu K.1 * ‖w K.1‖
            ≤ 1 * 1 := mul_le_mul (mu_le_one K.1) (hw K.1)
              (norm_nonneg _) zero_le_one
          _ = 1 := one_mul 1
    _ = (Fintype.card (SimplicialComplex B) : ℝ) := by
        rw [Finset.sum_const, Finset.card_univ, nsmul_eq_mul, mul_one]

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

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

This does not claim that the partition function equals any physical observable. This does not claim that the simplicial class includes all geometric simplicial complexes, since triangle faces are absent. This does not claim that the bound is sharp or that it applies to the full bounded configuration class.

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: