Freedom of action for structural permutations

In this file, we state and prove the freedom of action theorem for structural permutations.

Main declarations

• ConNF.StrApprox.Approximates: A structural approximation approximates an allowable permutation if it agrees with it wherever it is defined.
• ConNF.StrApprox.ExactlyApproximates: A structural approximation exactly approximates an allowable permutation if it approximates the permutation and every undefined atom is "typical" in a suitable sense.
• ConNF.StrApprox.FreedomOfAction: Freedom of action for structural approximations: every coherent approximation exactly approximates some allowable permutation.
• ConNF.StrApprox.freedomOfAction: The proof of freedom of action for structural permutations.

def ConNF.StrApprox.Approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (ρ : ConNF.AllPerm β) : Prop

Equations

• ψ.Approximates ρ = ∀ (A : β ↝ ⊥), (ψ A).Approximates (ρᵁ A)

def ConNF.StrApprox.ExactlyApproximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (ρ : ConNF.AllPerm β) : Prop

Equations

• ψ.ExactlyApproximates ρ = ∀ (A : β ↝ ⊥), (ψ A).ExactlyApproximates (ρᵁ A)

theorem ConNF.StrApprox.ExactlyApproximates.toApproximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.ExactlyApproximates ρ) : ψ.Approximates ρ

