Bounded enumeration of the actual sumset-extractor calls

The supplied unary counts bound both enumeration loops. Each position uses its concrete fixed-width binary code as a sampler index and in its advice. The actual sampler supplies the seed to the actual selected affine program on the same original source word. XOR within each outer coordinate and strict majority produce one final bit, including at zero counts.

The counts are runtime inputs rather than unrestricted powers generated from their bit widths. Agreement with the finite semantic construction uses separate exact-count hypotheses. Eventual bounds allowing those counts to be selected uniformly belong to the parameter-family layer.

def Algebraic.Cutwidth.Extractor.sourceReductionCallRuntime (L C : ℕ) (source : List Bool) (i z : ℕ) : Bool

One actual call at the two supplied binary enumeration indices.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionCandidatesRuntime (L C : ℕ) (source : List Bool) (i : ℕ) : List Bool

The candidate calls at one outer coordinate, in increasing binary-index order.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionCandidatesRuntime L C source i = List.map (Algebraic.Cutwidth.Extractor.sourceReductionCallRuntime L C source i) (List.range C)

def Algebraic.Cutwidth.Extractor.sourceReductionRowsRuntime (L N C : ℕ) (source : List Bool) : List Bool

XOR each actual candidate row, retaining outer-coordinate order.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionRuntime (L N C : ℕ) (source : List Bool) : List Bool

Strict majority of the actual XOR rows, always serialized as one Boolean bit.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionRuntime L N C source = Algebraic.Cutwidth.Extractor.majorityEval (Algebraic.Cutwidth.Extractor.sourceReductionRowsRuntime L N C source)

def Algebraic.Cutwidth.Extractor.sourceReductionEval (input : List Bool) : List Bool

Codec: pair source (pair scale (pair outerCount candidateCount)), unary parameters.

Equations

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