Gravity Seven Gaps Path Sum Measure Status Measure Positive

A proved positive measure

The declaration status_measure_positive is a machine-checked proof that a particular measure, built for a class of bounded combinatorial triangulations, is always positive. The measure assigns to each labeled triangulation a weight equal to one divided by the size of its automorphism group, the group of relabelings that leave the triangulation unchanged. The proof shows this weight is always greater than zero and at most one, and that the total path sum built from these weights is finite and bounded. This is a theorem in the framework's library: it is proved with no unproved assumptions and no new axioms.

The classical setting is the discrete path-sum measure used in causal dynamical triangulations, a standard approach to quantum gravity in which spacetime is approximated by a sum over equilateral triangulations. The framework's version fixes a lattice scale, drops the metric field, and caps the size of the complex by a bound B. The finiteness of the class of bounded complexes is proved, not assumed, via an explicit encoding into a finite type. The relabeling equivalence is proved to be a genuine equivalence relation, and the quotient of triangulation classes is finite. The automorphism group of any labeled complex is finite and nonempty, which is what makes the symmetry factor well-defined and positive.

The path sum Z(B, w) = Σ_K mu(K) · w(K) is a finite sum over the labeled class, with the modulus bound ‖Z‖ ≤ Σ mu and ‖Z‖ ≤ card(BoundedComplex B). The measure is invariant under relabeling: if two configurations are equivalent, they receive the same weight, and the sum itself is invariant under any equivalence-preserving bijection of configurations. For the unitary weight w(K) = exp(i·S(K)) with a real action S, the modulus of each weight is one, so all bounds apply. This is the honest Z_RS statement for the scoped class.

In Recognition Science, this declaration is the second lane of the Seven Gaps program: it proves that a path-sum measure exists, is finite, is positive, and respects relabeling symmetry. It does not claim that the continuum limit as B tends to infinity is derived; that remains open. It does not claim that the measure is derived from the recognition ledger: a retracted 2026-07-26 claim that the substrate measure was derived is now explicitly false, because the ledger data was proved to be irrelevant to the counting. The declaration also does not claim the orbit-counting identity that would equate the weighted labeled sum with a bare quotient sum; that identity is not proved here.

/-- The path-sum measure: the standard `1/|Aut|` symmetry factor of each
labeled configuration.  (MODEL: uniform convention; a substrate-derived
nonuniform measure is OPEN, see `pathSumMeasureStatus`.) -/
noncomputable def mu {B : ℕ} (K : BoundedComplex B) : ℝ :=
  1 / (Nat.card (Aut K) : ℝ)

theorem status_measure_positive : pathSumMeasureStatus.measure_positive_proved = true := rfl

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

What this page does not claim

The continuum limit of the path sum is derived. The measure is derived from recognition-ledger information. The orbit-counting identity equating the weighted labeled sum with a quotient sum is proved. The scoped class enforces simplicial constraints, so it contains non-simplicial configurations.

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: