Encyclopedia Gravity Gravity Seven Gaps Regulator Removal No Go

ARTICLE 4 claims 3 theorems 1 open

Gravity Seven Gaps Regulator Removal No Go

A machine-checked proof shows that a certain way of taming an infinite sum in gravity fails at zero phase, and why the door stays open for other phases.

Verify this page

The regulator no-go

In Recognition Science, a central object is a ledger, a discrete record of events. For gravity, the framework builds a path sum over discrete complexes, a kind of bookkeeping over all possible ways to arrange vertices, edges, and tetrahedra. To make the sum finite, it introduces a Gaussian regulator, a smoothing factor that suppresses large contributions. The question is whether the regulator can be removed, that is, whether the sum has a well-defined limit as the smoothing is turned off.

The module Seven Gaps: Regulator Removal No Go answers this question for one specific case: the zero phase, where every term in the sum is real and nonnegative. The answer is no. The framework's machine-checked library of formal theorems proves that the regulated sum has no limit as the regulator strength goes to zero. The proof is quantitative. It shows that the sum of the shell masses, which are the contributions from complexes with a fixed number of vertices, edges, and tetrahedra, grows without bound. In fact, for a shell with n of each, the mass is at least n^(3n). This growth is so fast that it overwhelms any possible finite limit.

The mechanism is a Burnside-style identity. The framework counts complexes up to relabeling, and the sum of the per-class measures equals the labeled count divided by the full relabeling gauge volume, which is v!e!t!. This identity is proved via an orbit-stabilizer argument. The divergence then follows because the labeled entropy beats the factorial gauge volume. At zero phase, every term is nonnegative, so a single shell bounds the whole sum from below. As the regulator tends to one on any fixed shell, any putative limit is exceeded by a shell with mass greater than the limit plus two. This contradiction is the kernel no-go theorem.

In Recognition Science, this result is a theorem, not a conjecture. It is proved in the framework's library with zero axioms beyond the standard trio. The result does not say anything about nonzero phases. There, the terms can have complex phases that might cancel, and the question of regulator removal remains open. The framework explicitly names this as an open problem. The result also says nothing about the physical continuum limit, which is a separate and standing constraint.

The practical consequence is that one naive route to a finite gravitational path sum is closed. The absolute-value or positive-term approach cannot work. Any successful construction must exploit cancellations between phases. This is a precise, formal statement about the structure of the framework's gravity path sum, and it directs future work toward oscillatory phases.

THEOREM not_hasZRSRegulatorRemoval_zeroPhase · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
not_hasZRSRegulatorRemoval_zeroPhase · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:469 
/-- **HEADLINE (kernel no-go).**  Regulator removal FAILS at zero phase:
the Gaussian-regulated quotient path sum `Z_RS_uv ρ zeroPhase` has NO
limit as `ρ → 0⁺`.  Mechanism: any putative limit `L` is beaten by a
single shell of mass `> L.re + 2` (shell masses diverge), whose regulated
contribution tends to its full mass as the regulator is removed. -/
theorem not_hasZRSRegulatorRemoval_zeroPhase :
    ¬ HasZRSRegulatorRemoval zeroPhase := by
  rintro ⟨L, hL⟩
  have hre : Filter.Tendsto (fun ρ : ℝ => (Z_RS_uv ρ zeroPhase).re)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds L.re) :=
    (Complex.continuous_re.tendsto L).comp hL
  obtain ⟨n₀, hn₀⟩ := shellMass_unbounded (L.re + 2)
  have hexp : Filter.Tendsto
      (fun ρ : ℝ => Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀)
      (nhdsWithin 0 (Set.Ioi 0)) (nhds (shellMass n₀)) := by
    refine Filter.Tendsto.mono_left ?_ nhdsWithin_le_nhds
    refine Continuous.tendsto' ?_ 0 (shellMass n₀) ?_
    · exact (Real.continuous_exp.comp
        (continuous_neg.mul continuous_const)).mul continuous_const
    · simp only [neg_zero, zero_mul, Real.exp_zero, one_mul]
  have hev1 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0),
      L.re + 1 < Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀ :=
    hexp.eventually_const_lt (by linarith)
  have hev2 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0),
      (Z_RS_uv ρ zeroPhase).re < L.re + 1 :=
    hre.eventually_lt_const (by linarith)
  have hev3 : ∀ᶠ ρ in nhdsWithin (0 : ℝ) (Set.Ioi 0), ρ ∈ Set.Ioi (0 : ℝ) :=
    eventually_mem_nhdsWithin
  obtain ⟨ρ, ⟨h1, h2⟩, h3⟩ := ((hev1.and hev2).and hev3).exists
  have h4 := single_shell_re_lower_bound ρ (Set.mem_Ioi.mp h3) n₀
  linarith
THEOREM shellMass_unbounded · shellMass_lower · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
shellMass_unbounded · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:428 
/-- **HEADLINE DIVERGENCE.**  The shell masses are unbounded: for every
real threshold there is a shell whose total `1/|Aut|` mass exceeds it. -/
theorem shellMass_unbounded (C : ℝ) : ∃ n : ℕ, C < shellMass n := by
  obtain ⟨m, hm⟩ := exists_nat_gt C
  refine ⟨max 1 m, ?_⟩
  have hle : ((max 1 m : ℕ) : ℝ) ^ (3 * max 1 m) ≤ shellMass (max 1 m) :=
    shellMass_lower (max 1 m)
  have hselfN : (max 1 m : ℕ) ≤ (max 1 m) ^ (3 * max 1 m) :=
    Nat.le_self_pow (by omega) _
  have hself : ((max 1 m : ℕ) : ℝ) ≤ ((max 1 m : ℕ) : ℝ) ^ (3 * max 1 m) := by
    calc ((max 1 m : ℕ) : ℝ)
        ≤ (((max 1 m) ^ (3 * max 1 m) : ℕ) : ℝ) := by exact_mod_cast hselfN
      _ = ((max 1 m : ℕ) : ℝ) ^ (3 * max 1 m) := Nat.cast_pow _ _
  have hmR : (m : ℝ) ≤ ((max 1 m : ℕ) : ℝ) := by
    exact_mod_cast le_max_right 1 m
  linarith
