Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.Extractor.Padding.Internal

Proofs for balanced padding #

Fixing the fresh coordinate loses at most a factor two in source support. The resulting padding has exact balance and preserves polynomial-time evaluation.

source
noncomputable def Algebraic.Cutwidth.Extractor.Internal.tailFiber {n : ℕ} (P : Finset (Fin (n + 1) → Bool)) (b : Bool) :
Finset (Fin n → Bool)

Tail strings in a fixed first-bit fibre of a source.

Equations
Instances For
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.card_tailFiber {n : ℕ} (P : Finset (Fin (n + 1) → Bool)) (b : Bool) :
    (tailFiber P b).card = {x ∈ P | x 0 = b}.card
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.card_tailFiber_add {n : ℕ} (P : Finset (Fin (n + 1) → Bool)) :
    (tailFiber P false).card + (tailFiber P true).card = P.card
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.exists_large_tailFiber {n K : ℕ} {P : Finset (Fin (n + 1) → Bool)} (hP : 2 * K ≤ P.card) :
    ∃ (b : Bool), K ≤ (tailFiber P b).card
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.exists_mem_of_mem_tailFiber {n : ℕ} {P : Finset (Fin (n + 1) → Bool)} {b : Bool} {x : Fin n → Bool} (hx : x ∈ tailFiber P b) :
    ∃ z ∈ P, z 0 = b ∧ Fin.tail z = x
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.rectangleFree_of_flatSumsetDisperser {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : FlatSumsetDisperser f K) :
    RectangleFree f K
    source
    theorem Algebraic.Cutwidth.Extractor.Internal.flatSumsetExtractor_disperser {n K : ℕ} {f : Cslib.BooleanFunction n} {ν : ℝ} (extract : FlatSumsetExtractor f K ν) (hK : 0 < K) (hν : ν < 1 / 2) :
    FlatSumsetDisperser f K

    Error strictly below one half guarantees both output values on every large flat-source pair.

    source
    theorem Algebraic.Cutwidth.Extractor.Internal.flatSumsetDisperser_balancePad {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : FlatSumsetDisperser f K) :
    FlatSumsetDisperser (balancePad f) (2 * K)

    A two-sided sumset disperser remains one after balanced padding, with a factor-two loss in support threshold.

    source
    theorem Algebraic.Cutwidth.Extractor.Internal.flatSumsetDisperser_rectangleFree {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : FlatSumsetDisperser f K) :
    RectangleFree f K

    Dispersion excludes one-rectangles, without any accepting-density assumption.

    source
    theorem Algebraic.Cutwidth.Extractor.Internal.flatSumsetExtractor_balancePad_rectangleFree {n K : ℕ} {f : Cslib.BooleanFunction n} {ν : ℝ} (extract : FlatSumsetExtractor f K ν) (hK : 0 < K) (hν : ν < 1 / 2) :
    RectangleFree (balancePad f) (2 * K)

    Any extraction error strictly below one half yields a rectangle-free balanced extension.

    source
    theorem Algebraic.Cutwidth.Extractor.Internal.card_accepting_balancePad {n : ℕ} (f : Cslib.BooleanFunction n) :
    (accepting (balancePad f)).card = 2 ^ n

    Exactly one fresh bit accepts for each old input, so balanced padding accepts exactly half its input cube.

    source
    theorem Algebraic.Cutwidth.Extractor.Internal.balancePadEval_toList {n : ℕ} {f : Cslib.BooleanFunction n} {eval : List Bool → List Bool} (heval : ∀ (x : Complexity.BitString n), eval x.toList = [f x]) (x : Complexity.BitString (n + 1)) :
    balancePadEval eval x.toList = [balancePad f x]

    The list evaluator agrees with the finite Boolean-function padding on every positive input length.

    source
    theorem Algebraic.Cutwidth.Extractor.Internal.balancePadEval_mem_FP {eval : List Bool → List Bool} (heval : eval ∈ Complexity.FP) :
    balancePadEval eval ∈ Complexity.FP

    Balanced padding preserves a uniform polynomial-time evaluator.