Strong supports

In this file, we define strong supports.

Main declarations

• ConNF.Support.Strong: The property that a support is strong.

structure ConNF.BaseSupport.Closed [Params] (S : BaseSupport) : Prop

• interference_subset {N₁ N₂ : NearLitter} : N₁ ∈ Sᴺ → N₂ ∈ Sᴺ → ∀ a ∈ interference N₁ N₂, a ∈ Sᴬ

structure ConNF.Support.PreStrong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : Prop

• support_le {A : β ↝ ⊥} {N : NearLitter} (h : N ∈ (S ⇘. A)ᴺ) (P : InflexiblePath β) (t : Tangle P.δ) (hA : A = P.A ↘ ⋯ ↘.) (ht : Nᴸ = fuzz ⋯ t) : t.support ≤ S ⇘ (P.A ↘ ⋯)

structure ConNF.Support.Closed [Params] {β : TypeIndex} (S : Support β) : Prop

• closed (A : β ↝ ⊥) : (S ⇘. A).Closed

structure ConNF.Support.Strong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) extends S.PreStrong, S.Closed : Prop

• support_le {A : β ↝ ⊥} {N : NearLitter} (h : N ∈ (S ⇘. A)ᴺ) (P : InflexiblePath β) (t : Tangle P.δ) (hA : A = P.A ↘ ⋯ ↘.) (ht : Nᴸ = fuzz ⋯ t) : t.support ≤ S ⇘ (P.A ↘ ⋯)
• closed (A : β ↝ ⊥) : (S ⇘. A).Closed

theorem ConNF.Support.PreStrong.smul [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {S : Support β} (hS : S.PreStrong) (ρ : AllPerm β) : (ρᵁ • S).PreStrong

theorem ConNF.Support.Closed.smul [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {S : Support β} (hS : S.Closed) (ρ : AllPerm β) : (ρᵁ • S).Closed

theorem ConNF.Support.Strong.smul [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {S : Support β} (hS : S.Strong) (ρ : AllPerm β) : (ρᵁ • S).Strong

theorem ConNF.Support.PreStrong.add [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {S T : Support β} (hS : S.PreStrong) (hT : T.PreStrong) : (S + T).PreStrong

theorem ConNF.Support.Closed.scoderiv [Params] {β γ : TypeIndex} {S : Support γ} (hS : S.Closed) (hγ : γ < β) : (S ↗ hγ).Closed

def ConNF.Support.Constrains [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] : Rel (β ↝ ⊥ × NearLitter) (β ↝ ⊥ × NearLitter)

Equations

• ConNF.Support.Constrains x y = ∃ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (B : P.δ ↝ ⊥), x.1 = P.A ↘ ⋯ ⇘ B ∧ x.2 ∈ (t.support ⇘. B)ᴺ ∧ y.1 = P.A ↘ ⋯ ↘. ∧ y.2ᴸ = ConNF.fuzz ⋯ t

theorem ConNF.Support.constrains_subrelation [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] : Subrelation Constrains (InvImage (fun (x1 x2 : NearLitter) => pos x1 < pos x2) Prod.snd)

theorem ConNF.Support.constrains_wf [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] : WellFounded Constrains

theorem ConNF.Support.not_constrains_of_flexible [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {x : β ↝ ⊥ × NearLitter} {A : β ↝ ⊥} {N : NearLitter} (h : ¬Inflexible A Nᴸ) : ¬Constrains x (A, N)

theorem ConNF.Support.constrains_iff_of_inflexible [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] {x : β ↝ ⊥ × NearLitter} {A : β ↝ ⊥} {N : NearLitter} (P : InflexiblePath β) (t : Tangle P.δ) (hA : A = P.A ↘ ⋯ ↘.) (ht : Nᴸ = fuzz ⋯ t) : Constrains x (A, N) ↔ x ∈ (t.support ⇗ (P.A ↘ ⋯))ᴺ

theorem ConNF.Support.constrains_small [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (y : β ↝ ⊥ × NearLitter) : Small {x : β ↝ ⊥ × NearLitter | Constrains x y}

theorem ConNF.Support.reflTransGen_constrains_small [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (s : Set (β ↝ ⊥ × NearLitter)) (hs : Small s) : Small {x : β ↝ ⊥ × NearLitter | ∃ y ∈ s, Relation.ReflTransGen Constrains x y}

def ConNF.Support.constrainsNearLitters [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : Support β

A support that contains all of the near-litters that transitively constrain something in S.

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.Support.mem_constrainsNearLitters_nearLitters [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) (A : β ↝ ⊥) (N : NearLitter) : N ∈ (S.constrainsNearLitters ⇘. A)ᴺ ↔ ∃ (B : β ↝ ⊥), ∃ N' ∈ (S ⇘. B)ᴺ, Relation.ReflTransGen Constrains (A, N) (B, N')

theorem ConNF.Support.constrainsNearLitters_atoms [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (S.constrainsNearLitters ⇘. A)ᴬ = Enumeration.empty

def ConNF.Support.ConstrainsAtom [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) (a : β ↝ ⊥ × Atom) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.Support.constrainsAtoms_small [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : Small {a : β ↝ ⊥ × Atom | S.ConstrainsAtom a}

def ConNF.Support.constrainsAtoms [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : Support β

A support that contains all the atoms that constrain something in S.

Equations

• S.constrainsAtoms = { atoms := ConNF.Enumeration.ofSet {a : β ↝ ⊥ × ConNF.Atom | S.ConstrainsAtom a} ⋯, nearLitters := ConNF.Enumeration.empty }

theorem ConNF.Support.mem_constrainsAtoms_atoms [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) (A : β ↝ ⊥) (a : Atom) : a ∈ (S.constrainsAtoms ⇘. A)ᴬ ↔ S.ConstrainsAtom (A, a)

theorem ConNF.Support.constrainsAtoms_nearLitters [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (S.constrainsAtoms ⇘. A)ᴺ = Enumeration.empty

def ConNF.Support.preStrong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : Support β

Equations

• S.preStrong = S + S.constrainsNearLitters + (S + S.constrainsNearLitters).constrainsAtoms

theorem ConNF.Support.subsupport_preStrong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : S.Subsupport S.preStrong

theorem ConNF.Support.preStrong_atoms [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (S.preStrong ⇘. A)ᴬ = (S ⇘. A)ᴬ + ((S + S.constrainsNearLitters).constrainsAtoms ⇘. A)ᴬ

theorem ConNF.Support.preStrong_nearLitters [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (S.preStrong ⇘. A)ᴺ = (S ⇘. A)ᴺ + (S.constrainsNearLitters ⇘. A)ᴺ

theorem ConNF.Support.preStrong_preStrong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : S.preStrong.PreStrong

theorem ConNF.Support.interference_small [Params] {β : TypeIndex} (S : Support β) : Small {a : β ↝ ⊥ × Atom | ∃ (N₁ : NearLitter) (N₂ : NearLitter), N₁ ∈ (S ⇘. a.1)ᴺ ∧ N₂ ∈ (S ⇘. a.1)ᴺ ∧ a.2 ∈ interference N₁ N₂}

def ConNF.Support.interferenceSupport [Params] {β : TypeIndex} (S : Support β) : Support β

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.Support.mem_interferenceSupport_atoms [Params] {β : TypeIndex} (S : Support β) (A : β ↝ ⊥) (a : Atom) : a ∈ (S.interferenceSupport ⇘. A)ᴬ ↔ ∃ N₁ ∈ (S ⇘. A)ᴺ, ∃ N₂ ∈ (S ⇘. A)ᴺ, a ∈ interference N₁ N₂

theorem ConNF.Support.interferenceSupport_nearLitters [Params] {β : TypeIndex} (S : Support β) (A : β ↝ ⊥) : (S.interferenceSupport ⇘. A)ᴺ = Enumeration.empty

def ConNF.Support.close [Params] {β : TypeIndex} (S : Support β) : Support β

Equations

• S.close = S + S.interferenceSupport

theorem ConNF.Support.subsupport_close [Params] {β : TypeIndex} (S : Support β) : S.Subsupport S.close

theorem ConNF.Support.close_atoms [Params] {β : TypeIndex} (S : Support β) (A : β ↝ ⊥) : (S.close ⇘. A)ᴬ = (S ⇘. A)ᴬ + (S.interferenceSupport ⇘. A)ᴬ

theorem ConNF.Support.close_nearLitters [Params] {β : TypeIndex} (S : Support β) (A : β ↝ ⊥) : (S.close ⇘. A)ᴺ = (S ⇘. A)ᴺ

theorem ConNF.Support.close_closed [Params] {β : TypeIndex} (S : Support β) : S.close.Closed

def ConNF.Support.strong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : Support β

Equations

• S.strong = S.preStrong.close

theorem ConNF.Support.preStrong_subsupport_strong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : S.preStrong.Subsupport S.strong

theorem ConNF.Support.subsupport_strong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : S.Subsupport S.strong

theorem ConNF.Support.strong_strong [Params] {β : TypeIndex} [Level] [CoherentData] [LeLevel β] (S : Support β) : S.strong.Strong