Gravity Seven Gaps Path Sum Measure

The path sum measure

A path sum measure in discrete quantum gravity assigns a number to each possible configuration of spacetime, then adds them up with weights. The configurations here are bounded combinatorial triangulations: finite collections of tetrahedra glued along triangular faces, with vertices, edges, and tetrahedra labeled, and the total size capped by a bound B. All edges have the same fixed length, so the geometry is carried entirely by the incidence data: which vertices belong to which edges and tetrahedra. This is the standard causal dynamical triangulations (CDT) style measure class.

The measure mu(K) for a labeled complex K is 1 divided by the size of its automorphism group, the number of relabelings that map the complex to itself. A highly symmetric complex gets a smaller weight. The path sum Z(B, w) is the finite sum over all labeled complexes in the class of mu(K) times w(K), where w(K) is a complex weight. For the unitary choice w(K) = exp(i*S(K)) with a real action S, the modulus of each weight is exactly 1, so the sum is bounded by the number of configurations. The measure is a relabeling invariant: equivalent complexes get the same weight, so the sum respects the equivalence relation of relabeling isomorphism.

What the module proves, in the machine-checked library of formal theorems, is that this scoped path sum is mathematically sound. The configuration class is finite, the quotient by relabeling is finite, the automorphism group of each complex is finite and nonempty, and the measure is positive and at most 1. The path sum itself is finite with explicit modulus bounds, and it is invariant under relabeling. These are proved with zero unproved axioms, not assumed. Earlier claims that the recognition ledger's cost function derives this measure were retracted in 2026-07-26: the counting principle is label indifference, and the ledger cost is blind to it. The continuum limit as B approaches infinity remains open.

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

theorem status_relabel_invariance : pathSumMeasureStatus.relabel_invariance_proved = true := rfl

theorem status_measure_positive : pathSumMeasureStatus.measure_positive_proved = true := rfl

/-- **THEOREM (measure respects the equivalence).**  μ is a relabeling
invariant: equivalent complexes have equal measure. -/
theorem mu_congr {B : ℕ} {K K' : BoundedComplex B} (h : Equivalent K K') :
    mu K = mu K' := by
  obtain ⟨r⟩ := h
  unfold mu
  rw [Nat.card_congr r.autCongr]

/-- **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 status_quotient_finite : pathSumMeasureStatus.quotient_finite_proved = true := rfl

What this page does not claim

The continuum limit of the path sum is derived. The recognition ledger's cost function derives the measure. The path sum is a complete theory of quantum gravity with experimental predictions.

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: