RelativeNullLayer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The relative null-layer obstruction at every integer level

This is the version of Proposition 5.1 of paper 082-03 needed for a relative frame. It uses connected support, cap accessibility and finite spherical socle saturation. It does not require the frame to be adjacent to every operated color, or the isolated level to be positive.

theorem OAI.HarmonicArtin.ParabolicIntersections.relative_null_layer line 36

Source documentation

Relative null-layer obstruction, with no restriction on the sign of q. All the inputs concern concrete layer counts and spherical caps.

theorem relative_null_layer (I J : Set S) (hI : I.Nonempty)
    (hJI : J ⊆ I) (hJ : IsSpherical M J)
    (z₀ : List ((S ⊕ Unit) × Bool)) (s : S ⊕ Unit)
    (hs : s ∉ Sum.inl '' I) (hw : ∀ a ∈ z₀, a.1 ≠ s) (q : ℤ)
    (c : S ⊕ Unit → ℝ) (hc : ∀ v, 0 ≤ c v)
    (hcSupp : ∀ v, v ∉ Sum.inl '' I → c v = 0)
    (hcPos : ∀ v, v ∈ Sum.inl '' I → 0 < c v)
    (hcNull : ∀ v, v ∈ Sum.inl '' I → (C *ᵥ c) v = 0)
    (hE : ∀ L, ClassCapOn Q (O z₀ s L)
      (closedNeighborhood Q (fusionColorRegion m (Sum.inl '' I)) \
        fusionColorRegion m (Sum.inl '' J)) q)
    (hdata : ∀ v, (v ∈ Sum.inl '' I ∧ v ∉ Sum.inl '' J) ∨
…

Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.fusionColorRegion