Witness assignments attaining the anchored lower bounds

def GenLimit.FiniteWitness.Anchored.low (k : ℕ) : Finset ℕ

The first half of the indices, rounded up.

Equations

• GenLimit.FiniteWitness.Anchored.low k = Finset.range ((k + 1) / 2)

def GenLimit.FiniteWitness.Anchored.high (k : ℕ) : Finset ℕ

The remaining indices below the row and column count.

Equations

• GenLimit.FiniteWitness.Anchored.high k = Finset.range k \ GenLimit.FiniteWitness.Anchored.low k

noncomputable def GenLimit.FiniteWitness.Anchored.rowWitness {k : ℕ} (i : Fin k) : Finset Point

Left-side anchor points assigned to a row.

Equations

• GenLimit.FiniteWitness.Anchored.rowWitness i = Finset.image Sum.inl (if ↑i < (k + 1) / 2 then GenLimit.FiniteWitness.Anchored.low k else GenLimit.FiniteWitness.Anchored.high k)

noncomputable def GenLimit.FiniteWitness.Anchored.colWitness {k : ℕ} (j : Fin k) : Finset Point

Right-side anchor points assigned to a column.

Equations

• GenLimit.FiniteWitness.Anchored.colWitness j = Finset.image Sum.inr (if ↑j < (k + 1) / 2 then GenLimit.FiniteWitness.Anchored.high k else GenLimit.FiniteWitness.Anchored.low k)

noncomputable def GenLimit.FiniteWitness.Anchored.upperAssignment {k : ℕ} (L : Set Point) : Finset Point

Assign the row or column witness of an anchored target, using the empty set off the family.

Equations

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

theorem GenLimit.FiniteWitness.Anchored.upper_left {k : ℕ} (i : Fin k) (D : Set ℕ) : upperAssignment (leftTarget i D) = rowWitness i

theorem GenLimit.FiniteWitness.Anchored.upper_right {k : ℕ} (j : Fin k) (E : Set ℕ) : upperAssignment (rightTarget j E) = colWitness j

theorem GenLimit.FiniteWitness.Anchored.upper_valid (k : ℕ) : Valid (family k) upperAssignment

theorem GenLimit.FiniteWitness.Anchored.upper_bound (k : ℕ) : HasBoundedWitnesses (family k) ((k + 1) / 2)

theorem GenLimit.FiniteWitness.Anchored.exact_width (k : ℕ) : separationWidth (family k) = finiteValue ((k + 1) / 2)

Every finite level, on the precise anchored family, including the empty k=0 case.

theorem GenLimit.FiniteWitness.Anchored.realizes_every_finite (d : ℕ) : separationWidth (family (2 * d)) = finiteValue d