Punctured affine lines

A punctured line puncturedLine u v through the anchor u with a nonzero direction v has Fintype.card K - 1 points and omits u. A point y lies on it exactly when v is a nonzero multiple of y - u, so a point other than the anchor lies on the punctured lines of exactly Fintype.card K - 1 nonzero directions. Consequently a set B meets the punctured lines through u of at most #(B.erase u) * (Fintype.card K - 1) nonzero directions; in particular, an occupied anchor blocks nothing. A list of g lines occupies at most g * (Fintype.card K - 1) points. Cleanliness of a request (IsClean) is decidable.

Main results

• Cslib.LineCode.card_subtype_ne_zero: there are Fintype.card K ^ ℓ - 1 nonzero directions.
• Cslib.LineCode.card_puncturedLine: a punctured line has Fintype.card K - 1 points.
• Cslib.LineCode.notMem_puncturedLine_self: a punctured line omits its anchor.
• Cslib.LineCode.mem_puncturedLine_iff_exists_eq_smul: y is on the line of direction v iff v is a nonzero multiple of y - u.
• Cslib.LineCode.card_filter_mem_puncturedLine: a point other than the anchor lies on the lines of exactly Fintype.card K - 1 nonzero directions.
• Cslib.LineCode.card_filter_not_disjoint_puncturedLine_le: the blocking bound.
• Cslib.LineCode.disjoint_puncturedLine_iff: two punctured lines through one anchor are disjoint iff their directions are not proportional.
• Cslib.LineCode.card_occupiedPoints_le: g lines occupy at most g * (Fintype.card K - 1) points.

References

• Adapted, with nonzero vectors in place of projective directions, from MassProduction/Scheduler.lean and MassProduction/Nonuniform/PhaseMenu.lean in S. Schlesinger, Boolean circuit mass production formalization.

@[instance_reducible]

instance Cslib.LineCode.instDecidablePredFinIsClean {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ k : ℕ} (occupied : Finset (Fin ℓ → K)) (targets directions : Fin k → Fin ℓ → K) : DecidablePred (IsClean occupied targets directions)

Whether a request is clean is decidable.

theorem Cslib.LineCode.card_subtype_ne_zero {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} : Fintype.card { v : Fin ℓ → K // v ≠ 0 } = Fintype.card K ^ ℓ - 1

There are Fintype.card K ^ ℓ - 1 nonzero directions.

theorem Cslib.LineCode.mem_puncturedLine {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} {u v y : Fin ℓ → K} : y ∈ puncturedLine u v ↔ ∃ (c : K), c ≠ 0 ∧ u + c • v = y

Membership in a punctured line is witnessed by a nonzero scalar.

theorem Cslib.LineCode.card_puncturedLine_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} (u v : Fin ℓ → K) : (puncturedLine u v).card ≤ Fintype.card K - 1

A punctured line has at most Fintype.card K - 1 points, one for each nonzero scalar.

theorem Cslib.LineCode.card_puncturedLine {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} (u : Fin ℓ → K) {v : Fin ℓ → K} (hv : v ≠ 0) : (puncturedLine u v).card = Fintype.card K - 1

A punctured line with a nonzero direction has exactly Fintype.card K - 1 points.

theorem Cslib.LineCode.notMem_puncturedLine_self {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} (u : Fin ℓ → K) {v : Fin ℓ → K} (hv : v ≠ 0) : u ∉ puncturedLine u v

A punctured line with a nonzero direction omits its anchor.

theorem Cslib.LineCode.mem_puncturedLine_iff_exists_eq_smul {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} {u v y : Fin ℓ → K} : y ∈ puncturedLine u v ↔ ∃ (c : K), c ≠ 0 ∧ v = c • (y - u)

The point y lies on the punctured line through u with direction v iff v is a nonzero multiple of y - u.

theorem Cslib.LineCode.card_filter_mem_puncturedLine {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} {u y : Fin ℓ → K} (hy : y ≠ u) : {v ∈ Finset.univ.erase 0 | y ∈ puncturedLine u v}.card = Fintype.card K - 1

A point other than the anchor lies on the punctured lines of exactly Fintype.card K - 1 nonzero directions: the nonzero multiples of y - u.

theorem Cslib.LineCode.card_filter_not_disjoint_puncturedLine_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} (u : Fin ℓ → K) (B : Finset (Fin ℓ → K)) : {v ∈ Finset.univ.erase 0 | ¬Disjoint (puncturedLine u v) B}.card ≤ (B.erase u).card * (Fintype.card K - 1)

Blocking bound. A set B meets the punctured lines through u of at most #(B.erase u) * (Fintype.card K - 1) nonzero directions. The anchor u blocks nothing.

theorem Cslib.LineCode.disjoint_puncturedLine_iff {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ : ℕ} {u v w : Fin ℓ → K} : Disjoint (puncturedLine u v) (puncturedLine u w) ↔ ∀ (c : K), c ≠ 0 → v ≠ c • w

Two punctured lines through the same anchor are disjoint iff their directions are not proportional: v ≠ c • w for every nonzero c.

theorem Cslib.LineCode.card_occupiedPoints_le {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] {ℓ g : ℕ} (lines : Fin g → Option ((Fin ℓ → K) × (Fin ℓ → K))) : (occupiedPoints lines).card ≤ g * (Fintype.card K - 1)

A list of g lines occupies at most g * (Fintype.card K - 1) points.