Surjectivity from a flip

A sentence can say that a guessed family of sets contains the empty set and is closed under flipping a single element, and it can say that the guess is injective. It cannot say that the guess is onto: quantifying over all sets is second order, and a first-order kernel over an extended universe has no way to reach them.

This file is what buys surjectivity anyway, and it is a counting argument in Lean rather than a condition in the logic. A family containing the empty set and closed under one-element flips is everything (DescriptiveComplexity.eq_of_flipClosed), because every finite set is reached from the empty one by flipping its elements in one at a time; so an injective guess into it is a bijection (DescriptiveComplexity.bijective_of_flipClosed, and its set-valued reading DescriptiveComplexity.bijective_of_flipClosedP).

That is the shape the exponential rung of value invention needs: invent exponentially many is not a condition a sentence states, it is a bound the definition carries, and this is where the bound is spent.

def DescriptiveComplexity.flipAt {α : Type} [DecidableEq α] (T : Finset α) (a : α) : Finset α

Flipping one element of a finite set: in if it was out, out if it was in.

Equations

• DescriptiveComplexity.flipAt T a = if a ∈ T then T.erase a else insert a T

theorem DescriptiveComplexity.flipAt_of_notMem {α : Type} [DecidableEq α] {T : Finset α} {a : α} (ha : a ∉ T) : flipAt T a = insert a T

theorem DescriptiveComplexity.eq_of_flipClosed {α : Type} [DecidableEq α] {S : Finset α → Prop} (h0 : S ∅) (hflip : ∀ (T : Finset α) (a : α), S T → S (flipAt T a)) (T : Finset α) : S T

A family containing the empty set and closed under one-element flips is everything: every finite set is reached from the empty one by flipping its elements in, one at a time.

theorem DescriptiveComplexity.bijective_of_flipClosed {α ι : Type} [DecidableEq α] (f : ι → Finset α) (hinj : Function.Injective f) (h0 : ∃ (i : ι), f i = ∅) (hflip : ∀ (i : ι) (a : α), ∃ (j : ι), f j = flipAt (f i) a) : Function.Bijective f

An injective guess into a flip-closed family is a bijection: the family is everything, so an injection into it is onto.

The same, read at set-valued guesses

noncomputable def DescriptiveComplexity.toFinsetOf {α ι : Type} [Fintype α] (f : ι → α → Prop) (i : ι) : Finset α

The family a guess names, as finite sets.

Equations

• DescriptiveComplexity.toFinsetOf f i = Finset.filter (f i) Finset.univ

theorem DescriptiveComplexity.mem_toFinsetOf {α ι : Type} [Fintype α] (f : ι → α → Prop) (i : ι) (x : α) : x ∈ toFinsetOf f i ↔ f i x

theorem DescriptiveComplexity.bijective_of_flipClosedP {α ι : Type} [Finite α] (f : ι → α → Prop) (hinj : Function.Injective f) (h0 : ∃ (i : ι), ∀ (x : α), ¬f i x) (hflip : ∀ (i : ι) (a : α), ∃ (j : ι), ∀ (x : α), f j x ↔ Xor (f i x) (x = a)) : Function.Bijective f

An injective set-valued guess, flip-closed, is a bijection. This is the form a guessed meaning relation takes: one set of α per invented value.