Gravity Seven Gaps Zq Continuum Blocker Has Phased Zq Limit Iff Exact Shell Tail

The compatibility bridge

In the Recognition Science framework's machine-checked library of formal theorems, a central question is whether an infinite sum over path classes has a well-defined limit. The sum is built from a sequence of finite approximations, each summing contributions up to a complexity cap B. The framework shows that this sequence has a limit exactly when it satisfies the Cauchy criterion, meaning the terms eventually get arbitrarily close to each other. This is a standard completeness fact about complex numbers, applied here to a specific family of sums.

The framework's library also works with a different, cap-free description of the same physical idea. Instead of summing up to a cap, it sums exact shells, each shell containing all path classes of a given complexity n. The key theorem here is that this exact-shell sequence is Cauchy exactly when the late shells cancel: for any tolerance, there is a point beyond which every contiguous block of shells sums to less than that tolerance. This property is called tail cancellation, a plain-words condition that late contributions wash out.

The declaration hasPhasedZqLimit_iff_exactShellTail_of_compatibility connects the two descriptions. It states that if the capped sum and the exact-shell sum agree at every finite cap, a condition named CapShellCompatibility, then the capped sequence has a limit exactly when the exact-shell sequence satisfies tail cancellation. In plain language: under that agreement, the two routes to removing the complexity cutoff stand or fall together. The argument is short: the compatibility condition makes the two sequences identical term by term, so the limit question for one is the limit question for the other.

The framework also shows this bridge is discriminating. The zero phase, where every path class gets the same weight, fails both routes: it has no exact-shell limit and no capped-sequence limit. The argument exhibits an explicit failure witness for epsilon equal to one, meaning the late shells do not shrink below that tolerance no matter how far out one looks. This is not a vague instability but a concrete, checked counterexample.

What the declaration does not claim is equally important. It says nothing about mesh refinement, continuum geometry, or observations. All limits here remove a complexity cutoff, not a discretization scale. The bridge also does not establish that any physically relevant phase satisfies tail cancellation; it only establishes the equivalence under the compatibility hypothesis. The zero phase is a demonstrated failure, but whether a substrate-derived phase succeeds remains open in the current API.

/-- **BLOCKER CERTIFICATE.** Once the missing cap-to-shell compatibility is
supplied, convergence of the existing phased `Zq B` sequence is exactly the
ordered-tail cancellation obligation on exact shells. No desired convergence
is assumed. -/
theorem hasPhasedZqLimit_iff_exactShellTail_of_compatibility
    (P : CapPhaseFamily) (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
    (hcompat : CapShellCompatibility P phase) :
    HasPhasedZqComplexityLimit P ↔ ExactShellTailCancellation phase := by
  have hseq : phasedZqSequence P = exactComplexityCutoff phase :=
    funext hcompat.sum_eq
  unfold HasPhasedZqComplexityLimit
  rw [hseq]
  exact hasExactComplexityCutoffLimit_iff_tailCancellation phase

/-- Zero phase fails both available removal routes: the unregulated
complexity cutoff and the positive Gaussian regulator-removal limit. Neither
statement is a mesh-refinement or physical-continuum claim. -/
theorem zeroPhase_fails_both_removal_routes :
    (¬ HasExactComplexityCutoffLimit zeroPhase) ∧
      (¬ HasZRSRegulatorRemoval zeroPhase) :=
  ⟨not_hasExactComplexityCutoffLimit_zeroPhase,
    RegulatorRemovalNoGo.not_hasZRSRegulatorRemoval_zeroPhase⟩

/-- **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

/-- **BLOCKER CERTIFICATE.** Once the missing cap-to-shell compatibility is
supplied, convergence of the existing phased `Zq B` sequence is exactly the
ordered-tail cancellation obligation on exact shells. No desired convergence
is assumed. -/
theorem hasPhasedZqLimit_iff_exactShellTail_of_compatibility
    (P : CapPhaseFamily) (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
    (hcompat : CapShellCompatibility P phase) :
    HasPhasedZqComplexityLimit P ↔ ExactShellTailCancellation phase := by
  have hseq : phasedZqSequence P = exactComplexityCutoff phase :=
    funext hcompat.sum_eq
  unfold HasPhasedZqComplexityLimit
  rw [hseq]
  exact hasExactComplexityCutoffLimit_iff_tailCancellation phase

What this page does not claim

The declaration does not prove that any physically relevant phase satisfies tail cancellation. It does not establish anything about mesh refinement, continuum geometry, or observations. It does not claim that the zero phase is the only phase that fails.

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: