Encyclopedia Gravity Gravity Seven Gaps Zq Continuum Blocker Has Exact Complexity Cutoff Limit Iff Ta

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Zq Continuum Blocker Has Exact Complexity Cutoff Limit Iff Ta

A machine-checked theorem pins down exactly when removing a computational cutoff in a gravity path sum yields a stable answer: the late terms must cancel.

Verify this page

The exact cutoff criterion

In the Recognition Science framework's machine-checked library of formal theorems, a central question is whether a sequence of finite sums, each approximating a more complex object, settles down to a definite value as the complexity cutoff is removed. The declaration hasExactComplexityCutoffLimit_iff_tailCancellation answers this precisely. It proves, for any phase assignment, that the sequence of exact complexity cutoff sums has a limit if and only if the tail of the sequence cancels: for any small tolerance, there is a cutoff beyond which the sum of any contiguous block of later shell amplitudes is smaller than that tolerance.

This is a Cauchy criterion in disguise. The theorem establishes that the sequence of partial sums, where each term is the sum over exact path classes up to a given complexity, converges exactly when the differences between later partial sums shrink to zero. The proof uses exact telescoping: the difference between two partial sums equals the sum of the shell amplitudes in the intervening range. The zero phase, where all phases are set to zero, provides a sharp counterexample: it fails the tail cancellation condition, and the theorem then shows that its cutoff sums do not converge.

The statement is deliberately narrow. It concerns only the removal of a complexity cutoff in a specific phased quotient path sum. It says nothing about mesh refinement in numerical analysis, about the existence of a continuum geometry, about any observable prediction, about the rate of convergence, or about a derived measure on the full theory. The theorem is a precise analytical tool: it tells you exactly when a certain infinite process stabilizes, and it gives a concrete test for that stabilization.

What changes with this result is the ability to speak rigorously about a limit that was previously only formal. The framework's library can now distinguish, for each phase model, whether the complexity cutoff can be removed at all. The zero phase failure is not a defect but a feature: it shows the criterion is discriminating. A phase that satisfies tail cancellation is one for which the infinite sum is well-defined; a phase that does not is one where the cutoff is essential and cannot be dropped.

THEOREM hasExactComplexityCutoffLimit_iff_tailCancellation · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean
hasExactComplexityCutoffLimit_iff_tailCancellation · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:174 
/-- **HEADLINE IFF, ORDERED-TAIL FORM.** The unregulated exact-shell quotient
cutoff has a limit exactly when its late shell blocks cancel in norm. This is
the analytic premise that a substrate-derived oscillatory phase must prove.
-/
theorem hasExactComplexityCutoffLimit_iff_tailCancellation
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
    HasExactComplexityCutoffLimit phase ↔ ExactShellTailCancellation phase := by
  constructor
  · rintro ⟨L, hL⟩
    have hC := Metric.cauchySeq_iff.mp hL.cauchySeq
    intro ε hε
    obtain ⟨N, hN⟩ := hC ε hε
    refine ⟨N, fun m n hm hmn => ?_⟩
    have hn : N ≤ n := le_trans hm hmn
    have hd := hN m hm n hn
    rw [dist_eq_norm] at hd
    rw [← exactComplexityCutoff_sub phase hmn, norm_sub_rev]
    exact hd
  · intro htail
    have hC : CauchySeq (exactComplexityCutoff phase) := by
      rw [Metric.cauchySeq_iff]
      intro ε hε
      obtain ⟨N, hN⟩ := htail ε hε
      refine ⟨N, fun m hm n hn => ?_⟩
      rcases le_total m n with hmn | hnm
      · rw [dist_eq_norm, norm_sub_rev, exactComplexityCutoff_sub phase hmn]
        exact hN m n hm hmn
      · rw [dist_eq_norm, exactComplexityCutoff_sub phase hnm]
        exact hN n m hn hnm
    exact cauchySeq_tendsto_of_complete hC
THEOREM not_hasExactComplexityCutoffLimit_zeroPhase · zeroPhase_not_exactShellTailCancellation · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean
not_hasExactComplexityCutoffLimit_zeroPhase · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:301 
/-- Zero phase has no unregulated exact-shell complexity-cutoff limit. -/
theorem not_hasExactComplexityCutoffLimit_zeroPhase :
    ¬ HasExactComplexityCutoffLimit zeroPhase := by
  rw [hasExactComplexityCutoffLimit_iff_tailCancellation]
  exact zeroPhase_not_exactShellTailCancellation
zeroPhase_not_exactShellTailCancellation · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:250 
/-- **NON-VACUITY WITNESS.** Zero phase fails the ordered-tail cancellation
criterion. A one-shell late block already has norm greater than one, because
the positive shell masses grow at least as `n^(3n)`. -/
theorem zeroPhase_not_exactShellTailCancellation :
    ¬ ExactShellTailCancellation zeroPhase := by
  intro htail
  obtain ⟨N, hN⟩ := htail 1 one_pos
  let k : ℕ := max 2 N
  have hNk : N ≤ k := le_max_right 2 N
  have hsingle :
      ∑ j ∈ Finset.Ico (k + 1) ((k + 1) + 1),
          exactShellAmplitude zeroPhase j =
        exactShellAmplitude zeroPhase (k + 1) := by
    rw [Finset.sum_Ico_eq_sub (exactShellAmplitude zeroPhase)
      (Nat.le_succ (k + 1)), Finset.sum_range_succ, add_sub_cancel_left]
  have hsmall := hN k (k + 1) hNk (Nat.le_succ k)
  rw [hsingle, exactShellAmplitude_zeroPhase, Complex.norm_real,
    Real.norm_eq_abs, abs_of_pos (shellMass_pos (k + 1))] at hsmall
  have hk2 : 2 ≤ k := le_max_left 2 N
  have hpowN : k + 1 ≤ (k + 1) ^ (3 * (k + 1)) :=
    Nat.le_self_pow (by omega) (k + 1)
  have hpowR :
      ((k + 1 : ℕ) : ℝ) ≤ ((k + 1 : ℕ) : ℝ) ^ (3 * (k + 1)) := by
    calc
      ((k + 1 : ℕ) : ℝ)
          ≤ (((k + 1) ^ (3 * (k + 1)) : ℕ) : ℝ) := by
            exact_mod_cast hpowN
      _ = ((k + 1 : ℕ) : ℝ) ^ (3 * (k + 1)) := Nat.cast_pow _ _
  have hkR : (1 : ℝ) < (k + 1 : ℕ) := by
    exact_mod_cast (show 1 < k + 1 by omega)
  have hmass : (1 : ℝ) < shellMass (k + 1) := by
    have hlower := RegulatorRemovalNoGo.shellMass_lower (k + 1)
    linarith
  linarith
THEOREM exactComplexityCutoff_sub · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean
exactComplexityCutoff_sub · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:165 
/-- The difference between two exact-shell cutoffs is exactly the intervening
ordered shell block. -/
theorem exactComplexityCutoff_sub
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) {m n : ℕ} (hmn : m ≤ n) :
    exactComplexityCutoff phase n - exactComplexityCutoff phase m =
      ∑ k ∈ Finset.Ico (m + 1) (n + 1), exactShellAmplitude phase k := by
  exact (Finset.sum_Ico_eq_sub (exactShellAmplitude phase)
    (Nat.succ_le_succ hmn)).symm

What this page does not claim

This theorem does not claim that any particular phase model describes gravity. It does not claim that the limit, when it exists, corresponds to a continuum geometry. It does not claim that the convergence rate is known or that the limit is computable in practice.

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/ZqContinuumBlocker.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