Bounded parameters for one uniform source-reduction family

The scale is the ceiling logarithm of the original input length plus one. The outer count is then a fixed power of a rounded input length. The Gamma candidate count is capped by the original input length plus one, ensuring polynomial-time enumeration on every input. The asymptotic theorem will show that this cap is eventually inactive.

def Algebraic.Cutwidth.Extractor.sourceReductionFamilyScale (n : ℕ) : ℕ

The scale shared by every component at input length n.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionFamilyScale n = Nat.clog 2 (n + 1)

def Algebraic.Cutwidth.Extractor.sourceReductionBoundedCandidates (n : ℕ) : ℕ

A uniformly bounded candidate count, agreeing eventually with the actual Gamma count.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionFamilyEval (source : List Bool) : List Bool

One total evaluator with all enumeration counts generated from the input length.

Equations

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

def Algebraic.Cutwidth.Extractor.sourceReductionFamily (n : ℕ) (x : Fin n → Bool) : Bool

The Boolean family computed by the bounded total evaluator.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionFamily n x = (Algebraic.Cutwidth.Extractor.sourceReductionFamilyEval (List.ofFn x)).headD false

def Algebraic.Cutwidth.Extractor.sourceReductionHardEval : List Bool → List Bool

Add a fresh XOR bit to balance the actual uniform evaluator.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionHardEval = Algebraic.Cutwidth.balancePadEval Algebraic.Cutwidth.Extractor.sourceReductionFamilyEval

def Algebraic.Cutwidth.Extractor.sourceReductionHardFamily (n : ℕ) (x : Fin n → Bool) : Bool

The single explicit family used for the coefficient-four circuit lower bound.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionHardFamily n x = (Algebraic.Cutwidth.Extractor.sourceReductionHardEval (List.ofFn x)).headD false

def Algebraic.Cutwidth.Extractor.sourceReductionHardLanguage : Complexity.Language

The language decided by the single balanced hard-family evaluator.

Equations

• Algebraic.Cutwidth.Extractor.sourceReductionHardLanguage = {source : List Bool | (Algebraic.Cutwidth.Extractor.sourceReductionHardEval source).headD false = true}