Gravity Seven Gaps Zq Shell Balance Blocker Eventually Zero Phase Not Oscillator

The phase-balance blocker

In the Recognition Science framework's study of gravity, a key question is whether a certain sequence of complex numbers, built from phases attached to path classes, keeps oscillating forever. The machine-checked library of formal theorems proves a precise negative result: if a phase eventually becomes exactly zero, meaning it agrees with the zero phase from some complexity level onward, then it cannot have an oscillatory tail. The theorem is named eventuallyZeroPhase_not_oscillatoryTail, and it is a theorem in the strongest sense: proved in the framework's machine-checked library with no unproved assumptions.

The proof is short and structural. If a phase eventually matches zero, and it did have an oscillatory tail, then by a congruence theorem the zero phase itself would have an oscillatory tail. But the library separately proves that the zero phase has no oscillatory tail, so the assumption collapses. The result is one of three certificates in a module called the shell-balance blocker, which isolates what is missing in a larger proof about gravity: genuine asymptotic balance inside each shell, not just agreement after a cutoff.

What the theorem does not claim is just as important. It does not say that a phase with an oscillatory tail must be eventually zero; the implication runs only one way. It does not say that changing finitely many early shells can help, and in fact a companion theorem proves that any phase supported below a finite bound also fails to have an oscillatory tail. It makes no claim about mesh refinement, geometric continua, or any full theory of gravity; all limits concern the complexity cutoff, and no full-theory flag is changed by any of these results.

/-- **FINITE-CAP NO-GO.** No phase modification supported on only finitely
many exact shells can satisfy the uniform oscillatory-tail condition. -/
theorem eventuallyZeroPhase_not_oscillatoryTail
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
    (hzero : EventuallyZeroPhase phase) :
    ¬ OscillatoryTail phase := by
  intro htail
  have hz : OscillatoryTail zeroPhase :=
    (oscillatoryTail_congr_eventually hzero).mp htail
  exact zeroPhase_not_oscillatoryTail hz

/-- **COMPLEXITY-PHASE NO-GO.** Any phase that only sees shell complexity
fails `OscillatoryTail`, regardless of how its common shell phase varies. -/
theorem shellConstant_not_oscillatoryTail
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ)
    (hconst : ShellConstant phase) :
    ¬ OscillatoryTail phase := by
  intro htail
  exact shellConstant_not_shellAmplitudeVanishes phase hconst
    (oscillatoryTail_implies_shellAmplitudeVanishes phase htail)

/-- A fixed-cap cancellation witness cannot be promoted to a uniform tail
theorem merely by extending it by zero phase beyond the witnessed cap. -/
theorem supportedBelow_not_oscillatoryTail
    (phase : ∀ n : ℕ, ExactPathClass n → ℝ) (B : ℕ)
    (hsupp : SupportedBelow phase B) :
    ¬ OscillatoryTail phase :=
  eventuallyZeroPhase_not_oscillatoryTail phase
    ⟨B, fun n hn c => by
      rw [hsupp n hn c]
      rfl⟩

What this page does not claim

The theorem does not claim that an oscillatory tail implies the phase is eventually zero. It does not claim that changing finitely many early shells can help. It makes no geometric-continuum or mesh-refinement claim.

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/ZqShellBalanceBlocker.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: