Encyclopedia Gravity Gravity Seven Gaps Regulator Removal No Go Regulator Removal No Go Status Ground

ARTICLE 3 claims 2 theorems 1 model

Gravity Seven Gaps Regulator Removal No Go Regulator Removal No Go Status Ground

A machine-checked result closes one route to removing a smoothing regulator from a path sum, and names the oscillatory route that remains open.

Verify this page

The zero-phase no-go result

A regulator, a smoothing parameter that keeps a divergent sum finite, is a standard tool in physics. The question is whether the regulator can be removed, that is, whether the sum settles on a definite value as the smoothing is turned off. The declaration regulatorRemovalNoGoStatus_grounded records a proved answer for one specific case: at zero phase, the removal fails.

The setup is a quotient path sum over labeled complexes, where each equivalence class is weighted by the reciprocal of its automorphism group size, a symmetry factor. The result is a theorem, not a conjecture. The theorem not_hasZRSRegulatorRemoval_zeroPhase states that this regulated sum has no limit as the regulator parameter tends to zero from above. The proof is quantitative: the shell mass, the sum of symmetry-weighted measures for complexes with a fixed number of vertices, edges, and tetrahedra, grows without bound. A single shell, with mass exceeding any proposed limit, provides a lower bound that contradicts the existence of a limit.

The declaration also records what is not proved. It does not claim anything about oscillatory phases, where terms carry complex phases that could cancel. The definition OscillatoryRemovalOpen is a named open problem, a target for future work. The zero-phase result relies on positivity, which oscillation destroys, so the failure at zero phase does not transport to nonzero phases.

The declaration is a status record, a data structure with boolean flags, and a theorem that grounds those flags in the actual proofs. It is a compact summary of the state of the art: one route closed, one route open, and the boundary between them marked exactly.

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 · 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
MODEL OscillatoryRemovalOpen · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean
OscillatoryRemovalOpen · IndisputableMonolith/Gravity/SevenGaps/RegulatorRemovalNoGo.lean:503 
/-- **NAMED OPEN (definition only, NEVER claimed).**  Whether regulator
removal holds for SOME phase (in particular, for a genuine oscillatory
action phase whose cancellations could tame the diverging shell masses).
The zero-phase refutation above does NOT decide this: its lower-bound
argument uses positivity, which oscillation destroys.  No theorem in this
module asserts or refutes this Prop. -/
def OscillatoryRemovalOpen : Prop :=
  ∃ phase : ∀ n : ℕ, ExactPathClass n → ℝ, HasZRSRegulatorRemoval phase

What this page does not claim

This does not claim anything about regulator removal for oscillatory phases, which remains open. This does not claim that the physical continuum limit is reached by refining a mesh. This does not claim that the quotient-sum convention equals the 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