Encyclopedia Gravity Gravity Seven Gaps Zq Continuum Blocker

ARTICLE 4 claims 4 theorems

Gravity Seven Gaps Zq Continuum Blocker

A formal module that pinpoints the exact missing step between a finite approximation and a complete theory of gravity.

Verify this page

The cutoff blocker

In Recognition Science, the path to a theory of gravity runs through a sum over discrete path classes, a sum that grows with a complexity cutoff. The ledger, a discrete record of events, supplies these classes. The module called Seven Gaps, P2-a, the phased quotient cutoff blocker, isolates the precise analytic condition under which that sum has a limit as the cutoff is removed.

The current capped API can express a family of phase models and a sequence of finite quotient sums. Completeness of the complex numbers gives an exact criterion: that sequence has a limit if and only if it is Cauchy. The cap-free exact-shell API gives the panel-locked form. Zcap phase B sums the exact quotient shells in range B, and OscillatoryTail phase uniformly quantifies every sufficiently late contiguous shell block. Exact telescoping proves CauchySeq (Zcap phase) ↔ OscillatoryTail phase. This is the cancellation statement that a substrate-derived phase must supply. It is discriminating: the zero phase has an explicit epsilon-one failure witness.

One bridge is still absent from the current API. Zq B uses the capped quotient TriangulationClass B, while the nonduplicating shell decomposition uses ExactPathClass n. CapShellCompatibility names the smallest required cross-API statement: equality of the two finite sums at every cap. Under that bridge, convergence of the existing phased Zq sequence is equivalent to the exact-shell tail-cancellation criterion.

All limits here remove a complexity cutoff. They are not mesh refinement and carry no claim about continuum geometry, observations, a convergence rate, a derived measure, or the full-theory ledger.

THEOREM hasPhasedZqComplexityLimit_iff_cauchy · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean
hasPhasedZqComplexityLimit_iff_cauchy · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:66 
/-- **HEADLINE IFF.** The existing phased quotient sums have a
complexity-cutoff limit exactly when their cross-cap differences are Cauchy.
This theorem assumes no convergence and no physical continuum interpretation.
-/
theorem hasPhasedZqComplexityLimit_iff_cauchy (P : CapPhaseFamily) :
    HasPhasedZqComplexityLimit P ↔ PhasedZqCauchyCriterion P := by
  constructor
  · rintro ⟨L, hL⟩
    have hC := (Metric.cauchySeq_iff.mp hL.cauchySeq)
    intro ε hε
    obtain ⟨N, hN⟩ := hC ε hε
    refine ⟨N, fun m hm n hn => ?_⟩
    simpa only [dist_eq_norm] using hN m hm n hn
  · intro h
    have hC : CauchySeq (phasedZqSequence P) := by
      rw [Metric.cauchySeq_iff]
      exact h
    exact cauchySeq_tendsto_of_complete hC
THEOREM cauchySeq_Zcap_iff_oscillatoryTail · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean
cauchySeq_Zcap_iff_oscillatoryTail · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:117 
/-- **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
THEOREM zeroPhase_epsilon_one_failure · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean
zeroPhase_epsilon_one_failure · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:216 
/-- **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
THEOREM hasPhasedZqLimit_iff_exactShellTail_of_compatibility · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean
hasPhasedZqLimit_iff_exactShellTail_of_compatibility · IndisputableMonolith/Gravity/SevenGaps/ZqContinuumBlocker.lean:328 
/-- **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

This module does not establish that any physical phase model exists, only the criterion it must satisfy. The limits here are not mesh refinement and carry no claim about continuum geometry. The module does not provide a convergence rate or a derived measure.

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