Encyclopedia Gravity Gravity Seven Gaps Regulator Removal No Go Single Shell Re Lower Bound

ARTICLE 5 claims 4 theorems 1 open

Gravity Seven Gaps Regulator Removal No Go Single Shell Re Lower Bound

A machine-checked theorem proves that a certain way of taming an infinite sum fails at zero phase, and names exactly what remains open.

Verify this page

The single-shell bound

In the Recognition Science framework, a ledger, a discrete record of events, can be used to build a path sum: a weighted total over all possible configurations. A common tool in such sums is a regulator, a smoothing factor that makes the infinite sum finite, with the hope that removing the regulator recovers a meaningful limit. The declaration single_shell_re_lower_bound establishes a precise obstruction to this removal in one specific case.

The theorem proves that at zero phase, where every term in the sum is real and nonnegative, a single shell of configurations bounds the entire regulated sum from below. The bound is explicit: for any positive regulator strength ρ and any shell size n₀, the regulated sum is at least exp(−ρ·n₀²) times the shell mass. Because the shell mass grows without bound as n₀ increases, this lower bound itself grows without bound as the regulator is removed. The consequence is a kernel-checked no-go: the regulated quotient path sum has no limit as the regulator strength tends to zero at zero phase.

The proof rests on a shell-mass identity, derived through the orbit-stabilizer theorem, which shows that the sum of per-class measures equals the labeled count divided by the full relabeling gauge volume. Restricting to a single signature gives a lower bound that grows faster than any polynomial, so the absolute or positive-term route to regulator removal is dead. This is a proved theorem in the framework's machine-checked library of formal theorems, with no unproved assumptions.

The theorem does not claim anything about oscillatory phases. When the action has a genuine phase, terms can cancel, and the positivity argument that drives the zero-phase no-go no longer applies. Regulator removal for a nonzero phase remains an explicitly named open problem. The theorem also does not address the physical continuum limit, which is a separate standing constraint, and it does not equate the quotient-sum convention used here with any other path-sum convention.

In plain terms, the declaration closes one door and leaves another open. It shows that a specific, positive-term approach to removing the regulator cannot work at zero phase, and it does so with a rigorous proof. What it does not do is rule out all possible approaches, especially those involving oscillatory phases, which remain a target for future work.

THEOREM single_shell_re_lower_bound · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
single_shell_re_lower_bound · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:447 
/-- **Single-shell lower bound.**  At zero phase every regulated term is
real and nonnegative, so any single shell bounds the real part of the
regulated path sum from below. -/
theorem single_shell_re_lower_bound (ρ : ℝ) (hρ : 0 < ρ) (n₀ : ℕ) :
    Real.exp (-ρ * (n₀ : ℝ) ^ 2) * shellMass n₀
      ≤ (Z_RS_uv ρ zeroPhase).re := by
  have hsC : Summable
      (fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) :=
    (summable_zRSUVShell ρ hρ zeroPhase).congr
      (fun n => zRSUVShell_zeroPhase_eq ρ n)
  have hsR : Summable
      (fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) :=
    Complex.summable_ofReal.mp hsC
  have hZ : Z_RS_uv ρ zeroPhase =
      ((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by
    unfold Z_RS_uv
    rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n),
      ← Complex.ofReal_tsum]
  rw [hZ, Complex.ofReal_re]
  exact hsR.le_tsum n₀
    (fun j _ => (mul_pos (Real.exp_pos _) (shellMass_pos j)).le)
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 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)
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

What this page does not claim

The theorem does not claim regulator removal is impossible for any nonzero phase, only that the zero-phase positivity argument fails. The theorem does not claim anything about the physical continuum limit, which is a separate standing constraint. The theorem does not equate the quotient-sum convention with any other path-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