theorem ConNF.StructApprox.atom_injective_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {a : ConNF.Atom} {b : ConNF.Atom} {A : ConNF.ExtendedIndex ↑β} (hac : { path := A, value := Sum.inl a } ∈ ConNF.StructApprox.reflTransConstrained c d) (hbc : { path := A, value := Sum.inl b } ∈ ConNF.StructApprox.reflTransConstrained c d) (h : π.completeAtomMap A a = π.completeAtomMap A b) : a = b

def ConNF.StructApprox.InOut [ConNF.Params] (π : ConNF.BasePerm) (a : ConNF.Atom) (L : ConNF.Litter) : Prop

Equations

• ConNF.StructApprox.InOut π a L = Xor' (a.1 = L) ((π • a).1 = π • L)

theorem ConNF.StructApprox.inOut_def [ConNF.Params] {π : ConNF.BasePerm} {a : ConNF.Atom} {L : ConNF.Litter} : ConNF.StructApprox.InOut π a L ↔ Xor' (a.1 = L) ((π • a).1 = π • L)

theorem ConNF.StructApprox.isException_of_inOut [ConNF.Params] {π : ConNF.BasePerm} {a : ConNF.Atom} {L : ConNF.Litter} : ConNF.StructApprox.InOut π a L → π.IsException a ∨ π.IsException (π • a)

structure ConNF.StructApprox.Biexact [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (π : ConNF.StructPerm ↑β) (π' : ConNF.StructPerm ↑β) (c : ConNF.Address ↑β) : Prop

• smul_eq_smul_atom : ∀ (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom), { path := A, value := Sum.inl a } ≤ c → π A • a = π' A • a
• smul_eq_smul_litter : ∀ (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter), { path := A, value := Sum.inr L.toNearLitter } ≤ c → ConNF.Flexible A L → π A • L = π' A • L
• exact : ∀ (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter), { path := A, value := Sum.inr L.toNearLitter } ≤ c → π A • L = π' A • L → π A • L.toNearLitter = π' A • L.toNearLitter

theorem ConNF.StructApprox.Biexact.smul_eq_smul_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {π : ConNF.StructPerm ↑β} {π' : ConNF.StructPerm ↑β} {c : ConNF.Address ↑β} (self : ConNF.StructApprox.Biexact π π' c) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) : { path := A, value := Sum.inl a } ≤ c → π A • a = π' A • a

theorem ConNF.StructApprox.Biexact.smul_eq_smul_litter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {π : ConNF.StructPerm ↑β} {π' : ConNF.StructPerm ↑β} {c : ConNF.Address ↑β} (self : ConNF.StructApprox.Biexact π π' c) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : { path := A, value := Sum.inr L.toNearLitter } ≤ c → ConNF.Flexible A L → π A • L = π' A • L

theorem ConNF.StructApprox.Biexact.exact [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {π : ConNF.StructPerm ↑β} {π' : ConNF.StructPerm ↑β} {c : ConNF.Address ↑β} (self : ConNF.StructApprox.Biexact π π' c) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) : { path := A, value := Sum.inr L.toNearLitter } ≤ c → π A • L = π' A • L → π A • L.toNearLitter = π' A • L.toNearLitter

theorem ConNF.StructApprox.Biexact.constrains [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {π : ConNF.StructPerm ↑β} {π' : ConNF.StructPerm ↑β} {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (h : ConNF.StructApprox.Biexact π π' c) (h' : d ≤ c) : ConNF.StructApprox.Biexact π π' d

theorem ConNF.StructApprox.Biexact.smul_eq_smul [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {π : ConNF.Allowable ↑β} {π' : ConNF.Allowable ↑β} {c : ConNF.Address ↑β} (h : ConNF.StructApprox.Biexact (ConNF.Allowable.toStructPerm π) (ConNF.Allowable.toStructPerm π') c) : π • c = π' • c

theorem ConNF.StructApprox.Biexact.smul_eq_smul_nearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {π : ConNF.Allowable ↑β} {π' : ConNF.Allowable ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} (h : ConNF.StructApprox.Biexact (ConNF.Allowable.toStructPerm π) (ConNF.Allowable.toStructPerm π') { path := A, value := Sum.inr N }) : ConNF.Allowable.toStructPerm π A • N = ConNF.Allowable.toStructPerm π' A • N

theorem ConNF.StructApprox.mem_dom_of_exactlyApproximates [ConNF.Params] [ConNF.Level] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {π₀ : ConNF.StructApprox ↑β} {π : ConNF.StructPerm ↑β} (hπ : π₀.ExactlyApproximates π) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {L : ConNF.Litter} (h : ConNF.StructApprox.InOut (π A) a L) : a ∈ (π₀ A).atomPerm.domain

theorem ConNF.StructApprox.constrainedAction_comp_mapFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} {s : Set (ConNF.Address ↑β)} {hs : ConNF.Small s} (A : Quiver.Path ↑β ↑γ) : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp A (π.constrainedAction s hs))

We can prove that map_flexible holds at any constrained_action without any lawful hypothesis.

theorem ConNF.StructApprox.ihAction_comp_mapFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} (c : ConNF.Address ↑β) (A : Quiver.Path ↑β ↑γ) : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp A (ConNF.StructApprox.ihAction π.foaHypothesis))

theorem ConNF.StructApprox.ihsAction_comp_mapFlexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) (A : Quiver.Path ↑β ↑γ) : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp A (π.ihsAction c d))

theorem ConNF.StructApprox.completeLitterMap_flexible [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.Flexible A L) : ConNF.Flexible A (π.completeLitterMap A L)

noncomputable def ConNF.StructApprox.completeLitterMap_inflexibleBot [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleBot A L) : ConNF.InflexibleBot A (π.completeLitterMap A L)

Equations

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

noncomputable def ConNF.StructApprox.completeLitterMap_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleCoe A L) (hL : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) : ConNF.InflexibleCoe A (π.completeLitterMap A L)

Equations

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

theorem ConNF.StructApprox.completeLitterMap_flexible' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (hL : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) (h : ConNF.Flexible A (π.completeLitterMap A L)) : ConNF.Flexible A L

theorem ConNF.StructApprox.completeLitterMap_flexible_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (hL : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) : ConNF.Flexible A (π.completeLitterMap A L) ↔ ConNF.Flexible A L

noncomputable def ConNF.StructApprox.completeLitterMap_inflexibleBot' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (hL : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) (h : ConNF.InflexibleBot A (π.completeLitterMap A L)) : ConNF.InflexibleBot A L

Equations

• ConNF.StructApprox.completeLitterMap_inflexibleBot' hπf hcd hL h = ⋯.some

theorem ConNF.StructApprox.completeLitterMap_inflexibleBot_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (hL : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) : Nonempty (ConNF.InflexibleBot A (π.completeLitterMap A L)) ↔ Nonempty (ConNF.InflexibleBot A L)

noncomputable def ConNF.StructApprox.completeLitterMap_inflexibleCoe' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleCoe A (π.completeLitterMap A L)) : ConNF.InflexibleCoe A L

Equations

• ConNF.StructApprox.completeLitterMap_inflexibleCoe' hπf h = ⋯.some

theorem ConNF.StructApprox.completeLitterMap_inflexibleCoe_iff [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (hL : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) : Nonempty (ConNF.InflexibleCoe A (π.completeLitterMap A L)) ↔ Nonempty (ConNF.InflexibleCoe A L)

theorem ConNF.StructApprox.supports [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] {π : ConNF.Allowable ↑β} {π' : ConNF.Allowable ↑β} {t : ConNF.Tangle ↑β} (ha : ∀ (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom), { path := A, value := Sum.inl a } ∈ t.support → ConNF.Allowable.toStructPerm π A • a = ConNF.Allowable.toStructPerm π' A • a) (hN : ∀ (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter), { path := A, value := Sum.inr N } ∈ t.support → ConNF.Allowable.toStructPerm π A • N = ConNF.Allowable.toStructPerm π' A • N) : π • t = π' • t

theorem ConNF.StructApprox.ConNF.StructApprox.extracted_1 [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (s : Set (ConNF.Address ↑β)) (hs : ConNF.Small s) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (π.constrainedAction s hs))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (π.constrainedAction s hs)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) (B : ConNF.ExtendedIndex ↑γ) (N : ConNF.NearLitter) (c : ConNF.Address ↑β) (hc₁ : c ∈ s) (hc₂ : { path := A.comp B, value := Sum.inr N } ≤ c) (L : ConNF.Litter) (hc₂' : { path := A.comp B, value := Sum.inr L.toNearLitter } ≤ c) (hNL : N.fst = L) (hL : ConNF.InflexibleBot B L) : π.completeLitterMap (A.comp B) L = ConNF.Allowable.toStructPerm ρ B • L

theorem ConNF.StructApprox.ConNF.StructApprox.extracted_2 [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (s : Set (ConNF.Address ↑β)) (hs : ConNF.Small s) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (π.constrainedAction s hs))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (π.constrainedAction s hs)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) (B : ConNF.ExtendedIndex ↑γ) (N : ConNF.NearLitter) (ih : ∀ (C : ConNF.ExtendedIndex ↑γ) (M : ConNF.NearLitter), { path := C, value := Sum.inr M } < { path := B, value := Sum.inr N } → π.completeNearLitterMap (A.comp C) M = ConNF.Allowable.toStructPerm ρ C • M) (c : ConNF.Address ↑β) (hc₁ : c ∈ s) (hc₂ : { path := A.comp B, value := Sum.inr N } ≤ c) (L : ConNF.Litter) (hc₂' : { path := A.comp B, value := Sum.inr L.toNearLitter } ≤ c) (hNL : N.fst = L) (hL : ConNF.InflexibleCoe B L) : π.completeLitterMap (A.comp B) L = ConNF.Allowable.toStructPerm ρ B • L

theorem ConNF.StructApprox.constrainedAction_coherent' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (N : ConNF.ExtendedIndex ↑γ × ConNF.NearLitter) (s : Set (ConNF.Address ↑β)) (hs : ConNF.Small s) (hc : ∃ c ∈ s, { path := A.comp N.1, value := Sum.inr N.2 } ≤ c) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (π.constrainedAction s hs))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (π.constrainedAction s hs)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeNearLitterMap (A.comp N.1) N.2 = ConNF.Allowable.toStructPerm ρ N.1 • N.2

theorem ConNF.StructApprox.constrainedAction_coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (N : ConNF.NearLitter) (s : Set (ConNF.Address ↑β)) (hs : ConNF.Small s) (hc : ∃ c ∈ s, { path := A.comp B, value := Sum.inr N } ≤ c) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (π.constrainedAction s hs))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (π.constrainedAction s hs)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeNearLitterMap (A.comp B) N = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • N

Coherence lemma: The action of the complete litter map, below a given address c, is equal to the action of any allowable permutation that exactly approximates it. This condition can only be applied for γ < α as we're dealing with lower allowable permutations.

theorem ConNF.StructApprox.constrainedAction_coherent_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (a : ConNF.Atom) (s : Set (ConNF.Address ↑β)) (hs : ConNF.Small s) (hc : ∃ c ∈ s, { path := A.comp B, value := Sum.inl a } ≤ c) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (π.constrainedAction s hs))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (π.constrainedAction s hs)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeAtomMap (A.comp B) a = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • a

The coherence lemma for atoms, which is much easier to prove. The statement is here for symmetry.

theorem ConNF.StructApprox.ihsAction_coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (N : ConNF.NearLitter) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) (hc : { path := A.comp B, value := Sum.inr N } ∈ ConNF.StructApprox.transConstrained c d) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (π.ihsAction c d))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (π.ihsAction c d)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeNearLitterMap (A.comp B) N = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • N

theorem ConNF.StructApprox.ihsAction_coherent_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (a : ConNF.Atom) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) (hc : { path := A.comp B, value := Sum.inl a } < c) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (π.ihsAction c d))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (π.ihsAction c d)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeAtomMap (A.comp B) a = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • a

theorem ConNF.StructApprox.ihAction_coherent [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (N : ConNF.NearLitter) (c : ConNF.Address ↑β) (hc : { path := A.comp B, value := Sum.inr N } < c) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (ConNF.StructApprox.ihAction π.foaHypothesis))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (ConNF.StructApprox.ihAction π.foaHypothesis)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeNearLitterMap (A.comp B) N = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • N

theorem ConNF.StructApprox.ihAction_coherent_atom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {γ : ConNF.Λ} [ConNF.LeLevel ↑γ] (A : Quiver.Path ↑β ↑γ) (B : ConNF.ExtendedIndex ↑γ) (a : ConNF.Atom) (c : ConNF.Address ↑β) (hc : { path := A.comp B, value := Sum.inl a } < c) (hπ : ConNF.StructLAction.Lawful (ConNF.Tree.comp A (ConNF.StructApprox.ihAction π.foaHypothesis))) (ρ : ConNF.Allowable ↑γ) (h : (ConNF.StructLAction.toApprox (ConNF.Tree.comp A (ConNF.StructApprox.ihAction π.foaHypothesis)) hπ).ExactlyApproximates (ConNF.Allowable.toStructPerm ρ)) : π.completeAtomMap (A.comp B) a = ConNF.Tree.comp B (ConNF.Allowable.toStructPerm ρ) • a

theorem ConNF.StructApprox.ihAction_smul_tangle' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (hL₁ : { path := A, value := Sum.inr L.toNearLitter } ≤ c) (hL₂ : ConNF.InflexibleCoe A L) (hlaw₁ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (hL₂.path.B.cons ⋯) (ConNF.StructApprox.ihAction π.foaHypothesis))) (hlaw₂ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (hL₂.path.B.cons ⋯) (π.ihsAction c d))) : (ConNF.StructApprox.ihAction π.foaHypothesis).hypothesisedAllowable hL₂.path hlaw₁ ⋯ • hL₂.t = (π.ihsAction c d).hypothesisedAllowable hL₂.path hlaw₂ ⋯ • hL₂.t

theorem ConNF.StructApprox.ihAction_smul_tangle [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (hL₁ : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) (hL₂ : ConNF.InflexibleCoe A L) (hlaw₁ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (hL₂.path.B.cons ⋯) (ConNF.StructApprox.ihAction π.foaHypothesis))) (hlaw₂ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (hL₂.path.B.cons ⋯) (π.ihsAction c d))) : (ConNF.StructApprox.ihAction π.foaHypothesis).hypothesisedAllowable hL₂.path hlaw₁ ⋯ • hL₂.t = (π.ihsAction c d).hypothesisedAllowable hL₂.path hlaw₂ ⋯ • hL₂.t

