Power-of-two candidate/request/slot layouts

Independent powers of two flatten into one exact sorting-network capacity. Candidate identifiers are hardwired binary ranks and therefore injective.

def Algebraic.MassProduction.Nonuniform.PowerLayout.points (menuDepth requestDepth slotDepth : ℕ) : Fin (Sorting.networkRecords menuDepth) × Fin (Sorting.networkRecords requestDepth) × Fin (2 ^ slotDepth) ≃ Fin (Sorting.networkRecords (menuDepth + requestDepth + slotDepth))

A row-major triple of power-of-two indices is one sorting-network record.

Equations

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

noncomputable def Algebraic.MassProduction.Nonuniform.PowerLayout.codes (menuDepth : ℕ) (candidate : Fin (Sorting.networkRecords menuDepth)) : Fin menuDepth → Bool

Fixed candidate identifiers fit in exactly the menu sorting depth.

Equations

• Algebraic.MassProduction.Nonuniform.PowerLayout.codes menuDepth candidate = Algebraic.MassProduction.lexBitVectorAt (Fin.cast ⋯ candidate)

theorem Algebraic.MassProduction.Nonuniform.PowerLayout.codes_injective (menuDepth : ℕ) : Function.Injective (codes menuDepth)

The fixed candidate identifiers are distinct.