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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ψ : StrApprox β) (ρ : AllPerm β) : Prop

Equations

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

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

Equations

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

Add a flexible litter to this approximation.

Equations

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

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

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

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

Equations

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

theorem ConNF.StrApprox.smul_support_zpow [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ψ : StrApprox β} {ρ : AllPerm β} (h : ψ.Approximates ρ) (t : 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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) {ρ : AllPerm P.δ} (hρ : Approximates (ψ ⇘ P.A ↘ ⋯) ρ) {hL : ∀ (n : ℤ), 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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {L : Litter} {P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (ht : L = fuzz ⋯ t) {ρ : AllPerm P.δ} (hρ : Approximates (ψ ⇘ P.A ↘ ⋯) ρ) {n : ℤ} (hL : 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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ψ : StrApprox β) (A : β ↝ ⊥) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : 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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ψ : StrApprox β) (A : β ↝ ⊥) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : ψ ≤ ψ.addInflexible A P t ρ

theorem ConNF.StrApprox.addInflexible_coherent [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) {ρ : AllPerm P.δ} (hρ : 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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {ψ : StrApprox β} {A : β ↝ ⊥} {L : Litter} {P : InflexiblePath β} {t : Tangle P.δ} (hA : A = P.A ↘ ⋯ ↘.) (hL : L = fuzz ⋯ t) {ρ : AllPerm P.δ} (hρ : 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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ψ : StrApprox β) (A : β ↝ ⊥) (L : Litter) (hψ : ψ.Coherent) (foa : ∀ δ < β, ∀ [inst : LeLevel δ], FreedomOfAction δ) (hLA : ∀ (B : β ↝ ⊥) (a : Atom), pos a < pos L → a ∈ (ψ B)ᴬ.dom) (hLN : ∀ (B : β ↝ ⊥) (N : NearLitter), pos N < pos L → N ∈ (ψ B)ᴺ.dom) : ∃ χ ≥ ψ, χ.Coherent ∧ L ∈ (χ A)ᴸ.dom

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

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

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

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