ConNF.FOA.Complete.CompleteAction

We now construct the completed action of a structural approximation using well-founded recursion on addresses. It remains to prove that this map yields an allowable permutation. TODO: Rename completeAtomMap, atomCompletion etc.

source

noncomputable def ConNF.StructApprox.completeAtomMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) :

ConNF.ExtendedIndex ↑β → ConNF.Atom → ConNF.Atom

Equations

π.completeAtomMap = ConNF.HypAction.fixAtom π.atomCompletion π.nearLitterCompletion

Instances For

source

noncomputable def ConNF.StructApprox.completeNearLitterMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) :

ConNF.ExtendedIndex ↑β → ConNF.NearLitter → ConNF.NearLitter

Equations

π.completeNearLitterMap = ConNF.HypAction.fixNearLitter π.atomCompletion π.nearLitterCompletion

Instances For

source

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

ConNF.Litter

Equations

π.completeLitterMap A L = (π.completeNearLitterMap A L.toNearLitter).fst

Instances For

source

noncomputable def ConNF.StructApprox.foaHypothesis [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) {c : ConNF.Address ↑β} :

ConNF.HypAction c

Equations

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

Instances For

source

theorem ConNF.StructApprox.completeAtomMap_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} :

π.completeAtomMap A a = π.atomCompletion A a π.foaHypothesis

source

theorem ConNF.StructApprox.completeNearLitterMap_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} :

π.completeNearLitterMap A N = π.nearLitterCompletion A N π.foaHypothesis

source

theorem ConNF.StructApprox.completeLitterMap_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} :

π.completeLitterMap A L = π.litterCompletion A L π.foaHypothesis

source

theorem ConNF.StructApprox.completeNearLitterMap_fst_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} :

(π.completeNearLitterMap A L.toNearLitter).fst = π.completeLitterMap A L

source

@[simp]

theorem ConNF.StructApprox.completeNearLitterMap_fst_eq' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} :

(π.completeNearLitterMap A N).fst = π.completeLitterMap A N.fst

source

@[simp]

theorem ConNF.StructApprox.foaHypothesis_atomImage [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} {c : ConNF.Address ↑β} (h : { path := A, value := Sum.inl a } < c) :

π.foaHypothesis.atomImage A a h = π.completeAtomMap A a

source

@[simp]

theorem ConNF.StructApprox.foaHypothesis_nearLitterImage [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {N : ConNF.NearLitter} {c : ConNF.Address ↑β} (h : { path := A, value := Sum.inr N } < c) :

π.foaHypothesis.nearLitterImage A N h = π.completeNearLitterMap A N

source

theorem ConNF.StructApprox.completeAtomMap_eq_of_mem_domain [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} (h : a ∈ (π A).atomPerm.domain) :

π.completeAtomMap A a = π A • a

source

theorem ConNF.StructApprox.completeAtomMap_eq_of_not_mem_domain [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} (h : a ∉ (π A).atomPerm.domain) :

π.completeAtomMap A a = ↑((((π A).largestSublitter a.1).equiv ((π A).largestSublitter (π.completeLitterMap A a.1))) ⟨a, ⋯⟩)

source

@[simp]

def ConNF.StructApprox.nearLitterHypothesis_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) :

ConNF.StructApprox.nearLitterHypothesis A N π.foaHypothesis = π.foaHypothesis

Equations

⋯ = ⋯

Instances For

source

theorem ConNF.StructApprox.completeLitterMap_eq_of_inflexibleCoe [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleCoe A L) (h₁ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction π.foaHypothesis))) (h₂ : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction π.foaHypothesis))) :

π.completeLitterMap A L = ConNF.fuzz ⋯ ((ConNF.StructApprox.ihAction π.foaHypothesis).hypothesisedAllowable h.path h₁ h₂ • h.t)

A basic definition unfold.

source

theorem ConNF.StructApprox.completeLitterMap_eq_of_inflexible_coe' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {A : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} (h : ConNF.InflexibleCoe A L) :

π.completeLitterMap A L = if h' : ConNF.StructLAction.Lawful (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction π.foaHypothesis)) ∧ ConNF.StructLAction.MapFlexible (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction π.foaHypothesis)) then ConNF.fuzz ⋯ ((ConNF.StructApprox.ihAction π.foaHypothesis).hypothesisedAllowable h.path ⋯ ⋯ • h.t) else L

source

theorem ConNF.StructApprox.completeLitterMap_eq_of_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) :

π.completeLitterMap A L = ConNF.fuzz ⋯ (π.completeAtomMap (h.path.B.cons ⋯) h.a)

A basic definition unfold.

source

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

π.completeLitterMap A L = (π A).flexibleCompletion A • L

A basic definition unfold.

source

theorem ConNF.StructApprox.toStructPerm_bot [ConNF.Params] :

⇑ConNF.Allowable.toStructPerm = ⇑ConNF.Tree.toBotIso.toMonoidHom

source

theorem ConNF.StructApprox.completeNearLitterMap_eq' [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) :

↑(π.completeNearLitterMap A N) = symmDiff (↑(π.completeNearLitterMap A N.fst.toNearLitter)) (π.completeAtomMap A '' symmDiff (ConNF.litterSet N.fst) ↑N)

source

theorem ConNF.StructApprox.completeNearLitterMap_toNearLitter_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) :

↑(π.completeNearLitterMap A L.toNearLitter) = ConNF.litterSet (π.completeLitterMap A L) \ (π A).atomPerm.domain ∪ π A • (ConNF.litterSet L ∩ (π A).atomPerm.domain)

source

theorem ConNF.StructApprox.eq_of_mem_completeNearLitterMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {A : ConNF.ExtendedIndex ↑β} (a : ConNF.Atom) (ha₁ : a ∈ π.completeNearLitterMap A L₁.toNearLitter) (ha₂ : a ∈ π.completeNearLitterMap A L₂.toNearLitter) :

π.completeLitterMap A L₁ = π.completeLitterMap A L₂

source

theorem ConNF.StructApprox.eq_of_completeLitterMap_inter_nonempty [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {π : ConNF.StructApprox ↑β} {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {A : ConNF.ExtendedIndex ↑β} (h : (↑(π.completeNearLitterMap A L₁.toNearLitter) ∩ ↑(π.completeNearLitterMap A L₂.toNearLitter)).Nonempty) :

π.completeLitterMap A L₁ = π.completeLitterMap A L₂