Universal phase menus with power-of-two length

Repeat the first candidate in the unused suffix of the next power-of-two menu. Coverage is preserved, and the number of evaluated candidate lines increases by a factor of at most two.

def Algebraic.MassProduction.Nonuniform.padMenu {length : ℕ} {Choice : Sort u_1} {paddedLength : ℕ} (menu : Fin length → Choice) (positive : 0 < length) (_fits : length ≤ paddedLength) (index : Fin paddedLength) : Choice

Extend a nonempty fixed menu by repeating its first entry.

Equations

• Algebraic.MassProduction.Nonuniform.padMenu menu positive _fits index = if before : ↑index < length then menu ⟨↑index, before⟩ else menu ⟨0, positive⟩

theorem Algebraic.MassProduction.Nonuniform.padMenu_original {length : ℕ} {Choice : Sort u_1} {paddedLength : ℕ} (menu : Fin length → Choice) (positive : 0 < length) (fits : length ≤ paddedLength) (index : Fin length) : padMenu menu positive fits (Fin.castLE fits index) = menu index

Every original entry survives padding at the same position.

theorem Algebraic.MassProduction.Nonuniform.padMenu_covers {State : Type u_1} {Choice : Type u_2} {length paddedLength : ℕ} (good : State → Choice → Prop) (menu : Fin length → Choice) (positive : 0 < length) (fits : length ≤ paddedLength) (covers : Covers good menu) : Covers good (padMenu menu positive fits)

Padding a covering menu preserves universal coverage.

def Algebraic.MassProduction.Nonuniform.phaseMenuDepth (capacity active addressBits : ℕ) : ℕ

Power-of-two depth for the universal menu at one phase.

Equations

• Algebraic.MassProduction.Nonuniform.phaseMenuDepth capacity active addressBits = Algebraic.MassProduction.FiniteParameters.binaryDepth (capacity * (1 + 3 * addressBits) / active + 1)

theorem Algebraic.MassProduction.Nonuniform.existsUniversalPowerPhaseMenu {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 (Sorting.networkRecords (phaseMenuDepth capacity active addressBits)) → Fin active → Projectivization K V), ∀ (state : PhaseState V (Projectivization K V) capacity active), ∃ (entry : Fin (Sorting.networkRecords (phaseMenuDepth capacity active addressBits))), HalfClean state (menu entry)

The power-of-two menu still covers every geometric phase state.

theorem Algebraic.MassProduction.Nonuniform.powerPhaseMenuCandidateCount_le (capacity active addressBits : ℕ) (activeLe : active ≤ capacity) : Sorting.networkRecords (phaseMenuDepth capacity active addressBits) * active ≤ 2 * (capacity * (2 + 3 * addressBits))

Padding adds at most a factor of two to the linear candidate-line bound.