def ConNF.StructApprox.FOAIh [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] : Prop

The inductive hypothesis used for proving freedom of action: Every free approximation exactly approximates some allowable permutation.

Equations

• ConNF.StructApprox.FOAIh β = ∀ (π₀ : ConNF.StructApprox ↑β), π₀.Free → ∃ (π : ConNF.Allowable ↑β), π₀.ExactlyApproximates (ConNF.Allowable.toStructPerm π)

class ConNF.StructApprox.FreedomOfActionHypothesis [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] : Prop

• freedomOfAction_of_lt : ∀ γ < β, ∀ [inst : ConNF.LeLevel ↑γ], ConNF.StructApprox.FOAIh γ

theorem ConNF.StructApprox.FreedomOfActionHypothesis.freedomOfAction_of_lt [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [self : ConNF.StructApprox.FreedomOfActionHypothesis β] (γ : ConNF.Λ) : γ < β → ∀ [inst : ConNF.LeLevel ↑γ], ConNF.StructApprox.FOAIh γ

def ConNF.StructApprox.ihAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} (H : ConNF.HypAction c) : ConNF.StructLAction ↑β

The structural action associated to a given inductive hypothesis.

Equations

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

@[simp]

theorem ConNF.StructApprox.ihAction_atomMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {H : ConNF.HypAction c} {B : ConNF.ExtendedIndex ↑β} {a : ConNF.Atom} : (ConNF.StructApprox.ihAction H B).atomMap a = { Dom := { path := B, value := Sum.inl a } < c, get := fun (h : { path := B, value := Sum.inl a } < c) => H.atomImage B a h }

@[simp]

theorem ConNF.StructApprox.ihAction_litterMap [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} {c : ConNF.Address ↑β} {H : ConNF.HypAction c} {B : ConNF.ExtendedIndex ↑β} {L : ConNF.Litter} : (ConNF.StructApprox.ihAction H B).litterMap L = { Dom := { path := B, value := Sum.inr L.toNearLitter } < c, get := fun (h : { path := B, value := Sum.inr L.toNearLitter } < c) => H.nearLitterImage B L.toNearLitter h }

noncomputable def ConNF.StructLAction.allowable [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] (φ : ConNF.StructLAction ↑γ) (h : γ < β) (h₁ : φ.Lawful) (h₂ : φ.MapFlexible) : ConNF.Allowable ↑γ

Equations

• φ.allowable h h₁ h₂ = ⋯.choose

theorem ConNF.StructLAction.allowable_exactlyApproximates [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] {γ : ConNF.Λ} [ConNF.LtLevel ↑γ] (φ : ConNF.StructLAction ↑γ) (h : γ < β) (h₁ : φ.Lawful) (h₂ : φ.MapFlexible) : (φ.toApprox h₁).ExactlyApproximates (ConNF.Allowable.toStructPerm (φ.allowable h h₁ h₂))

noncomputable def ConNF.StructLAction.hypothesisedAllowable [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (φ : ConNF.StructLAction ↑β) {A : ConNF.ExtendedIndex ↑β} (h : ConNF.InflexibleCoePath A) (h₁ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (h.B.cons ⋯) φ)) (h₂ : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp (h.B.cons ⋯) φ)) : ConNF.Allowable ↑h.δ

Equations

• φ.hypothesisedAllowable h h₁ h₂ = ConNF.StructLAction.allowable (ConNF.Tree.comp (h.B.cons ⋯) φ) ⋯ h₁ h₂

theorem ConNF.StructLAction.hypothesisedAllowable_exactlyApproximates [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (φ : ConNF.StructLAction ↑β) {A : ConNF.ExtendedIndex ↑β} (h : ConNF.InflexibleCoePath A) (h₁ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (h.B.cons ⋯) φ)) (h₂ : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp (h.B.cons ⋯) φ)) : (ConNF.StructLAction.toApprox (ConNF.Tree.comp (h.B.cons ⋯) φ) h₁).ExactlyApproximates (ConNF.Allowable.toStructPerm (φ.hypothesisedAllowable h h₁ h₂))

noncomputable def ConNF.StructApprox.litterCompletion [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] [ConNF.StructApprox.FreedomOfActionHypothesis β] (π : ConNF.StructApprox ↑β) (A : ConNF.ExtendedIndex ↑β) (L : ConNF.Litter) (H : ConNF.HypAction { path := A, value := Sum.inr L.toNearLitter }) : ConNF.Litter

Equations

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

theorem ConNF.StructApprox.litterCompletion_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.HypAction { path := A, value := Sum.inr L.toNearLitter }) (hflex : ConNF.Flexible A L) : π.litterCompletion A L H = (π A).flexibleCompletion A • L

theorem ConNF.StructApprox.litterCompletion_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.HypAction { path := A, value := Sum.inr L.toNearLitter }) (h : ConNF.InflexibleCoe A L) : π.litterCompletion A L H = if h' : ConNF.StructLAction.Lawful (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction H)) ∧ ConNF.StructLAction.MapFlexible (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction H)) then ConNF.fuzz ⋯ ((ConNF.StructApprox.ihAction H).hypothesisedAllowable h.path ⋯ ⋯ • h.t) else L

theorem ConNF.StructApprox.litterCompletion_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.HypAction { path := A, value := Sum.inr L.toNearLitter }) (h : ConNF.InflexibleCoe A L) (h₁ : ConNF.StructLAction.Lawful (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction H))) (h₂ : ConNF.StructLAction.MapFlexible (ConNF.Tree.comp (h.path.B.cons ⋯) (ConNF.StructApprox.ihAction H))) : π.litterCompletion A L H = ConNF.fuzz ⋯ ((ConNF.StructApprox.ihAction H).hypothesisedAllowable h.path h₁ h₂ • h.t)

theorem ConNF.StructApprox.litterCompletion_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.HypAction { path := A, value := Sum.inr L.toNearLitter }) (h : ConNF.InflexibleBot A L) : π.litterCompletion A L H = ConNF.fuzz ⋯ (H.atomImage (h.path.B.cons ⋯) h.a ⋯)