Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.LanguageBitHornerLoop

Unrestricted depth-three lower bound: language bit horner loop #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/LanguageBitHornerLoop.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

source
def Complexity.DepthThreeLowerBound.hornerStep (r : ℕ) (p h b a : List Bool) :
List Bool

One multiply-and-add step of Horner evaluation.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.hornerStep_length (r : ℕ) (p h b a : List Bool) (hb : b.length = r) :
    (hornerStep r p h b a).length = r
    source
    theorem Complexity.DepthThreeLowerBound.hornerStep_eq_word (r : ℕ) (p h b a : List Bool) (hb : b.length = r) :
    hornerStep r p h b a = wordList (wordXor (listWord r b) (wordMulMod (listWord r p) (listWord r h) (listWord r a)))
    source
    def Complexity.DepthThreeLowerBound.hornerFrom (r : ℕ) (p h : List Bool) (bs : List (List Bool)) (a : List Bool) :
    List Bool

    Continue Horner evaluation from an initial accumulator.

    Equations
    Instances For
      source
      @[simp]
      theorem Complexity.DepthThreeLowerBound.hornerFrom_nil (r : ℕ) (p h a : List Bool) :
      hornerFrom r p h [] a = a
      source
      theorem Complexity.DepthThreeLowerBound.hornerFrom_cons (r : ℕ) (p h b : List Bool) (bs : List (List Bool)) (a : List Bool) :
      hornerFrom r p h (b :: bs) a = hornerStep r p h b (hornerFrom r p h bs a)
      source
      theorem Complexity.DepthThreeLowerBound.hornerFrom_append (r : ℕ) (p h : List Bool) (bs cs : List (List Bool)) (a : List Bool) :
      hornerFrom r p h (bs ++ cs) a = hornerFrom r p h bs (hornerFrom r p h cs a)
      source
      theorem Complexity.DepthThreeLowerBound.hornerFrom_append_singleton (r : ℕ) (p h : List Bool) (bs : List (List Bool)) (b a : List Bool) :
      hornerFrom r p h (bs ++ [b]) a = hornerFrom r p h bs (hornerStep r p h b a)
      source
      theorem Complexity.DepthThreeLowerBound.hornerFrom_length (r : ℕ) (p h : List Bool) (bs : List (List Bool)) (a : List Bool) (ha : a.length = r) (hbs : ∀ b ∈ bs, b.length = r) :
      (hornerFrom r p h bs a).length = r
      source
      theorem Complexity.DepthThreeLowerBound.hornerFrom_zero_eq_hornerBitLists (r : ℕ) (p h : List Bool) (bs : List (List Bool)) (hbs : ∀ b ∈ bs, b.length = r) :
      hornerFrom r p h bs (List.replicate r false) = hornerBitLists r p h bs
      source
      theorem Complexity.DepthThreeLowerBound.block_flatten_length {α : Type uDepth1} (r : ℕ) (bs : List (List α)) (hbs : ∀ b ∈ bs, b.length = r) :
      bs.flatten.length = bs.length * r