shellMass_lower · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:384 
/-- **Quantitative shell-mass lower bound.**
`shellMass n ≥ n^(6n)/(n!)³ ≥ n^(3n)`: the labeled entropy of the cube
signature beats its factorial gauge volume. -/
theorem shellMass_lower (n : ℕ) :
    ((n : ℝ)) ^ (3 * n) ≤ shellMass n := by
  have hfact3 : n.factorial * n.factorial * n.factorial ≤ n ^ (3 * n) := by
    have h := Nat.factorial_le_pow n
    calc n.factorial * n.factorial * n.factorial
        ≤ n ^ n * n ^ n * n ^ n := Nat.mul_le_mul (Nat.mul_le_mul h h) h
      _ = n ^ (3 * n) := by
          rw [← pow_add, ← pow_add]
          congr 1
          omega
  have hcard : Fintype.card (ExactComplex n n n) = n ^ (6 * n) := by
    rw [exactComplex_card_eq, ← pow_two, ← pow_mul, ← pow_mul, ← pow_add]
    congr 1
    omega
  have hfactR : (0 : ℝ) < ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := by
    exact_mod_cast
      Nat.mul_pos (Nat.mul_pos n.factorial_pos n.factorial_pos) n.factorial_pos
  have hkey : ((n : ℝ)) ^ (3 * n)
      ≤ (Fintype.card (ExactComplex n n n) : ℝ)
        / ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := by
    rw [le_div_iff₀ hfactR]
    calc ((n : ℝ)) ^ (3 * n)
          * ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ)
        ≤ ((n : ℝ)) ^ (3 * n) * ((n : ℝ)) ^ (3 * n) := by
          refine mul_le_mul_of_nonneg_left ?_ (by positivity)
          calc ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ)
              ≤ ((n ^ (3 * n) : ℕ) : ℝ) := by exact_mod_cast hfact3
            _ = ((n : ℝ)) ^ (3 * n) := Nat.cast_pow n (3 * n)
      _ = ((n : ℝ)) ^ (6 * n) := by
          rw [← pow_add]
          congr 1
          omega
      _ = ((n ^ (6 * n) : ℕ) : ℝ) := (Nat.cast_pow n (6 * n)).symm
      _ = (Fintype.card (ExactComplex n n n) : ℝ) := by rw [hcard]
  calc ((n : ℝ)) ^ (3 * n)
      ≤ (Fintype.card (ExactComplex n n n) : ℝ)
          / ((n.factorial * n.factorial * n.factorial : ℕ) : ℝ) := hkey
    _ = ∑ q : Quotient (exactSetoid n n n), classMuOn n n n q :=
        (sum_classMuOn_eq_card_div_factorials n n n).symm
    _ ≤ shellMass n := cube_sum_le_shellMass n
THEOREM sum_classMuOn_eq_card_div_factorials · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
sum_classMuOn_eq_card_div_factorials · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:310 
/-- **HEADLINE IDENTITY (Burnside / orbit-stabilizer route).**  At every
exact signature, the total per-class measure equals the labeled count
divided by the full gauge volume:
`∑_classes 1/|Aut| = |labeled| / (v!·e!·t!)`. -/
theorem sum_classMuOn_eq_card_div_factorials (v e t : ℕ) :
    ∑ c : Quotient (exactSetoid v e t), classMuOn v e t c
      = (Fintype.card (ExactComplex v e t) : ℝ)
        / ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
  classical
  have hfactpos : 0 < v.factorial * e.factorial * t.factorial :=
    Nat.mul_pos (Nat.mul_pos v.factorial_pos e.factorial_pos) t.factorial_pos
  have hfactR : (0 : ℝ) < ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
    exact_mod_cast hfactpos
  rw [eq_div_iff hfactR.ne', Finset.sum_mul]
  have hterm : ∀ c : Quotient (exactSetoid v e t),
      classMuOn v e t c * ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ)
        = (orbitCard (Quotient.out c) : ℝ) := by
    intro c
    have hOS := orbitCard_mul_autCard (Quotient.out c)
    have hautpos : (0 : ℝ) < (Nat.card (ExactAut (Quotient.out c)) : ℝ) := by
      exact_mod_cast exactAutCard_pos (Quotient.out c)
    have hcast : (orbitCard (Quotient.out c) : ℝ)
        * (Nat.card (ExactAut (Quotient.out c)) : ℝ)
        = ((v.factorial * e.factorial * t.factorial : ℕ) : ℝ) := by
      exact_mod_cast congrArg (Nat.cast : ℕ → ℝ) hOS
    rw [classMuOn_out c]
    unfold exactMu
    rw [div_mul_eq_mul_div, one_mul, ← hcast, mul_div_assoc,
      div_self hautpos.ne', mul_one]
  rw [Finset.sum_congr rfl fun c _ => hterm c, ← Nat.cast_sum]
  exact_mod_cast congrArg (Nat.cast : ℕ → ℝ) (sum_orbitCard v e t)

What this page does not claim

This result does not apply to nonzero phases, where cancellation between complex phases might allow regulator removal. This result does not establish anything about the physical continuum limit, which is a separate and standing constraint. The quotient-sum convention used here is not the same as the labeled-sum convention used elsewhere in the framework.

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/RegulatorRemovalNoGo.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND