Near-litters

In this file, we define near-litters. A near-litter is a set of atoms that is near some litter set. Large families of near-litters will be used to obscure certain information from the model.

Since there is exactly one litter near a given near-litter, we will store this litter as extra data, which helps improve some definitional equalities.

Definition and basic results

structure ConNF.NearLitter [ConNF.Params] : Type u

A near-litter consists of a litter, a set of atoms, and a proof that those atoms are near the litter set of that litter.

• litter : ConNF.Litter
• atoms : Set ConNF.Atom
• atoms_near_litter' : self.atoms ~ self.litterᴬ

instance ConNF.instSuperLNearLitterLitter [ConNF.Params] : ConNF.SuperL ConNF.NearLitter ConNF.Litter

We write Nᴸ for the litter associated to a near-litter N.

Equations

• ConNF.instSuperLNearLitterLitter = { superL := fun (N : ConNF.NearLitter) => N.litter }

instance ConNF.instSuperANearLitterSetAtom [ConNF.Params] : ConNF.SuperA ConNF.NearLitter (Set ConNF.Atom)

We write Nᴬ for the set of atoms associated to a near-litter N.

Equations

• ConNF.instSuperANearLitterSetAtom = { superA := fun (N : ConNF.NearLitter) => N.atoms }

instance ConNF.instSuperNLitterNearLitter [ConNF.Params] : ConNF.SuperN ConNF.Litter ConNF.NearLitter

We write Lᴺ for the near-litter whose atoms are precisely the litter set of a litter L.

Equations

• ConNF.instSuperNLitterNearLitter = { superN := fun (L : ConNF.Litter) => { litter := L, atoms := Lᴬ, atoms_near_litter' := ⋯ } }

@[simp]

theorem ConNF.NearLitter.mk_litter [ConNF.Params] (L : ConNF.Litter) (s : Set ConNF.Atom) (h : s ~ Lᴬ) : { litter := L, atoms := s, atoms_near_litter' := h }ᴸ = L

A definitional simplification lemma for the ᴸ notation.

@[simp]

theorem ConNF.NearLitter.mk_atoms [ConNF.Params] (L : ConNF.Litter) (s : Set ConNF.Atom) (h : s ~ Lᴬ) : { litter := L, atoms := s, atoms_near_litter' := h }ᴬ = s

A definitional simplification lemma for the ᴬ notation.

theorem ConNF.NearLitter.atoms_near_litter [ConNF.Params] (N : ConNF.NearLitter) : Nᴬ ~ Nᴸᴬ

The set of atoms of a near-litter N is near the litter set of its associated litter.

theorem ConNF.NearLitter.symmDiff_small [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Small (symmDiff Nᴬ Nᴸᴬ)

theorem ConNF.NearLitter.diff_small [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Small (Nᴬ \ Nᴸᴬ)

theorem ConNF.NearLitter.diff_small' [ConNF.Params] (N : ConNF.NearLitter) : ConNF.Small (Nᴸᴬ \ Nᴬ)

theorem ConNF.NearLitter.card_atoms [ConNF.Params] (N : ConNF.NearLitter) : Cardinal.mk ↑Nᴬ = Cardinal.mk ConNF.κ

There are precisely κ-many atoms in each near-litter.

theorem ConNF.NearLitter.atoms_not_small [ConNF.Params] (N : ConNF.NearLitter) : ¬ConNF.Small Nᴬ

theorem ConNF.nearLitter_litter_eq_of_near [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴬ ~ N₂ᴬ) : N₁ᴸ = N₂ᴸ

theorem ConNF.near_of_litter_eq [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ = N₂ᴸ) : N₁ᴬ ~ N₂ᴬ

@[simp]

theorem ConNF.nearLitter_near_iff [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : N₁ᴬ ~ N₂ᴬ ↔ N₁ᴸ = N₂ᴸ

Near-litters are near (treated as sets of atoms) precisely if they are near the same litter.

theorem ConNF.NearLitter.ext [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴬ = N₂ᴬ) : N₁ = N₂

The extensionality principle for near-litters: if two near-litters contain the same atoms, they are the same. This proves that the data of the litter near a given near-litter is redundant, but as mentioned, its presence helps with certain definitional equalities.

theorem ConNF.card_near_litter [ConNF.Params] (L : ConNF.Litter) : Cardinal.mk ↑{s : Set ConNF.Atom | s ~ Lᴬ} = Cardinal.mk ConNF.μ

There are #μ sets of atoms near a given litter set.

def ConNF.nearLitterEquiv [ConNF.Params] : ConNF.NearLitter ≃ (L : ConNF.Litter) × ↑{s : Set ConNF.Atom | s ~ Lᴬ}

Strips away the name of the type of near-litters, converting it into a combination of types well-known to mathlib.

Equations

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

@[simp]

theorem ConNF.card_nearLitter [ConNF.Params] : Cardinal.mk ConNF.NearLitter = Cardinal.mk ConNF.μ

There are exactly #μ near-litters.

Interference of near-litters

Later, we will prove some combinatorial results that relate to the ways that different near-litters interact under certain permutations of our atoms. More precisely, we will need to calculate where the images of atoms under a permutation can lie, given that we know the pointwise image of the permutation on some near-litters. If we know the pointwise images of two near-litters under a permutation of atoms, we know that (for example) atoms in the intersection of the two near-litters must be mapped to the intersection of the pointwise images, and the same holds for other operations on sets such as the symmetric difference.

This motivates the following definition: the interference of two near-litters N₁ and N₂ is either their intersection or their symmetric difference, whichever is small. Note that precisely one of these two sets will always be small. This is the set of atoms that is most tightly controlled by the images of N₁ and N₂ under a permutation of atoms: an atom that was in the interference of N₁ and N₂ must remain in the intersection or symmetric difference of their images, which will still be a small set.

This definition will remain unused for quite some time; we will next revisit the interference of near-litters when we begin to prove the freedom of action theorem.

theorem ConNF.litter_eq_iff_symmDiff_small [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : N₁ᴸ = N₂ᴸ ↔ ConNF.Small (symmDiff N₁ᴬ N₂ᴬ)

theorem ConNF.litter_ne_of_inter_small [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : ConNF.Small (N₁ᴬ ∩ N₂ᴬ)) : N₁ᴸ ≠ N₂ᴸ

theorem ConNF.inter_small_of_litter_ne [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ ≠ N₂ᴸ) : ConNF.Small (N₁ᴬ ∩ N₂ᴬ)

theorem ConNF.litter_ne_iff_inter_small [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : N₁ᴸ ≠ N₂ᴸ ↔ ConNF.Small (N₁ᴬ ∩ N₂ᴬ)

def ConNF.interference [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : Set ConNF.Atom

The interference of two near-litters N₁ and N₂ is their intersection if N₁ and N₂ are near different litters, and their symmetric difference if N₁ and N₂ are near the same litter. This will always be a small set.

Equations

• ConNF.interference N₁ N₂ = {a : ConNF.Atom | N₁ᴸ = N₂ᴸ ↔ ¬(a ∈ N₁ᴬ ↔ a ∈ N₂ᴬ)} ∩ (N₁ᴬ ∪ N₂ᴬ)

theorem ConNF.interference_eq_of_litter_eq [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ = N₂ᴸ) : ConNF.interference N₁ N₂ = symmDiff N₁ᴬ N₂ᴬ

theorem ConNF.interference_eq_of_litter_ne [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} (h : N₁ᴸ ≠ N₂ᴸ) : ConNF.interference N₁ N₂ = N₁ᴬ ∩ N₂ᴬ

theorem ConNF.interference_small [ConNF.Params] (N₁ N₂ : ConNF.NearLitter) : ConNF.Small (ConNF.interference N₁ N₂)