Vanishing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DiamondDistortion.Midpoint.Heads.TailVanishing line 19
Source documentation
Uniform pure-tail vanishing at the unit sphere, the qualitative mass-removal input. No power law or quantitative modulus is inserted into this hypothesis.
```
def Heads.TailVanishing (A : Heads ι X) : Prop :=
…
```
Mentions: OAI.DiamondDistortion.Midpoint.Heads
lemma OAI.DiamondDistortion.Midpoint.Heads.vanishing_gap line 24
theorem OAI.DiamondDistortion.Midpoint.Heads.vanishing_lens line 73
Source documentation
Pure-tail vanishing transfers uniformly to separated lenses at arbitrary centers. This retains the qualitative route independently of a square input.
```
theorem Heads.vanishing_lens (A : Heads ι X) (hinput : A.TailVanishing) {ε : ℝ}
    (hε : 0 < ε) : ∃ ρ : ℝ,0 ≤ ρ ∧ ρ < 1 ∧ Diamond.UnitLensBound X ε ρ := by
…
```
Mentions: OAI.DiamondDistortion.Midpoint.Heads, OAI.DiamondDistortion.Diamond.UnitLensBound

theorem OAI.DiamondDistortion.Midpoint.Heads.vanishing_weak line 82

Source documentation

The separately stated weak-null uniformity: the same rho works for every center and sequence with the specified positive lower norm bound.

theorem Heads.vanishing_weak (A : Heads ι X) (hinput : A.TailVanishing) {ε : ℝ}
    (hε : 0 < ε) : ∃ ρ : ℝ,0 ≤ ρ ∧ ρ < 1 ∧
    ∀ (x : X) (z : ℕ → X),WeaklyNull z → (∀ i,ε ≤ ‖z i‖) →
      (∀ i,‖x+z i‖ ≤ 1) → (∀ i,‖x-z i‖ ≤ 1) → ‖x‖ ≤ ρ := by
…

Mentions: OAI.DiamondDistortion.Midpoint.Heads, OAI.DiamondDistortion.Midpoint.WeaklyNull

theorem OAI.DiamondDistortion.Midpoint.Heads.vanishing_obstruction line 92
Source documentation
Bottom-up mass removal, qualitative diamond obstruction.
```
theorem Heads.vanishing_obstruction (A : Heads ι X) (hinput : A.TailVanishing) :
    ¬ Diamond.UniformEmbeddings X := by
…
```
Mentions: OAI.DiamondDistortion.Midpoint.Heads, OAI.DiamondDistortion.Diamond.UniformEmbeddings