Gravity Seven Gaps Zq Continuum Blocker Cauchy Seq Zcap Iff Oscillatory Tail

The tail cancellation test

In quantum gravity, physicists often write a physical quantity as an infinite sum of contributions, one for each possible geometric configuration. The sum only makes sense if the partial sums, taken to larger and larger complexity, eventually converge to a finite number. A ledger, a discrete record of events, needs such a finite total to be meaningful.

The Recognition Science library proves a precise test for this convergence. The theorem cauchySeq_Zcap_iff_oscillatoryTail states that a sequence of partial sums is Cauchy, meaning it converges, if and only if the tail of the sum, the contributions from all sufficiently late terms, collectively shrink to zero. This is not a vague hope; it is a formal equivalence, checked line by line by a machine.

The test is discriminating. The library also proves that for the simplest choice, the zero phase where every contribution is just a positive mass, the tail does not shrink. There is an explicit witness: for any cutoff point, one can find a later block of terms whose sum has magnitude greater than 1. This means the zero phase fails the convergence test, and the corresponding infinite sum does not have a finite limit.

This matters because it shows the framework's own default model of gravity, without any oscillatory phases, cannot produce a finite total. The theorem does not say which phase is correct, only that the zero phase is ruled out. It also does not claim anything about the physical geometry of space, the rate of convergence, or any observable prediction. It is a precise statement about a formal sum, and its power is in what it eliminates.

In Recognition Science, this is one step in a larger program: the framework models gravity as a sum over recognition events, where each event is a discrete act of the ledger recording a configuration. The convergence test is a necessary condition for the sum to be a well-defined physical quantity. The theorem provides the exact criterion, and the failure of the zero phase is a concrete, checkable result that guides the search for the correct phase.

/-- **C1 HEADLINE.** The exact-shell cutoff sequence is Cauchy if and only if
every sufficiently late contiguous shell block is uniformly small. This is a
pure complexity-cutoff criterion and assumes no desired convergence. -/
theorem cauchySeq_Zcap_iff_oscillatoryTail
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
    CauchySeq (Zcap phase) ↔ OscillatoryTail phase := by
  constructor
  · intro hC
    have hMetric := Metric.cauchySeq_iff.mp hC
    intro ε hε
    obtain ⟨N, hN⟩ := hMetric ε 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 [← Zcap_telescoping phase hmn, norm_sub_rev]
    exact hd
  · intro htail
    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, Zcap_telescoping phase hmn]
      exact hN m n hm hmn
    · rw [dist_eq_norm, Zcap_telescoping phase hnm]
      exact hN n m hn hnm

/-- **C1 EPSILON-ONE WITNESS.** Beyond every proposed tail threshold there
is a contiguous one-shell block whose zero-phase norm is greater than one.
The bridge is direct: `shellMass_lower` concerns the same cap-free exact
quotient `ExactPathClass` and the same `classMu` used by
`exactShellAmplitude`; it is neither a pre-quotient nor a cap-dependent mass.
-/
theorem zeroPhase_epsilon_one_failure (N : ℕ) :
    ∃ m n : ℕ, N ≤ m ∧ m ≤ n ∧
      1 < ‖∑ k ∈ Finset.Ico m n, exactShellAmplitude zeroPhase k‖ := by
  let k : ℕ := max 2 N
  have hNk : N ≤ k := le_max_right 2 N
  have hsingle :
      ∑ j ∈ Finset.Ico k (k + 1), exactShellAmplitude zeroPhase j =
        exactShellAmplitude zeroPhase k := by
    rw [Finset.sum_Ico_eq_sub (exactShellAmplitude zeroPhase)
      (Nat.le_succ k), Finset.sum_range_succ, add_sub_cancel_left]
  have hk2 : 2 ≤ k := le_max_left 2 N
  have hpowN : k ≤ k ^ (3 * k) :=
    Nat.le_self_pow (by omega) k
  have hpowR : ((k : ℕ) : ℝ) ≤ ((k : ℕ) : ℝ) ^ (3 * k) := by
    calc
      ((k : ℕ) : ℝ) ≤ ((k ^ (3 * k) : ℕ) : ℝ) := by
        exact_mod_cast hpowN
      _ = ((k : ℕ) : ℝ) ^ (3 * k) := Nat.cast_pow _ _
  have hkR : (1 : ℝ) < (k : ℕ) := by
    exact_mod_cast (show 1 < k by omega)
  have hmass : (1 : ℝ) < shellMass k := by
    have hlower := RegulatorRemovalNoGo.shellMass_lower k
    linarith
  refine ⟨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)]
  exact hmass

/-- The panel-locked `OscillatoryTail` criterion fails at zero phase, with
the explicit epsilon-one witness above. -/
theorem zeroPhase_not_oscillatoryTail :
    ¬ OscillatoryTail zeroPhase := by
  intro htail
  obtain ⟨N, hN⟩ := htail 1 one_pos
  obtain ⟨m, n, hm, hmn, hlarge⟩ := zeroPhase_epsilon_one_failure N
  have hsmall := hN m n hm hmn
  linarith

/-- Consequently the exact zero-phase `Zcap` sequence is not Cauchy. -/
theorem zeroPhase_Zcap_not_cauchy :
    ¬ CauchySeq (Zcap zeroPhase) := by
  rw [cauchySeq_Zcap_iff_oscillatoryTail]
  exact zeroPhase_not_oscillatoryTail

What this page does not claim

The theorem does not identify which specific phase is physically correct. The theorem makes no claim about the geometry of space, observations, or any convergence rate. The failure of the zero phase does not imply the framework's full theory is inconsistent.

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: