Affine-line recovery scheduling

This file proves the combinatorial scheduler used in the Boolean mass-production manuscript. A recovery direction is projective, so each previously used point forbids at most one direction. Greedy counting therefore gives pairwise-disjoint punctured affine lines whenever the used point budget is smaller than projective direction space.

This is an existence theorem. It does not yet claim the manuscript's circuit cost for computing the schedule; that requires a separate concrete routing construction. Public scheduler data requires only Finite fields and states cardinalities with Nat.card; concrete enumerations remain implementation details.

noncomputable def Algebraic.MassProduction.puncturedLine {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] (target : V) (direction : Projectivization K V) : Finset V

All non-center points on the affine line through target in a projective direction.

Equations

• Algebraic.MassProduction.puncturedLine target direction = Finset.image (fun (scalar : K) => target + scalar • direction.rep) (Finset.univ.erase 0)

noncomputable def Algebraic.MassProduction.recoverySets {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] : List V → List (Projectivization K V) → List (Finset V)

Recovery sets obtained by pairing targets and directions in list order. An unmatched suffix of either list is ignored.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.MassProduction.recoverySets x✝¹ x✝ = []

def Algebraic.MassProduction.ValidSchedule {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] (targets : List V) (directions : List (Projectivization K V)) : Prop

A schedule assigns one direction per target and uses pairwise-disjoint recovery sets.

Equations

• Algebraic.MassProduction.ValidSchedule targets directions = (directions.length = targets.length ∧ List.Pairwise Disjoint (Algebraic.MassProduction.recoverySets targets directions))

theorem Algebraic.MassProduction.card_projectiveDirections (K : Type u_1) [Field K] [Finite K] (dimension : ℕ) : Nat.card (Projectivization K (Fin dimension → K)) = ∑ exponent ∈ Finset.range dimension, Nat.card K ^ exponent

Exact geometric-sum cardinality of projective direction space.

theorem Algebraic.MassProduction.card_projectiveDirections_div (K : Type u_1) [Field K] [Finite K] (dimension : ℕ) : Nat.card (Projectivization K (Fin dimension → K)) = (Nat.card K ^ dimension - 1) / (Nat.card K - 1)

Quotient form of the projective direction count.

theorem Algebraic.MassProduction.memPuncturedLine_iff {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] (target : V) (direction : Projectivization K V) (point : V) : point ∈ puncturedLine target direction ↔ ∃ (scalar : K), scalar ≠ 0 ∧ target + scalar • direction.rep = point

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

theorem Algebraic.MassProduction.card_puncturedLine {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] (target : V) (direction : Projectivization K V) : (puncturedLine target direction).card = Nat.card K - 1

A punctured affine line has one point per nonzero field scalar.

theorem Algebraic.MassProduction.target_not_mem_puncturedLine {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] (target : V) (direction : Projectivization K V) : target ∉ puncturedLine target direction

The center is not in its punctured affine line.

theorem Algebraic.MassProduction.sum_puncturedLine {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Fintype K] [DecidableEq K] {A : Type u_3} [AddCommMonoid A] (target : V) (direction : Projectivization K V) (function : V → A) : ∑ point ∈ puncturedLine target direction, function point = ∑ scalar ∈ Finset.univ.erase 0, function (target + scalar • direction.rep)

Summing over a punctured line is the same as summing over its nonzero parameters.

theorem Algebraic.MassProduction.puncturedLine_mk_eq_image {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Fintype K] [DecidableEq K] [DecidableEq V] (target vector : V) (vectorNonzero : vector ≠ 0) : puncturedLine target (Projectivization.mk K vector vectorNonzero) = Finset.image (fun (scalar : K) => target + scalar • vector) (Finset.univ.erase 0)

A punctured projective line can be enumerated using any chosen nonzero representative of its direction. This removes any dependence on the arbitrary representative selected by Projectivization.rep.

theorem Algebraic.MassProduction.puncturedLine_disjoint_of_avoids_differences {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] (target : V) (direction : Projectivization K V) (used : Finset V) (avoids : ∀ point ∈ used, ∀ (pointDifferent : point ≠ target), direction ≠ Projectivization.mk K (point - target) ⋯) : Disjoint (puncturedLine target direction) used

A direction whose projective class differs from every nonzero point - target direction yields a punctured line disjoint from the used points. This is the pointwise form consumed by the constructive scheduler circuit.

theorem Algebraic.MassProduction.cardIntersectingDirections_le {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] [Finite V] (target : V) (used : Finset V) : Nat.card { direction : Projectivization K V // ¬Disjoint (puncturedLine target direction) used } ≤ used.card

Each occupied point blocks at most one projective direction. This is the counting form used when a direction is sampled uniformly.

theorem Algebraic.MassProduction.exists_puncturedLine_disjoint {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Finite K] [Finite V] (target : V) (used : Finset V) (cardBound : used.card < Nat.card (Projectivization K V)) : ∃ (direction : Projectivization K V), Disjoint (puncturedLine target direction) used

If fewer points are used than there are projective directions, some punctured line through a new target avoids the used set.

theorem Algebraic.MassProduction.exists_validSchedule {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] [Finite V] (targets : List V) (cardBound : targets.length * (Nat.card K - 1) < Nat.card (Projectivization K V)) : ∃ (directions : List (Projectivization K V)), ValidSchedule targets directions

Every request list has pairwise-disjoint punctured-line recovery sets when its exact point budget is smaller than projective direction space.

theorem Algebraic.MassProduction.exists_validSchedule_of_mul_card_lt {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] [Finite V] (targets : List V) (cardBound : targets.length * Nat.card K < Nat.card (Projectivization K V)) : ∃ (directions : List (Projectivization K V)), ValidSchedule targets directions

The paper's simpler requests * |K| condition implies the exact recovery-set budget condition.