theorem ConNF.StrApprox.Approximates.mono [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ χ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (hχ : χ.Approximates ρ) (h : ψ ≤ χ) : ψ.Approximates ρ

theorem ConNF.StrApprox.ExactlyApproximates.mono [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ χ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (hχ : χ.ExactlyApproximates ρ) (h : ψ ≤ χ) : ψ.ExactlyApproximates ρ

def ConNF.StrApprox.FreedomOfAction [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] (β : ConNF.TypeIndex) [ConNF.LeLevel β] : Prop

Equations

• ConNF.StrApprox.FreedomOfAction β = ∀ (ψ : ConNF.StrApprox β), ψ.Coherent → ∃ (ρ : ConNF.AllPerm β), ψ.ExactlyApproximates ρ

theorem ConNF.StrApprox.smul_atom_mem_dom_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {a : ConNF.Atom} (ha : a ∈ (ψ A)ᴬ.dom) : ρᵁ A • a ∈ (ψ A)ᴬ.dom

theorem ConNF.StrApprox.smul_nearLitter_mem_dom_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {N : ConNF.NearLitter} (hN : N ∈ (ψ A)ᴺ.dom) : ρᵁ A • N ∈ (ψ A)ᴺ.dom

theorem ConNF.StrApprox.inv_smul_atom_mem_dom_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {a : ConNF.Atom} (ha : a ∈ (ψ A)ᴬ.dom) : (ρᵁ A)⁻¹ • a ∈ (ψ A)ᴬ.dom

theorem ConNF.StrApprox.inv_smul_nearLitter_mem_dom_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {N : ConNF.NearLitter} (hN : N ∈ (ψ A)ᴺ.dom) : (ρᵁ A)⁻¹ • N ∈ (ψ A)ᴺ.dom

theorem ConNF.StrApprox.zsmul_atom_mem_dom_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {a : ConNF.Atom} (ha : a ∈ (ψ A)ᴬ.dom) (n : ℤ) : ρᵁ A ^ n • a ∈ (ψ A)ᴬ.dom

theorem ConNF.StrApprox.zsmul_nearLitter_mem_dom_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {N : ConNF.NearLitter} (hN : N ∈ (ψ A)ᴺ.dom) (n : ℤ) : ρᵁ A ^ n • N ∈ (ψ A)ᴺ.dom

theorem ConNF.StrApprox.zsmul_atom_mem_dom_iff_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {a : ConNF.Atom} (n : ℤ) : ρᵁ A ^ n • a ∈ (ψ A)ᴬ.dom ↔ a ∈ (ψ A)ᴬ.dom

theorem ConNF.StrApprox.zsmul_nearLitter_mem_dom_iff_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {A : β ↝ ⊥} {N : ConNF.NearLitter} (n : ℤ) : ρᵁ A ^ n • N ∈ (ψ A)ᴺ.dom ↔ N ∈ (ψ A)ᴺ.dom

theorem ConNF.StrApprox.smul_support_eq_smul_of_approximates [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) {S : ConNF.Support β} (hSA : ∀ (A : β ↝ ⊥), ∀ a ∈ (S ⇘. A)ᴬ, a ∈ (ψ A)ᴬ.dom) (hSN : ∀ (A : β ↝ ⊥), ∀ N ∈ (S ⇘. A)ᴺ, N ∈ (ψ A)ᴺ.dom) : ψ • S = ρᵁ • S

def ConNF.StrApprox.addFlexible [ConNF.Params] {β : ConNF.TypeIndex} (ψ : ConNF.StrApprox β) (A : β ↝ ⊥) (L : ConNF.Litter) (hLψ : L ∉ (ψ A)ᴸ.dom) : ConNF.StrApprox β

Add a flexible litter to this approximation.

Equations

• ψ.addFlexible A L hLψ = ψ.addOrbit A (fun (x : ℤ) => L) ⋯ ⋯

theorem ConNF.StrApprox.addFlexible_coherent [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {L : ConNF.Litter} {hLψ : L ∉ (ψ A)ᴸ.dom} (hψ : ψ.Coherent) (hL : ¬ConNF.Inflexible A L) : (ψ.addFlexible A L hLψ).Coherent

theorem ConNF.StrApprox.addInflexible_aux [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ) (m n k : ℤ) : ConNF.fuzz ⋯ (ρ ^ m • t) = ConNF.fuzz ⋯ (ρ ^ n • t) → ConNF.fuzz ⋯ (ρ ^ (m + k) • t) = ConNF.fuzz ⋯ (ρ ^ (n + k) • t)

def ConNF.StrApprox.addInflexible' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) {A : β ↝ ⊥} (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ) (hL : ∀ (n : ℤ), ConNF.fuzz ⋯ (ρ ^ n • t) ∉ (ψ A)ᴸ.dom) : ConNF.StrApprox β

Equations

• ψ.addInflexible' P t ρ hL = ψ.addOrbit A (fun (n : ℤ) => ConNF.fuzz ⋯ (ρ ^ n • t)) ⋯ hL

theorem ConNF.StrApprox.smul_support_zpow [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {ρ : ConNF.AllPerm β} (h : ψ.Approximates ρ) (t : ConNF.Tangle β) {n : ℤ} (hLA : ∀ (B : β ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ B)ᴬ.dom) (hLN : ∀ (B : β ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ B)ᴺ.dom) : ψ • (ρ ^ n • t).support = ρᵁ • (ρ ^ n • t).support

theorem ConNF.StrApprox.addInflexible'_coherent [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) {ρ : ConNF.AllPerm P.δ} (hρ : ConNF.StrApprox.Approximates (ψ ⇘ P.A ↘ ⋯) ρ) {hL : ∀ (n : ℤ), ConNF.fuzz ⋯ (ρ ^ n • t) ∉ (ψ A)ᴸ.dom} (hψ : ψ.Coherent) (hLA : ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴬ.dom) (hLN : ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴺ.dom) : (ψ.addInflexible' P t ρ hL).Coherent

theorem ConNF.StrApprox.mem_dom_of_inflexible [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {L : ConNF.Litter} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (ht : L = ConNF.fuzz ⋯ t) {ρ : ConNF.AllPerm P.δ} (hρ : ConNF.StrApprox.Approximates (ψ ⇘ P.A ↘ ⋯) ρ) {n : ℤ} (hL : ConNF.fuzz ⋯ (ρ ^ n • t) ∈ (ψ A)ᴸ.dom) (hψ : ψ.Coherent) (hLA : ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴬ.dom) (hLN : ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴺ.dom) : L ∈ (ψ A)ᴸ.dom

def ConNF.StrApprox.addInflexible [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (A : β ↝ ⊥) (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ) : ConNF.StrApprox β

Equations

• ψ.addInflexible A P t ρ = if hL : ∀ (n : ℤ), ConNF.fuzz ⋯ (ρ ^ n • t) ∉ (ψ A)ᴸ.dom then ψ.addInflexible' P t ρ hL else ψ

theorem ConNF.StrApprox.le_addInflexible [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (A : β ↝ ⊥) (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ) : ψ ≤ ψ.addInflexible A P t ρ

theorem ConNF.StrApprox.addInflexible_coherent [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) {ρ : ConNF.AllPerm P.δ} (hρ : ConNF.StrApprox.Approximates (ψ ⇘ P.A ↘ ⋯) ρ) (hψ : ψ.Coherent) (hLA : ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴬ.dom) (hLN : ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴺ.dom) : (ψ.addInflexible A P t ρ).Coherent

theorem ConNF.StrApprox.mem_addInflexible_dom [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {ψ : ConNF.StrApprox β} {A : β ↝ ⊥} {L : ConNF.Litter} {P : ConNF.InflexiblePath β} {t : ConNF.Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (hL : L = ConNF.fuzz ⋯ t) {ρ : ConNF.AllPerm P.δ} (hρ : ConNF.StrApprox.Approximates (ψ ⇘ P.A ↘ ⋯) ρ) (hψ : ψ.Coherent) (hLA : ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, a ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴬ.dom) (hLN : ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, N ∈ (ψ (P.A ↘ ⋯ ⇘ B))ᴺ.dom) : L ∈ (ψ.addInflexible A P t ρ A)ᴸ.dom

theorem ConNF.StrApprox.exists_extension_of_minimal [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (A : β ↝ ⊥) (L : ConNF.Litter) (hψ : ψ.Coherent) (foa : ∀ δ < β, ∀ [inst : ConNF.LeLevel δ], ConNF.StrApprox.FreedomOfAction δ) (hLA : ∀ (B : β ↝ ⊥) (a : ConNF.Atom), ConNF.pos a < ConNF.pos L → a ∈ (ψ B)ᴬ.dom) (hLN : ∀ (B : β ↝ ⊥) (N : ConNF.NearLitter), ConNF.pos N < ConNF.pos L → N ∈ (ψ B)ᴺ.dom) : ∃ χ ≥ ψ, χ.Coherent ∧ L ∈ (χ A)ᴸ.dom

theorem ConNF.StrApprox.exists_extension_of_minimal' [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (A : β ↝ ⊥) (L : ConNF.Litter) (hL : L ∉ (ψ A)ᴸ.dom) (hψ : ψ.Coherent) (foa : ∀ δ < β, ∀ [inst : ConNF.LeLevel δ], ConNF.StrApprox.FreedomOfAction δ) (hL' : ∀ (B : β ↝ ⊥) (L' : ConNF.Litter), ConNF.pos L' < ConNF.pos L → L' ∈ (ψ B)ᴸ.dom) : ∃ χ > ψ, χ.Coherent

theorem ConNF.StrApprox.exists_total [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (hψ : ψ.Coherent) (foa : ∀ δ < β, ∀ [inst : ConNF.LeLevel δ], ConNF.StrApprox.FreedomOfAction δ) : ∃ χ ≥ ψ, χ.Coherent ∧ χ.Total

theorem ConNF.StrApprox.exists_exactlyApproximates_of_total [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ψ : ConNF.StrApprox β) (hψ₁ : ψ.Coherent) (hψ₂ : ψ.Total) : ∃ (ρ : ConNF.AllPerm β), ψ.ExactlyApproximates ρ

theorem ConNF.StrApprox.freedomOfAction [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] : ConNF.StrApprox.FreedomOfAction β