Gravity Seven Gaps Zq Shell Balance Blocker Oscillatory Tail Of Eventually Agree

The tail property

In the Recognition Science framework's study of gravity, the declaration oscillatoryTail_of_eventuallyAgrees establishes a transfer property for a technical condition called OscillatoryTail. The condition concerns a phase, which here is an assignment of a real number to each exact path class at each complexity level. The property says that the sum of phase contributions over any contiguous block of late complexity levels tends to zero as the block's starting level grows. The theorem states: if two phases agree from some complexity level onward, and one of them has the OscillatoryTail property, then the other has it too. In plainer terms, changing only finitely many early levels cannot destroy or create the long-range oscillatory behavior.

The declaration is a formal theorem in the machine-checked library of formal theorems, proved without any unverified assumptions. Its proof rests on a congruence lemma showing that the shell amplitude at a single level depends only on the phase values at that level. Because the tail property only concerns levels beyond some cutoff, agreement from that cutoff onward suffices to transfer the property. The theorem is stated for arbitrary phases, not just those arising from a particular construction.

What the theorem does not claim is just as important. It does not say that any phase has the OscillatoryTail property; it only transfers the property between two phases that eventually agree. It does not assert that the tail property holds for the specific phases arising in the gravity construction; that remains an open target. Nor does it say anything about phases that differ at infinitely many levels, or about the behavior of individual levels before the agreement cutoff. The theorem is a structural implication, not an existence result.

The practical consequence is a sharp boundary on what finite modifications can achieve. If a proposed phase fails to have the tail property, no adjustment confined to finitely many early levels can fix it. The framework's library also proves that phases which vanish eventually, or which are constant within each shell, cannot have the tail property. These results together isolate the minimal missing ingredient for the gravity construction: genuine asymptotic balance within every late shell, not just a finite-pairing certificate.

/-- One direction of tail transport along eventual phase agreement. -/
theorem oscillatoryTail_of_eventuallyAgrees
    {phase ψ : ∀ n : ℕ, ExactPathClass n → ℝ}
    (hagree : EventuallyAgrees phase ψ)
    (hphase : OscillatoryTail phase) : OscillatoryTail ψ := by
  obtain ⟨N₀, hN₀⟩ := hagree
  intro ε hε
  obtain ⟨N, hN⟩ := hphase ε hε
  refine ⟨max N N₀, fun m n hm hmn => ?_⟩
  have hmN : N ≤ m := le_trans (le_max_left N N₀) hm
  have hmN₀ : N₀ ≤ m := le_trans (le_max_right N N₀) hm
  have heq :
      ∑ k ∈ Finset.Ico m n, exactShellAmplitude ψ k =
        ∑ k ∈ Finset.Ico m n, exactShellAmplitude phase k := by
    refine Finset.sum_congr rfl fun k hk => ?_
    have hmk : m ≤ k := (Finset.mem_Ico.mp hk).1
    exact (exactShellAmplitude_congr
      (fun c => (hN₀ k (le_trans hmN₀ hmk) c).symm))
  rw [heq]
  exact hN m n hmN hmn

/-- Exact shell amplitudes agree when all class phases agree on that shell. -/
theorem exactShellAmplitude_congr
    {phase ψ : ∀ n : ℕ, ExactPathClass n → ℝ} {n : ℕ}
    (h : ∀ c, phase n c = ψ n c) :
    exactShellAmplitude phase n = exactShellAmplitude ψ n := by
  unfold exactShellAmplitude
  refine Finset.sum_congr rfl fun c _ => ?_
  rw [h c]

/-- One direction of tail transport along eventual phase agreement. -/
theorem oscillatoryTail_of_eventuallyAgrees
    {phase ψ : ∀ n : ℕ, ExactPathClass n → ℝ}
    (hagree : EventuallyAgrees phase ψ)
    (hphase : OscillatoryTail phase) : OscillatoryTail ψ := by
  obtain ⟨N₀, hN₀⟩ := hagree
  intro ε hε
  obtain ⟨N, hN⟩ := hphase ε hε
  refine ⟨max N N₀, fun m n hm hmn => ?_⟩
  have hmN : N ≤ m := le_trans (le_max_left N N₀) hm
  have hmN₀ : N₀ ≤ m := le_trans (le_max_right N N₀) hm
  have heq :
      ∑ k ∈ Finset.Ico m n, exactShellAmplitude ψ k =
        ∑ k ∈ Finset.Ico m n, exactShellAmplitude phase k := by
    refine Finset.sum_congr rfl fun k hk => ?_
    have hmk : m ≤ k := (Finset.mem_Ico.mp hk).1
    exact (exactShellAmplitude_congr
      (fun c => (hN₀ k (le_trans hmN₀ hmk) c).symm))
  rw [heq]
  exact hN m n hmN hmn

What this page does not claim

The theorem does not assert that any particular phase has the OscillatoryTail property. The theorem does not say anything about phases that differ at infinitely many levels. The theorem does not claim that finite modifications can ever create the tail property where it was absent.

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: