Recursion on addresses

In this file, we define fixed-point functions that allow us to construct the allowable permutation used in the freedom of action theorem by recursion on addresses.

Main declarations

• ConNF.HypAction: A data structure that contains the induced action of an approximation before a certain address (under the transitive closure of the Constrains relation).
• ConNF.HypAction.fixAtom, ConNF.HypAction.fixNearLitter: Fixed-point functions that allow us to compute the induced action of an approximation by recursion along (the transitive closure of) the Constrains relation.

structure ConNF.HypAction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (c : ConNF.Address ↑β) : Type u

The inductive hypothesis used to construct the induced action of an approximation in the freedom of action theorem.

• atomImage : (A : ConNF.ExtendedIndex ↑β) → (a : ConNF.Atom) → { path := A, value := Sum.inl a } < c → ConNF.Atom
• nearLitterImage : (A : ConNF.ExtendedIndex ↑β) → (N : ConNF.NearLitter) → { path := A, value := Sum.inr N } < c → ConNF.NearLitter

@[irreducible]

noncomputable def ConNF.HypAction.fixAtom [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (Fa : (A : ConNF.ExtendedIndex ↑β) → (a : ConNF.Atom) → ConNF.HypAction { path := A, value := Sum.inl a } → ConNF.Atom) (FN : (A : ConNF.ExtendedIndex ↑β) → (N : ConNF.NearLitter) → ConNF.HypAction { path := A, value := Sum.inr N } → ConNF.NearLitter) : ConNF.ExtendedIndex ↑β → ConNF.Atom → ConNF.Atom

Construct the fixed-point functions fixAtom and fixNearLitter. This is used to compute the induced action of an approximation on all atoms and near-litters.

Equations

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

@[irreducible]

noncomputable def ConNF.HypAction.fixNearLitter [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (Fa : (A : ConNF.ExtendedIndex ↑β) → (a : ConNF.Atom) → ConNF.HypAction { path := A, value := Sum.inl a } → ConNF.Atom) (FN : (A : ConNF.ExtendedIndex ↑β) → (N : ConNF.NearLitter) → ConNF.HypAction { path := A, value := Sum.inr N } → ConNF.NearLitter) : ConNF.ExtendedIndex ↑β → ConNF.NearLitter → ConNF.NearLitter

Construct the fixed-point functions fixAtom and fixNearLitter. This is used to compute the induced action of an approximation on all atoms and near-litters.

Equations

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

theorem ConNF.HypAction.fixAtom_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (Fa : (A : ConNF.ExtendedIndex ↑β) → (a : ConNF.Atom) → ConNF.HypAction { path := A, value := Sum.inl a } → ConNF.Atom) (FN : (A : ConNF.ExtendedIndex ↑β) → (N : ConNF.NearLitter) → ConNF.HypAction { path := A, value := Sum.inr N } → ConNF.NearLitter) (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom) : ConNF.HypAction.fixAtom Fa FN A a = Fa A a { atomImage := fun (B : ConNF.ExtendedIndex ↑β) (b : ConNF.Atom) (x : { path := B, value := Sum.inl b } < { path := A, value := Sum.inl a }) => ConNF.HypAction.fixAtom Fa FN B b, nearLitterImage := fun (B : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) (x : { path := B, value := Sum.inr N } < { path := A, value := Sum.inl a }) => ConNF.HypAction.fixNearLitter Fa FN B N }

theorem ConNF.HypAction.fixNearLitter_eq [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.FOAAssumptions] {β : ConNF.Λ} (Fa : (A : ConNF.ExtendedIndex ↑β) → (a : ConNF.Atom) → ConNF.HypAction { path := A, value := Sum.inl a } → ConNF.Atom) (FN : (A : ConNF.ExtendedIndex ↑β) → (N : ConNF.NearLitter) → ConNF.HypAction { path := A, value := Sum.inr N } → ConNF.NearLitter) (A : ConNF.ExtendedIndex ↑β) (N : ConNF.NearLitter) : ConNF.HypAction.fixNearLitter Fa FN A N = FN A N { atomImage := fun (B : ConNF.ExtendedIndex ↑β) (b : ConNF.Atom) (x : { path := B, value := Sum.inl b } < { path := A, value := Sum.inr N }) => ConNF.HypAction.fixAtom Fa FN B b, nearLitterImage := fun (B : ConNF.ExtendedIndex ↑β) (N_1 : ConNF.NearLitter) (x : { path := B, value := Sum.inr N_1 } < { path := A, value := Sum.inr N }) => ConNF.HypAction.fixNearLitter Fa FN B N_1 }