Gravity Seven Gaps Path Sum Measure Status Relabel Invariance

Relabeling invariance

In discrete gravity, a triangulation of space is often described by listing its vertices, edges, and tetrahedra, and naming each one. Two descriptions that differ only in those names describe the same geometric object. A quantity that changes when the names change would be an artifact of bookkeeping, not a property of the geometry. The Recognition Science framework's ledger, a discrete record of events, treats this naming freedom as a relabeling of the configuration.

The declaration status_relabel_invariance records a proved theorem in the framework's machine-checked library of formal theorems. The theorem states that the path sum Z B w = Σ_K mu(K) · w(K), a sum over all bounded triangulations at a fixed scale, is invariant under any equivalence-preserving bijection of configurations. The measure mu K = 1 / |Aut K| divides by the size of the automorphism group, the number of relabelings that map a configuration to itself. This symmetry factor is the standard discrete-gravity convention, and the theorem proves that both the measure and the summand respect the equivalence relation. The sum therefore assigns the same value to any two descriptions of the same geometric object.

The theorem also establishes supporting finiteness facts. The class of bounded configurations is finite, the relabeling equivalence is a genuine equivalence relation with proved reflexivity, symmetry, and transitivity, and the quotient of configurations by relabeling is finite. The automorphism group of any labeled configuration is finite and nonempty, so the measure is always strictly between zero and one. These facts together discharge a count-finiteness assumption that was previously postulated, replacing a bound with a proved finite cardinal.

What the declaration does not claim is as important as what it proves. It does not derive the continuum limit of the path sum as the bound grows without limit; that remains open. It does not derive the measure from the recognition ledger's cost function; a separate result proves that the ledger's cost is blind to the site-symmetry counts that would be needed, so the premise that the substrate derives the gauge counting principle is named but not derived. The theorem also does not prove the orbit-counting identity that would equate the weighted labeled sum with a bare quotient sum. The invariance is a property of the chosen measure convention, not a derivation of that convention from deeper principles.

theorem status_relabel_invariance : pathSumMeasureStatus.relabel_invariance_proved = true := rfl

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

/-- Two bounded complexes are EQUIVALENT iff a relabeling isomorphism
exists between them. -/
def Equivalent {B : ℕ} (K K' : BoundedComplex B) : Prop :=
  Nonempty (Relabel K K')

theorem status_quotient_finite : pathSumMeasureStatus.quotient_finite_proved = true := rfl

/-- The automorphism count is positive (the identity is an automorphism). -/
theorem autCard_pos {B : ℕ} (K : BoundedComplex B) : 0 < Nat.card (Aut K) :=
  Nat.card_pos

theorem status_measure_positive : pathSumMeasureStatus.measure_positive_proved = true := rfl

What this page does not claim

The continuum limit of the path sum as the bound grows without limit is derived. The measure is derived from the recognition ledger's cost function. The orbit-counting identity equating the weighted labeled sum with a quotient sum is proved.

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: