BoundaryWitness.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

A boundary witness below a capped isolated layer

The relative frame need not be adjacent to the isolated set. Connected support finds an occupied exterior boundary color. A zero boundary cap then puts that occupation strictly below the isolated layer. This is the additional boundary argument of §5 of paper 082-03.

theorem OAI.HarmonicArtin.ParabolicIntersections.orbit_frame_generator line 34

Source documentation

The unchanged initial frame occurs in every minimal representative, with its original label and level.

theorem orbit_frame_generator (w : List (V × Bool)) (s : V)
    (hw : ∀ a ∈ w, a.1 ≠ s) (L : FusionLabel m) :
    ∃ j : (fusionOrbitModel m d hd hdiag w s L).Index,
      ((fusionOrbitModel m d hd hdiag w s L).complex.placement j).color = (s, L) ∧
      ((fusionOrbitModel m d hd hdiag w s L).complex.placement j).level = 0 := by
…

Mentions: OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.fusionOrbitModel

theorem OAI.HarmonicArtin.ParabolicIntersections.orbit_generator_of_positive line 53

Source documentation

A positive folded count is witnessed by an actual generator in one member of the family, at the specified color and level.

theorem orbit_generator_of_positive (w : List (V × Bool)) (s v : V) (q : ℤ)
    (hp : 0 < μ w s q v) :
    ∃ L : FusionLabel m, ∃ i : (fusionOrbitModel m d hd hdiag w s L).Index,
      ((fusionOrbitModel m d hd hdiag w s L).complex.placement i).color.1 = v ∧
      ((fusionOrbitModel m d hd hdiag w s L).complex.placement i).level = q := by
…

Mentions: OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.fusionOrbitModel

theorem OAI.HarmonicArtin.ParabolicIntersections.orbit_boundary_below line 83

Source documentation

An occupied generator in U and an unoperated frame outside U force an occupied boundary below q, if every boundary count at q and above is zero. No condition 0 < q is used.

theorem orbit_boundary_below (w : List (V × Bool)) (s : V)
    (hw : ∀ a ∈ w, a.1 ≠ s) (U : Set V) (hs : s ∉ U) (q : ℤ)
    (L : FusionLabel m) (i : (fusionOrbitModel m d hd hdiag w s L).Index)
    (hi : ((fusionOrbitModel m d hd hdiag w s L).complex.placement i).color.1 ∈ U)
    (hcap : ∀ H, ClassCapOn Q (O w s H)
      (colorBoundary Q (fusionColorRegion m U)) q)
    (hzero : ∀ v, v ∉ U → (∃ u ∈ U, C v u < 0) → μ w s q v = 0) :
    ∃ k v, k < q ∧ v ∉ U ∧ (∃ u ∈ U, C v u < 0) ∧ 0 < μ w s k v := by
…

Mentions: OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.fusionOrbitModel, OAI.HarmonicArtin.fusionColorRegion