SphericalGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The gap contradiction in Proposition 7.4 of paper 082-03.

lemma OAI.HarmonicArtin.ParabolicIntersections.no_cochain_gap line 17
Source documentation
A missing cochain placement separates every generator below it from all generators above it. The actual endomorphism dimension rules out such a separation for a transported indecomposable projective.
```
lemma no_cochain_gap (E : BasedComplex Q (K := ℂ) I) (hE : E.IsMinimal Q)
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.tests_exact_of_empty_gap line 35
Source documentation
Once the cochain tests have moved below the fixed exterior and the path bound forces a gap, all tests vanish. This is the contradiction used in the bounded-positive-height argument.
```
theorem tests_exact_of_empty_gap (U : Set V) (E : BasedComplex Q (K := ℂ) I)
…
```
theorem OAI.HarmonicArtin.ParabolicIntersections.cochain_lower_obstruction_of_mesh line 53
Source documentation
The quantitative form of Proposition 7.4: with fixed generator-level bounds and a fixed exterior lower placement, nonzero tests cannot all move arbitrarily far down in cochain degree.
```
theorem cochain_lower_obstruction_of_mesh (U : Set V) (hmesh : MeshNilpotent Q U) :
    ∃ N : ℕ, 0 < N ∧ ∀ (I : Type) [Fintype I] (E : BasedComplex Q (K := ℂ) I),
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.MeshNilpotent