Documentation

Complexitylib.Circuits.DepthThree.LowerBound.Internal.AlgebraBits

Unrestricted depth-three lower bound: algebra bits #

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

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

source
@[reducible, inline]
abbrev Complexity.DepthThreeLowerBound.BinaryAlgebra.F2 :
Type

The two-element field.

Equations
Instances For
    source
    def Complexity.DepthThreeLowerBound.BinaryAlgebra.boolEquivF2 :
    Bool ≃ F2

    Identify Boolean bits with the two elements of the field.

    Equations
    Instances For
      source
      def Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue (b : Bool) :
      F2

      View a Boolean bit as an element of the two-element field.

      Equations
      Instances For
        source
        def Complexity.DepthThreeLowerBound.BinaryAlgebra.fieldBit (a : F2) :
        Bool

        Read an element of the two-element field as a Boolean bit.

        Equations
        Instances For
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_false :
          bitValue false = 0
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_true :
          bitValue true = 1
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.fieldBit_zero :
          fieldBit 0 = false
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.fieldBit_one :
          fieldBit 1 = true
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.fieldBit_bitValue (b : Bool) :
          fieldBit (bitValue b) = b
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_fieldBit (a : F2) :
          bitValue (fieldBit a) = a
          source
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_injective :
          Function.Injective bitValue
          source
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_surjective :
          Function.Surjective bitValue
          source
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_xor (a b : Bool) :
          bitValue (a ^^ b) = bitValue a + bitValue b
          source
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_and (a b : Bool) :
          bitValue (a && b) = bitValue a * bitValue b
          source
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_not (a : Bool) :
          (bitValue !a) = 1 + bitValue a
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_eq_zero_iff (b : Bool) :
          bitValue b = 0 ↔ b = false
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitValue_eq_one_iff (b : Bool) :
          bitValue b = 1 ↔ b = true
          source
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.eq_zero_or_one (a : F2) :
          a = 0 ∨ a = 1
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.fieldBit_eq_false_iff (a : F2) :
          fieldBit a = false ↔ a = 0
          source
          @[simp]
          theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.fieldBit_eq_true_iff (a : F2) :
          fieldBit a = true ↔ a = 1
          source
          def Complexity.DepthThreeLowerBound.BinaryAlgebra.bitsEquivF2 (V : Type uDepth1) :
          (V → Bool) ≃ (V → F2)

          Coordinatewise identification of bit vectors with field vectors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitsEquivF2_apply (V : Type uDepth2) (x : V → Bool) (i : V) :
            (bitsEquivF2 V) x i = bitValue (x i)
            source
            @[simp]
            theorem Complexity.DepthThreeLowerBound.BinaryAlgebra.bitsEquivF2_symm_apply (V : Type uDepth3) (x : V → F2) (i : V) :
            (bitsEquivF2 V).symm x i = fieldBit (x i)