Documentation

Complexitylib.Algebraic.MassProduction.Nonuniform.GeometricPhaseOutput

Output contract for a geometric phase #

One candidate and one permutation witness the output: all original request data and complete line-point lists are preserved, and every accepted prefix request is clean with respect to the original occupied set.

source
def Algebraic.MassProduction.Nonuniform.GeometricPhase.CorrectOutput {width menuDepth requestDepth dimension requestWidth : ℕ} (positive : 0 < width) (menu : Fin (Sorting.networkRecords menuDepth) → Fin (Sorting.networkRecords requestDepth) → Projectivization (BinaryExtension width) (Fin dimension → BinaryExtension width)) (original : Fin (Sorting.networkRecords requestDepth) → Fin requestWidth → Bool) (targets : Fin (Sorting.networkRecords requestDepth) → Fin dimension → BinaryExtension width) (occupied : Finset (Fin dimension → BinaryExtension width)) (needed : ℕ) (output : Fin (Sorting.networkBits requestDepth (1 + (requestWidth + 2 ^ width * (dimension * width)))) → Bool) :
Prop

Full semantic output contract used when composing halving phases.

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