Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.IrreducibleEncoding

Unrestricted depth-three lower bound: irreducible encoding #

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/IrreducibleEncoding.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.BinaryAlgebra.polynomialBits (P : Polynomial F2) (r : ℕ) :
Fin r → Bool

Encode the coefficients of a monic binary polynomial as bits.

Equations
Instances For
    source
    theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.inputPolynomialBits_polynomialBits (P : Polynomial F2) (hP : P.Monic) {r : ℕ} (hdegree : P.natDegree = r) :
    inputPolynomialBits (polynomialBits P r) = P
    source
    theorem Complexity.DepthThreeLowerBound.exists_irreducible_inputPolynomialBits (r : ℕ) (hr : 0 < r) :
    ∃ (p : Fin r → Bool), Irreducible (BinaryAlgebra.inputPolynomialBits p)