Encyclopedia Gravity Gravity Seven Gaps Regulator Removal No Go Shell Mass Unbounded

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Regulator Removal No Go Shell Mass Unbounded

A counting argument in a discrete model of gravity shows that a certain sum over shapes grows without limit, which blocks one naive way of removing a mathematical smoothing device.

Verify this page

The unbounded shell mass

In the framework's discrete model of gravity, a ledger (a discrete record of events) keeps track of geometric complexes built from vertices, edges, and tetrahedra. The declaration shellMass_unbounded concerns a quantity called shell mass, which is a sum over equivalence classes of these complexes, where each class contributes a weight of one divided by the size of its symmetry group. The theorem proves that this shell mass has no upper bound: for any real number C, there exists a natural number n such that the shell mass at n is greater than C.

The proof works by restricting attention to a single signature where the numbers of vertices, edges, and tetrahedra are all equal to n. For this signature, the shell mass is at least n^(3n). This lower bound grows faster than any polynomial, so the shell mass diverges. The mechanism is a counting argument: the number of labeled complexes grows so quickly that it overwhelms the factorial factor that divides it in the symmetry-weighted sum.

This divergence has a consequence for a specific mathematical procedure. The framework considers a path sum with a Gaussian regulator, a smoothing factor that depends on a parameter rho. One might hope to remove the regulator by taking the limit as rho approaches zero from above. The theorem not_hasZRSRegulatorRemoval_zeroPhase proves that at zero phase, this limit does not exist. Because every term in the sum is nonnegative at zero phase, a single shell with sufficiently large mass forces the regulated sum to exceed any proposed limit, contradicting the existence of the limit.

In Recognition Science, this result is a no-go theorem: it closes off one specific route to defining the path sum by removing the regulator. It does not, however, say anything about the case where the phases are not all zero. With oscillatory phases, the positivity argument fails, and the question of whether a limit exists remains open. The framework also does not claim that this result says anything about a physical continuum limit; the discrete cutoff here is not mesh refinement.

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 shellMass_lower · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
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 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 apply to nonzero phases, where terms can cancel through oscillation. The theorem says nothing about a physical continuum limit, as the discrete cutoff is not mesh refinement. The shell mass divergence is a property of the quotient-sum convention and is not the same as a labeled-sum convention.

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