Universal menus for a punctured-line scheduling phase

An occupied state is described by at most capacity previously accepted lines and an ordered tuple of active targets. This is a finite description space, including repetitions. A single fixed menu simultaneously contains a half-clean candidate for every such state whenever the geometric packing budget holds.

The theorem is nonuniform: the menu depends on the dimensions and request counts, but is chosen before any occupied state or target tuple is supplied. This module proves the menu guarantee, not the cost of its circuit evaluator.

@[reducible, inline]

abbrev Algebraic.MassProduction.Nonuniform.PhaseState (Point : Type u_1) (Direction : Type u_2) (capacity active : ℕ) : Type (max (max u_1 u_2) u_1)

A bounded list of optional occupied lines together with ordered active targets. Empty slots permit every smaller occupied-line collection.

Equations

• Algebraic.MassProduction.Nonuniform.PhaseState Point Direction capacity active = ((Fin capacity → Option (Point × Direction)) × (Fin active → Point))

theorem Algebraic.MassProduction.Nonuniform.cardPhaseState_le {Point : Type u_1} {Direction : Type u_2} [Fintype Point] [Fintype Direction] (capacity active addressBits : ℕ) (activeLe : active ≤ capacity) (pointsSmall : Fintype.card Point ≤ 2 ^ addressBits) (directionsSmall : Fintype.card Direction ≤ 2 ^ addressBits) : Fintype.card (PhaseState Point Direction capacity active) ≤ 2 ^ (capacity * (1 + 3 * addressBits))

A phase state has at most capacity * (1 + 3 * addressBits) bits of information when points and directions each fit in addressBits bits.

noncomputable def Algebraic.MassProduction.Nonuniform.phaseOccupied {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] {capacity active : ℕ} (state : PhaseState V (Projectivization K V) capacity active) : Finset V

The actual occupied points described by the optional line slots.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.cardPhaseOccupied_le {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] {capacity active : ℕ} (state : PhaseState V (Projectivization K V) capacity active) : (phaseOccupied state).card ≤ capacity * (Nat.card K - 1)

A description with capacity slots occupies at most capacity * (|K| - 1) points. Overlaps only reduce this number.

def Algebraic.MassProduction.Nonuniform.HalfClean {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] {capacity active : ℕ} (state : PhaseState V (Projectivization K V) capacity active) (candidate : Fin active → Projectivization K V) : Prop

A candidate is successful if at least half of the active requests are clean, with rounding upward for an odd request count.

Equations

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

theorem Algebraic.MassProduction.Nonuniform.cardNotHalfCleanMulTwoPow_le {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] {capacity active : ℕ} [Fintype V] [Fintype (Projectivization K V)] (state : PhaseState V (Projectivization K V) capacity active) (activeLe : active ≤ capacity) (budget : 512 * capacity * Nat.card K ≤ Fintype.card (Projectivization K V)) : Nat.card { candidate : Fin active → Projectivization K V // ¬HalfClean state candidate } * 2 ^ active ≤ Fintype.card (Fin active → Projectivization K V)

Exact single-candidate failure bound under the geometric packing condition. Repeated targets and overlapping occupied descriptions are allowed.

theorem Algebraic.MassProduction.Nonuniform.existsUniversalPhaseMenu {K : Type u_1} {V : Type u_2} [Field K] [Finite K] [AddCommGroup V] [Module K V] [Fintype V] [Fintype (Projectivization K V)] [Nonempty (Projectivization K V)] (capacity active addressBits : ℕ) (activePositive : 0 < active) (activeLe : active ≤ capacity) (pointsSmall : Fintype.card V ≤ 2 ^ addressBits) (directionsSmall : Fintype.card (Projectivization K V) ≤ 2 ^ addressBits) (budget : 512 * capacity * Nat.card K ≤ Fintype.card (Projectivization K V)) : ∃ (menu : Fin (capacity * (1 + 3 * addressBits) / active + 1) → Fin active → Projectivization K V), ∀ (state : PhaseState V (Projectivization K V) capacity active), ∃ (entry : Fin (capacity * (1 + 3 * addressBits) / active + 1)), HalfClean state (menu entry)

Universal fixed menus of at most one plus description bits divided by the active request count. The existential quantifier is outside all states.

theorem Algebraic.MassProduction.Nonuniform.phaseMenuCandidateCount_le (capacity active addressBits : ℕ) (activeLe : active ≤ capacity) : (capacity * (1 + 3 * addressBits) / active + 1) * active ≤ capacity * (2 + 3 * addressBits)

Evaluating every menu entry examines a number of candidate lines linear in capacity, apart from the address-width factor.