theorem ConNF.StructApprox.litter_injective_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} (h₁ : { path := A, value := Sum.inr L₁.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) (h₂ : { path := A, value := Sum.inr L₂.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) (h : π.completeLitterMap A L₁ = π.completeLitterMap A L₂) : L₁ = L₂

inductive ConNF.StructApprox.SplitLt {α : Type u_1} (r : α → α → Prop) : α × α → α × α → Prop

Split relation Let < denote a relation on α. The split relation <ₛ defined on α × α is defined by:

• a < b → (a, c) <ₛ (b, c) (left <)
• b < c → (a, b) <ₛ (a, c) (right <)
• a < c → b < c → (a, b) <ₛ (c, d) (left split)
• a < d → b < d → (a, b) <ₛ (c, d) (right split)

This is more granular than the standard product of relations, which would be given by just the first two constructors. The splitting constructors allow one to "split" either c or d into two lower values a and b.

Splitting has applications with well-founded relations; in particular, <ₛ is well-founded whenever < is, so this relation can simplify certain inductive steps.

• left_lt: ∀ {α : Type u_1} {r : α → α → Prop} ⦃a b c : α⦄, r a b → ConNF.StructApprox.SplitLt r (a, c) (b, c)
• right_lt: ∀ {α : Type u_1} {r : α → α → Prop} ⦃a b c : α⦄, r b c → ConNF.StructApprox.SplitLt r (a, b) (a, c)
• left_split: ∀ {α : Type u_1} {r : α → α → Prop} ⦃a b c d : α⦄, r a c → r b c → ConNF.StructApprox.SplitLt r (a, b) (c, d)
• right_split: ∀ {α : Type u_1} {r : α → α → Prop} ⦃a b c d : α⦄, r a d → r b d → ConNF.StructApprox.SplitLt r (a, b) (c, d)

theorem ConNF.StructApprox.le_wellOrderExtension_lt {α : Type u_1} {r : α → α → Prop} (hr : WellFounded r) : r ≤ LT.lt

theorem ConNF.StructApprox.lex_lt_of_splitLt {α : Type u_1} {r : α → α → Prop} (hr : WellFounded r) : ConNF.StructApprox.SplitLt r ≤ InvImage (Prod.Lex LT.lt LT.lt) fun (a : α × α) => if a.1 < a.2 then (a.2, a.1) else (a.1, a.2)

theorem ConNF.StructApprox.splitLt_wellFounded {α : Type u_1} {r : α → α → Prop} (hr : WellFounded r) : WellFounded (ConNF.StructApprox.SplitLt r)

theorem ConNF.StructApprox.completeAtomMap_mem_completeNearLitterMap_toNearLitter' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {c : ConNF.Address ↑β} {d : ConNF.Address ↑β} (hcd : (π.ihsAction c d).Lawful) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {L : ConNF.Litter} (ha : a.1 = L) (hL : { path := A, value := Sum.inr L.toNearLitter } ∈ ConNF.StructApprox.reflTransConstrained c d) : π.completeAtomMap A a ∈ π.completeNearLitterMap A L.toNearLitter

theorem ConNF.StructApprox.ihsAction_lawful_extends [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) (hπ : ∀ (e f : ConNF.Address ↑β), ConNF.StructApprox.SplitLt (fun (c d : ConNF.Address ↑β) => c < d) (e, f) (c, d) → (π.ihsAction e f).Lawful) : (π.ihsAction c d).Lawful

theorem ConNF.StructApprox.ihsAction_lawful [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) (d : ConNF.Address ↑β) : (π.ihsAction c d).Lawful

Every ihs_action is lawful. This is a consequence of all of the previous lemmas.

theorem ConNF.StructApprox.ihAction_lawful [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (c : ConNF.Address ↑β) : (ConNF.StructApprox.ihAction π.foaHypothesis).Lawful

We now establish a number of key consequences of ihs_action_lawful, such as injectivity.

theorem ConNF.StructApprox.completeAtomMap_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Function.Injective (π.completeAtomMap A)

The complete atom map is injective.

theorem ConNF.StructApprox.completeLitterMap_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Function.Injective (π.completeLitterMap A)

The complete litter map is injective.

theorem ConNF.StructApprox.completeAtomMap_mem_completeNearLitterMap_toNearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {L : ConNF.Litter} : π.completeAtomMap A a ∈ π.completeNearLitterMap A L.toNearLitter ↔ a.1 = L

Atoms inside litters are mapped inside the corresponding image near-litter.

theorem ConNF.StructApprox.mem_image_iff {α : Type u_1} {β : Type u_2} {f : α → β} (hf : Function.Injective f) (x : α) (s : Set α) : f x ∈ f '' s ↔ x ∈ s

theorem ConNF.StructApprox.completeAtomMap_mem_completeNearLitterMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {N : ConNF.NearLitter} : π.completeAtomMap A a ∈ π.completeNearLitterMap A N ↔ a ∈ N

Atoms inside near-litters are mapped inside the corresponding image near-litter.

theorem ConNF.StructApprox.completeNearLitterMap_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (hπf : π.Free) (A : ConNF.ExtendedIndex ↑β) : Function.Injective (π.completeNearLitterMap A)

The complete near-litter map is injective.