Encyclopedia Gravity Gravity Seven Gaps Regulator Removal No Go Cube Sum Le Shell Mass

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Regulator Removal No Go Cube Sum Le Shell Mass

A machine-checked proof shows that a certain way of summing over discrete spacetime structures cannot be tamed by a standard smoothing trick, and it names precisely what remains unknown.

Verify this page

The shell-mass bound

In the Recognition Science framework, a path sum is a way of adding up contributions from many discrete geometric objects, each weighted by a symmetry factor. The declaration cube_sum_le_shellMass is a proved inequality about one such sum. It says that for any size n, the total weight of all objects in a particular family, the cube-like shells, is no larger than a quantity called the shell mass. That shell mass itself is defined as the sum of the reciprocal symmetry factors over all shells of that size.

The inequality is a stepping stone to a stronger, more striking result. The shell mass grows without bound as n increases. A separate proved theorem shows that for any real number C, there exists an n such that the shell mass exceeds C. This growth is driven by the fact that the number of labeled objects, which grows like n to the power 6n, overwhelms the factorial factor that counts how many ways those labels can be permuted. Labeled entropy beats the gauge volume.

That unbounded growth is the engine of the main no-go theorem. When a Gaussian regulator is applied at zero phase, every term in the path sum is real and nonnegative. A single shell then provides a lower bound on the whole regulated sum. As the regulator is removed, its effect on any fixed shell tends to 1, so the contribution from a shell with huge mass can be made arbitrarily large. No finite limit can exist. The framework's library proves this as not_hasZRSRegulatorRemoval_zeroPhase: regulator removal fails at zero phase.

In Recognition Science, this is a theorem, not a conjecture. The proof is machine-checked, with no unproved assumptions beyond the standard logical axioms. It is a statement about a specific mathematical construction, the quotient-sum convention with per-class measures of 1/|Aut|. It does not claim anything about other conventions or about the physical continuum limit.

What the result does not claim is as important as what it proves. It says nothing about oscillatory phases, where terms can have signs and cancellation might occur. The lower-bound argument relies on positivity, which oscillation destroys. Regulator removal for a genuine action phase remains an open problem, recorded as such in the library. The result also says nothing about the physical continuum limit, because the complexity cutoff is not mesh refinement. The theorem is a sharp mathematical fact, not a statement about the ultimate nature of spacetime.

THEOREM cube_sum_le_shellMass · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
cube_sum_le_shellMass · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:351 
/-- Restricting the shell mass to the single cube signature `(n, n, n)`
bounds it from below (all classes carry positive measure). -/
theorem cube_sum_le_shellMass (n : ℕ) :
    ∑ q : Quotient (exactSetoid n n n), classMuOn n n n q ≤ shellMass n := by
  classical
  have himg : ∑ c ∈ Finset.univ.image
        (fun q : Quotient (exactSetoid n n n) =>
          (⟨cubeSig n, q⟩ : ExactPathClass n)),
      classMu c
      = ∑ q : Quotient (exactSetoid n n n),
          classMu (⟨cubeSig n, q⟩ : ExactPathClass n) :=
    Finset.sum_image
      (f := fun c : ExactPathClass n => classMu c)
      (s := (Finset.univ : Finset (Quotient (exactSetoid n n n))))
      (g := fun q : Quotient (exactSetoid n n n) =>
        (⟨cubeSig n, q⟩ : ExactPathClass n))
      (by
        intro q _ q' _ h
        cases h
        rfl)
  calc ∑ q : Quotient (exactSetoid n n n), classMuOn n n n q
      = ∑ q : Quotient (exactSetoid n n n),
          classMu (⟨cubeSig n, q⟩ : ExactPathClass n) :=
        Finset.sum_congr rfl fun q _ => rfl
    _ = ∑ c ∈ Finset.univ.image
          (fun q : Quotient (exactSetoid n n n) =>
            (⟨cubeSig n, q⟩ : ExactPathClass n)),
          classMu c := himg.symm
    _ ≤ ∑ c : ExactPathClass n, classMu c :=
        Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ _)
          (fun c _ _ => (classMu_pos c).le)
    _ = shellMass n := rfl
THEOREM shellMass_unbounded · 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
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

What this page does not claim

The result does not claim anything about oscillatory phases, where regulator removal remains open. The result does not claim anything about the physical continuum limit, as the complexity cutoff is not mesh refinement. The result does not claim that the quotient-sum convention is the only valid one.

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