Gravity Seven Gaps Zq Shell Balance Blocker Supported Below Not Oscillatory Tail

The finite-support dead end

In the Recognition Science framework's work on the seven gaps problem, a phase is a real number attached to each exact path class at each complexity level n. Think of it as a bookkeeping entry that records how a path's contribution is rotated in the complex plane. The framework's library is a machine-checked collection of formal theorems, and one of its results concerns phases that are supported below a bound B: such a phase is exactly zero for every complexity level n at or above B. The theorem supportedBelow_not_oscillatoryTail proves that any phase supported below a finite bound cannot have an oscillatory tail.

An oscillatory tail is a stronger condition than merely having amplitudes that shrink. It requires that for any positive tolerance epsilon, there is a cutoff N such that the sum of shell amplitudes over any contiguous block of shells beyond N has norm less than epsilon. The theorem shows that a phase which is identically zero from some point onward fails this condition. The proof is short: a zero phase is eventually zero, and the framework has already established that an eventually zero phase cannot be oscillatory. So the finite-support dead end is real: no phase that switches off completely can satisfy the tail condition.

This result matters because it blocks a tempting shortcut. One might hope to certify the oscillatory tail by pairing up shells with a finite-cap certificate, showing cancellation only up to some fixed complexity. The theorem says that approach cannot work, because any certificate that only changes finitely many shells is equivalent to a phase supported below some bound, and that phase fails the tail condition. The framework's library also proves that a phase constant inside each shell fails, with its shell amplitude norm exactly the diverging shell mass. So the missing ingredient for the phase obligation is genuine asymptotic balance within late shells, not a finite patch job.

What the theorem does not claim is just as important. It does not say that no phase can have an oscillatory tail; it only rules out a specific class of phases. It makes no statement about whether a phase with the required intra-shell balance exists. The result is purely negative: it eliminates a family of candidates, it does not construct a successful one. It also makes no claim about mesh refinement or geometric continuum limits; all limits here concern the complexity cutoff, not any spatial discretization. The theorem is a blocker, not a builder.

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

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

/-- The norm of a shell-constant amplitude is exactly the shell mass. -/
theorem norm_exactShellAmplitude_shellConstant
    {phase : ∀ n : ℕ, ExactPathClass n → ℝ}
    (hconst : ShellConstant phase) (n : ℕ) :
    ‖exactShellAmplitude phase n‖ = shellMass n := by
  rw [exactShellAmplitude_shellConstant hconst n, norm_mul,
    Complex.norm_real, Real.norm_eq_abs, abs_of_pos (shellMass_pos n),
    Complex.norm_exp_I_mul_ofReal, mul_one]

What this page does not claim

No phase with an oscillatory tail exists. The theorem constructs a phase that satisfies the oscillatory tail condition. The result applies to mesh refinement or any geometric continuum limit.

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: