structure ConNF.StructLAction.CoherentDom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (ψ : ConNF.StructLAction ↑β) : Prop

• mapFlexible : ψ.MapFlexible
• atom_bot_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [inst : ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom}, ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz ⋯ a)).Dom → ((ψ (A.cons ⋯)).atomMap a).Dom
• atom_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {a : ConNF.Atom}, { path := B, value := Sum.inl a } ∈ t.support → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).atomMap a).Dom
• nearLitter_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N : ConNF.NearLitter}, { path := B, value := Sum.inr N } ∈ t.support → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).litterMap N.fst).Dom
• symmDiff_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N : ConNF.NearLitter} {a : ConNF.Atom}, { path := B, value := Sum.inr N } ∈ t.support → a ∈ symmDiff (ConNF.litterSet N.fst) ↑N → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).atomMap a).Dom

theorem ConNF.StructLAction.CoherentDom.mapFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ψ : ConNF.StructLAction ↑β} (self : ψ.CoherentDom) : ψ.MapFlexible

theorem ConNF.StructLAction.CoherentDom.atom_bot_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ψ : ConNF.StructLAction ↑β} (self : ψ.CoherentDom) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} : ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz ⋯ a)).Dom → ((ψ (A.cons ⋯)).atomMap a).Dom

theorem ConNF.StructLAction.CoherentDom.atom_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ψ : ConNF.StructLAction ↑β} (self : ψ.CoherentDom) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {a : ConNF.Atom} : { path := B, value := Sum.inl a } ∈ t.support → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).atomMap a).Dom

theorem ConNF.StructLAction.CoherentDom.nearLitter_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ψ : ConNF.StructLAction ↑β} (self : ψ.CoherentDom) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N : ConNF.NearLitter} : { path := B, value := Sum.inr N } ∈ t.support → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).litterMap N.fst).Dom

theorem ConNF.StructLAction.CoherentDom.symmDiff_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ψ : ConNF.StructLAction ↑β} (self : ψ.CoherentDom) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N : ConNF.NearLitter} {a : ConNF.Atom} : { path := B, value := Sum.inr N } ∈ t.support → a ∈ symmDiff (ConNF.litterSet N.fst) ↑N → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).atomMap a).Dom

structure ConNF.StructLAction.Coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (ψ : ConNF.StructLAction ↑β) extends ConNF.StructLAction.CoherentDom : Prop

• mapFlexible : ψ.MapFlexible
• atom_bot_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [inst : ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom}, ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz ⋯ a)).Dom → ((ψ (A.cons ⋯)).atomMap a).Dom
• atom_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {a : ConNF.Atom}, { path := B, value := Sum.inl a } ∈ t.support → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).atomMap a).Dom
• nearLitter_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N : ConNF.NearLitter}, { path := B, value := Sum.inr N } ∈ t.support → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).litterMap N.fst).Dom
• symmDiff_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N : ConNF.NearLitter} {a : ConNF.Atom}, { path := B, value := Sum.inr N } ∈ t.support → a ∈ symmDiff (ConNF.litterSet N.fst) ↑N → ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom → ((ψ ((A.cons hδ).comp B)).atomMap a).Dom
• coherent_coe : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_2 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} (h : ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom) (ρ : ConNF.Allowable ↑γ), (∀ (B : ConNF.ExtendedIndex ↑δ) (a : ConNF.Atom) (ha : { path := B, value := Sum.inl a } ∈ t.support), ((ψ ((A.cons hδ).comp B)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • a) → (∀ (B : ConNF.ExtendedIndex ↑δ) (N : ConNF.NearLitter) (ha : { path := B, value := Sum.inr N } ∈ t.support), ((ψ ((A.cons hδ).comp B)).litterMap N.fst).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • N.fst.toNearLitter) → (∀ (B : ConNF.ExtendedIndex ↑δ) (N : ConNF.NearLitter) (a : ConNF.Atom) (hN : { path := B, value := Sum.inr N } ∈ t.support) (ha : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N), ((ψ ((A.cons hδ).comp B)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • a) → (((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).get h).fst = ConNF.fuzz hδε ((ConNF.Allowable.comp (Quiver.Hom.toPath hδ)) ρ • t)
• coherent_bot : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} (h : ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz ⋯ a)).Dom) (ρ : ConNF.Allowable ↑γ), ((ψ (A.cons ⋯)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • a → (((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz ⋯ a)).get h).fst = ConNF.fuzz ⋯ ((ConNF.Allowable.comp (Quiver.Hom.toPath ⋯)) ρ • a)

theorem ConNF.StructLAction.Coherent.coherent_coe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ψ : ConNF.StructLAction ↑β} (self : ψ.Coherent) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} (h : ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).Dom) (ρ : ConNF.Allowable ↑γ) : (∀ (B : ConNF.ExtendedIndex ↑δ) (a : ConNF.Atom) (ha : { path := B, value := Sum.inl a } ∈ t.support), ((ψ ((A.cons hδ).comp B)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • a) → (∀ (B : ConNF.ExtendedIndex ↑δ) (N : ConNF.NearLitter) (ha : { path := B, value := Sum.inr N } ∈ t.support), ((ψ ((A.cons hδ).comp B)).litterMap N.fst).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • N.fst.toNearLitter) → (∀ (B : ConNF.ExtendedIndex ↑δ) (N : ConNF.NearLitter) (a : ConNF.Atom) (hN : { path := B, value := Sum.inr N } ∈ t.support) (ha : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N), ((ψ ((A.cons hδ).comp B)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • a) → (((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz hδε t)).get h).fst = ConNF.fuzz hδε ((ConNF.Allowable.comp (Quiver.Hom.toPath hδ)) ρ • t)

theorem ConNF.StructLAction.Coherent.coherent_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ψ : ConNF.StructLAction ↑β} (self : ψ.Coherent) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} (h : ((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz ⋯ a)).Dom) (ρ : ConNF.Allowable ↑γ) : ((ψ (A.cons ⋯)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • a → (((ψ ((A.cons hε).cons ⋯)).litterMap (ConNF.fuzz ⋯ a)).get h).fst = ConNF.fuzz ⋯ ((ConNF.Allowable.comp (Quiver.Hom.toPath ⋯)) ρ • a)

def ConNF.StructLAction.FOAMotive [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (ψ : ConNF.StructLAction ↑β) (ρ : ConNF.Allowable ↑β) : ConNF.Address ↑β → Prop

Equations

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

theorem ConNF.StructLAction.foaMotive_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (ψ : ConNF.StructLAction ↑β) (h₁ : ψ.Lawful) (ρ : ConNF.Allowable ↑β) (hρ : (ψ.toApprox h₁).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) (ha : ((ψ A).atomMap a).Dom) : ConNF.Allowable.toStructPerm ρ A • a = ((ψ A).atomMap a).get ha

theorem ConNF.StructLAction.foaMotive_litter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (ψ : ConNF.StructLAction ↑β) (h₁ : ψ.Lawful) (h₂ : ψ.Coherent) (ρ : ConNF.Allowable ↑β) (hρ : (ψ.toApprox h₁).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (ih : ∀ c < { path := A, value := Sum.inr L.toNearLitter }, ψ.FOAMotive ρ c) (hL : ((ψ A).litterMap L).Dom) : ConNF.Allowable.toStructPerm ρ A • L = (((ψ A).litterMap L).get hL).fst

theorem ConNF.StructLAction.foaMotive_nearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (ψ : ConNF.StructLAction ↑β) (h₁ : ψ.Lawful) (h₂ : ψ.Coherent) (ρ : ConNF.Allowable ↑β) (hρ : (ψ.toApprox h₁).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (ih : ∀ c < { path := A, value := Sum.inr L.toNearLitter }, ψ.FOAMotive ρ c) (hL : ((ψ A).litterMap L).Dom) : ConNF.Allowable.toStructPerm ρ A • L.toNearLitter = ((ψ A).litterMap L).get hL

theorem ConNF.StructLAction.freedom_of_action [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (ψ : ConNF.StructLAction ↑β) (h₁ : ψ.Lawful) (h₂ : ψ.Coherent) : ∃ (ρ : ConNF.Allowable ↑β), ψ.Approximates (ConNF.Allowable.toStructPerm ρ)

structure ConNF.StructNLAction.CoherentDom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) : Prop

• mapFlexible : ∀ (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (hN : ((ξ A).nearLitterMap N).Dom), ConNF.Flexible A N.fst → ConNF.Flexible A (((ξ A).nearLitterMap N).get hN).fst
• atom_bot_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [inst : ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} {Nt : ConNF.NearLitter}, Nt.fst = ConNF.fuzz ⋯ a → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ (A.cons ⋯)).atomMap a).Dom
• atom_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {a : ConNF.Atom} {Nt : ConNF.NearLitter}, Nt.fst = ConNF.fuzz hδε t → { path := B, value := Sum.inl a } ∈ t.support → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ ((A.cons hδ).comp B)).atomMap a).Dom
• nearLitter_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N Nt : ConNF.NearLitter}, Nt.fst = ConNF.fuzz hδε t → { path := B, value := Sum.inr N } ∈ t.support → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ ((A.cons hδ).comp B)).nearLitterMap N).Dom

theorem ConNF.StructNLAction.CoherentDom.mapFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ξ : ConNF.StructNLAction ↑β} (self : ξ.CoherentDom) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (hN : ((ξ A).nearLitterMap N).Dom) : ConNF.Flexible A N.fst → ConNF.Flexible A (((ξ A).nearLitterMap N).get hN).fst

theorem ConNF.StructNLAction.CoherentDom.atom_bot_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ξ : ConNF.StructNLAction ↑β} (self : ξ.CoherentDom) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} {Nt : ConNF.NearLitter} : Nt.fst = ConNF.fuzz ⋯ a → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ (A.cons ⋯)).atomMap a).Dom

theorem ConNF.StructNLAction.CoherentDom.atom_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ξ : ConNF.StructNLAction ↑β} (self : ξ.CoherentDom) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {a : ConNF.Atom} {Nt : ConNF.NearLitter} : Nt.fst = ConNF.fuzz hδε t → { path := B, value := Sum.inl a } ∈ t.support → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ ((A.cons hδ).comp B)).atomMap a).Dom

theorem ConNF.StructNLAction.CoherentDom.nearLitter_dom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ξ : ConNF.StructNLAction ↑β} (self : ξ.CoherentDom) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N : ConNF.NearLitter} {Nt : ConNF.NearLitter} : Nt.fst = ConNF.fuzz hδε t → { path := B, value := Sum.inr N } ∈ t.support → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ ((A.cons hδ).comp B)).nearLitterMap N).Dom

structure ConNF.StructNLAction.Coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) extends ConNF.StructNLAction.CoherentDom : Prop

• mapFlexible : ∀ (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (hN : ((ξ A).nearLitterMap N).Dom), ConNF.Flexible A N.fst → ConNF.Flexible A (((ξ A).nearLitterMap N).get hN).fst
• atom_bot_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [inst : ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} {Nt : ConNF.NearLitter}, Nt.fst = ConNF.fuzz ⋯ a → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ (A.cons ⋯)).atomMap a).Dom
• atom_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {a : ConNF.Atom} {Nt : ConNF.NearLitter}, Nt.fst = ConNF.fuzz hδε t → { path := B, value := Sum.inl a } ∈ t.support → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ ((A.cons hδ).comp B)).atomMap a).Dom
• nearLitter_dom : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {B : ConNF.ExtendedIndex ↑δ} {N Nt : ConNF.NearLitter}, Nt.fst = ConNF.fuzz hδε t → { path := B, value := Sum.inr N } ∈ t.support → ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom → ((ξ ((A.cons hδ).comp B)).nearLitterMap N).Dom
• coherent_coe : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [inst_2 : ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {Nt : ConNF.NearLitter} (hNt : Nt.fst = ConNF.fuzz hδε t) (h : ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom) (ρ : ConNF.Allowable ↑γ), (∀ (B : ConNF.ExtendedIndex ↑δ) (a : ConNF.Atom) (ha : { path := B, value := Sum.inl a } ∈ t.support), ((ξ ((A.cons hδ).comp B)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • a) → (∀ (B : ConNF.ExtendedIndex ↑δ) (N : ConNF.NearLitter) (ha : { path := B, value := Sum.inr N } ∈ t.support), ((ξ ((A.cons hδ).comp B)).nearLitterMap N).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • N) → (((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).get h).fst = ConNF.fuzz hδε ((ConNF.Allowable.comp (Quiver.Hom.toPath hδ)) ρ • t)
• coherent_bot : ∀ {γ : ConNF.Λ} [inst : ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [inst_1 : ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} {Nt : ConNF.NearLitter} (hNt : Nt.fst = ConNF.fuzz ⋯ a) (h : ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom) (ρ : ConNF.Allowable ↑γ), ((ξ (A.cons ⋯)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • a → (((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).get h).fst = ConNF.fuzz ⋯ ((ConNF.Allowable.comp (Quiver.Hom.toPath ⋯)) ρ • a)

theorem ConNF.StructNLAction.Coherent.coherent_coe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ξ : ConNF.StructNLAction ↑β} (self : ξ.Coherent) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {δ : ConNF.Λ} [ConNF.LtLevel ↑δ] {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hδ : ↑δ < ↑γ) (hε : ↑ε < ↑γ) (hδε : ↑δ ≠ ↑ε) {t : ConNF.Tangle ↑δ} {Nt : ConNF.NearLitter} (hNt : Nt.fst = ConNF.fuzz hδε t) (h : ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom) (ρ : ConNF.Allowable ↑γ) : (∀ (B : ConNF.ExtendedIndex ↑δ) (a : ConNF.Atom) (ha : { path := B, value := Sum.inl a } ∈ t.support), ((ξ ((A.cons hδ).comp B)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • a) → (∀ (B : ConNF.ExtendedIndex ↑δ) (N : ConNF.NearLitter) (ha : { path := B, value := Sum.inr N } ∈ t.support), ((ξ ((A.cons hδ).comp B)).nearLitterMap N).get ⋯ = ConNF.Allowable.toStructPerm ρ ((Quiver.Hom.toPath hδ).comp B) • N) → (((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).get h).fst = ConNF.fuzz hδε ((ConNF.Allowable.comp (Quiver.Hom.toPath hδ)) ρ • t)

theorem ConNF.StructNLAction.Coherent.coherent_bot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {ξ : ConNF.StructNLAction ↑β} (self : ξ.Coherent) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) {ε : ConNF.Λ} [ConNF.LtLevel ↑ε] (hε : ↑ε < ↑γ) {a : ConNF.Atom} {Nt : ConNF.NearLitter} (hNt : Nt.fst = ConNF.fuzz ⋯ a) (h : ((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).Dom) (ρ : ConNF.Allowable ↑γ) : ((ξ (A.cons ⋯)).atomMap a).get ⋯ = ConNF.Allowable.toStructPerm ρ (Quiver.Hom.toPath ⋯) • a → (((ξ ((A.cons hε).cons ⋯)).nearLitterMap Nt).get h).fst = ConNF.fuzz ⋯ ((ConNF.Allowable.comp (Quiver.Hom.toPath ⋯)) ρ • a)

noncomputable def ConNF.BaseNLAction.action [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : ConNF.BaseLAction

Equations

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

noncomputable def ConNF.StructNLAction.action [ConNF.Params] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) (hξ : ξ.Lawful) : ConNF.StructLAction ↑β

Equations

• ξ.action hξ A = (ξ A).action ⋯

theorem ConNF.BaseNLAction.action_lawful [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : (ξ.action hξ).Lawful

theorem ConNF.StructNLAction.action_lawful [ConNF.Params] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) (hξ : ξ.Lawful) : (ξ.action hξ).Lawful

@[simp]

theorem ConNF.BaseNLAction.action_atomMap [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : (ξ.action hξ).atomMap = (ξ.withLitters hξ).atomMap

@[simp]

theorem ConNF.BaseNLAction.action_litterMap [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : (ξ.action hξ).litterMap = fun (L : ConNF.Litter) => (ξ.withLitters hξ).nearLitterMap L.toNearLitter

@[simp]

theorem ConNF.StructNLAction.action_atomMap [ConNF.Params] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) (hξ : ξ.Lawful) (A : ConNF.ExtendedIndex ↑β) : (ξ.action hξ A).atomMap = ((ξ A).withLitters ⋯).atomMap

@[simp]

theorem ConNF.StructNLAction.action_litterMap [ConNF.Params] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) (hξ : ξ.Lawful) (A : ConNF.ExtendedIndex ↑β) : (ξ.action hξ A).litterMap = fun (L : ConNF.Litter) => ((ξ A).withLitters ⋯).nearLitterMap L.toNearLitter

theorem ConNF.BaseNLAction.action_approximates [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) (π : ConNF.BasePerm) (h : (ξ.action hξ).Approximates π) : ξ.Approximates π

theorem ConNF.StructNLAction.action_approximates [ConNF.Params] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) (hξ : ξ.Lawful) (π : ConNF.StructPerm ↑β) (h : (ξ.action hξ).Approximates π) : ξ.Approximates π

theorem ConNF.BaseNLAction.litterPresent_of_dom [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {L : ConNF.Litter} (h : ((ξ.withLitters hξ).nearLitterMap L.toNearLitter).Dom) : ξ.LitterPresent L

theorem ConNF.BaseNLAction.symmDiff [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst = N₂.fst) (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) : symmDiff ↑((ξ.nearLitterMap N₁).get hN₁) ↑((ξ.nearLitterMap N₂).get hN₂) = ⋃ (a : ConNF.Atom), ⋃ (ha : a ∈ symmDiff ↑N₁ ↑N₂), {(ξ.atomMap a).get ⋯}

theorem ConNF.StructNLAction.action_coherentDom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) (h₁ : ξ.Lawful) (h₂ : ξ.Coherent) : (ξ.action h₁).CoherentDom

theorem ConNF.StructNLAction.action_coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (ξ : ConNF.StructNLAction ↑β) (h₁ : ξ.Lawful) (h₂ : ξ.Coherent) : (ξ.action h₁).Coherent

theorem ConNF.StructNLAction.freedom_of_action [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (ξ : ConNF.StructNLAction ↑β) (h₁ : ξ.Lawful) (h₂ : ξ.Coherent) : ∃ (ρ : ConNF.Allowable ↑β), ξ.Approximates (ConNF.Allowable.toStructPerm ρ)