theorem CryptBoolean.quadraticPolarKernel_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel f a
      b =
    f (a + b) + f a + f b + f 0

theorem CryptBoolean.quadraticPolarKernel_comm
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel f a
      b =
    CryptBoolean.quadraticPolarKernel f b
      a

theorem CryptBoolean.quadraticPolarKernel_eq_dotProduct_of_derivative_eq_affine
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a b : FABL.F₂Cube n) (d : FABL.𝔽₂)
  (u : FABL.F₂Cube n)
  (hderivative :
    FABL.booleanDerivative f a =
      FABL.affineFunction d u) :
  CryptBoolean.quadraticPolarKernel f a
      b =
    FABL.f₂DotProduct u b

theorem CryptBoolean.quadraticPolarKernel_add_right
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (a b c : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel f a
      (b + c) =
    CryptBoolean.quadraticPolarKernel f a
        b +
      CryptBoolean.quadraticPolarKernel f
        a c

theorem CryptBoolean.quadraticPolarKernel_smul_right
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (a b : FABL.F₂Cube n) (c : FABL.𝔽₂) :
  CryptBoolean.quadraticPolarKernel f a
      (c • b) =
    c •
      CryptBoolean.quadraticPolarKernel f
        a b

theorem CryptBoolean.quadraticPolarKernel_add_left
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (a b c : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel f
      (a + b) c =
    CryptBoolean.quadraticPolarKernel f a
        c +
      CryptBoolean.quadraticPolarKernel f
        b c

theorem CryptBoolean.quadraticPolarKernel_smul_left
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (a b : FABL.F₂Cube n) (c : FABL.𝔽₂) :
  CryptBoolean.quadraticPolarKernel f
      (c • a) b =
    c •
      CryptBoolean.quadraticPolarKernel f
        a b

theorem CryptBoolean.quadraticPolar_apply {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (a b : FABL.F₂Cube n) :
  ((CryptBoolean.quadraticPolar f hdegree)
        a)
      b =
    CryptBoolean.quadraticPolarKernel f a
      b

theorem CryptBoolean.quadraticPolar_isSymm {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  (CryptBoolean.quadraticPolar f
      hdegree).IsSymm

theorem CryptBoolean.quadraticPolar_isAlt {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  (CryptBoolean.quadraticPolar f
      hdegree).IsAlt

theorem CryptBoolean.mem_quadraticRadical_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (a : FABL.F₂Cube n) :
  a ∈
      CryptBoolean.quadraticRadical f
        hdegree ↔
    ∀ (b : FABL.F₂Cube n),
      CryptBoolean.quadraticPolarKernel f
          a b =
        0

theorem CryptBoolean.booleanDerivative_eq_const_of_mem_quadraticRadical
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (a : FABL.F₂Cube n)
  (ha :
    a ∈
      CryptBoolean.quadraticRadical f
        hdegree) :
  FABL.booleanDerivative f a = fun x =>
    f a + f 0

theorem CryptBoolean.quadraticRadical_eq_linearKernel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.quadraticRadical f
      hdegree =
    CryptBoolean.linearKernel f

theorem CryptBoolean.walshTransform_zero_sq_eq_two_pow_mul_sum_quadraticRadical
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  ↑(CryptBoolean.walshTransform f 0) ^ 2 =
    2 ^ n *
      ∑ a,
        FABL.binarySign
          (FABL.booleanDerivative f (↑a)
            0)

theorem CryptBoolean.walshTransform_zero_sq_eq_two_pow_mul_sum_linearKernel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.walshTransform f 0 ^ 2 =
    2 ^ n *
      ∑ a,
        CryptBoolean.bitSignInt
          (FABL.booleanDerivative f (↑a)
            0)

theorem CryptBoolean.quadraticRadicalSignCharacter_eq_zero_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.quadraticRadicalSignCharacter
        f hdegree =
      0 ↔
    ∀
      (a :
        ↥(CryptBoolean.quadraticRadical f
            hdegree)),
      f ↑a = f 0

theorem CryptBoolean.walshTransform_zero_sq_eq_if_constant_on_quadraticRadical
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  ↑(CryptBoolean.walshTransform f 0) ^ 2 =
    if
        ∀
          (a :
            ↥(CryptBoolean.quadraticRadical
                f hdegree)),
          f ↑a = f 0 then
      2 ^ n *
        ↑(Fintype.card
            ↥(CryptBoolean.quadraticRadical
                f hdegree))
    else 0

theorem CryptBoolean.walshTransform_zero_sq_eq_if_constant_on_linearKernel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  ↑(CryptBoolean.walshTransform f 0) ^ 2 =
    if
        ∀
          (a :
            ↥(CryptBoolean.linearKernel
                f)),
          f ↑a = f 0 then
      2 ^ n *
        ↑(Fintype.card
            ↥(CryptBoolean.linearKernel
                f))
    else 0

theorem CryptBoolean.isBalanced_iff_not_constant_on_linearKernel_of_degree_le_two
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.IsBalanced f ↔
    ¬∀
        (a :
          ↥(CryptBoolean.linearKernel f)),
        f ↑a = f 0

theorem CryptBoolean.even_exponent_of_int_sq_eq_two_pow
  (z : ℤ) (e : ℕ) (h : z ^ 2 = 2 ^ e) :
  Even e

theorem CryptBoolean.walshTransform_zero_sq_eq_two_pow_add_finrank_of_not_balanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (hnotBalanced :
    ¬CryptBoolean.IsBalanced f) :
  CryptBoolean.walshTransform f 0 ^ 2 =
    2 ^
      (n +
        Module.finrank FABL.𝔽₂
          ↥(CryptBoolean.linearKernel f))

theorem CryptBoolean.even_dimension_add_finrank_linearKernel_of_not_balanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (hnotBalanced :
    ¬CryptBoolean.IsBalanced f) :
  Even
    (n +
      Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.linearKernel f))

theorem CryptBoolean.quadratic_weight_eq_two_pow_sub_or_add
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2)
  (hnotBalanced :
    ¬CryptBoolean.IsBalanced f) :
  CryptBoolean.hammingWeight f =
      2 ^ (n - 1) -
        2 ^
          ((n +
                Module.finrank FABL.𝔽₂
                  ↥(CryptBoolean.linearKernel
                      f)) /
              2 -
            1) ∨
    CryptBoolean.hammingWeight f =
      2 ^ (n - 1) +
        2 ^
          ((n +
                Module.finrank FABL.𝔽₂
                  ↥(CryptBoolean.linearKernel
                      f)) /
              2 -
            1)

theorem CryptBoolean.theorem_4_quadratic_weight
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  (CryptBoolean.IsBalanced f ↔
      ¬∀
          (a :
            ↥(CryptBoolean.linearKernel
                f)),
          f ↑a = f 0) ∧
    (¬CryptBoolean.IsBalanced f →
      Even
          (n +
            Module.finrank FABL.𝔽₂
              ↥(CryptBoolean.linearKernel
                  f)) ∧
        (CryptBoolean.hammingWeight f =
            2 ^ (n - 1) -
              2 ^
                ((n +
                      Module.finrank
                        FABL.𝔽₂
                        ↥(CryptBoolean.linearKernel
                            f)) /
                    2 -
                  1) ∨
          CryptBoolean.hammingWeight f =
            2 ^ (n - 1) +
              2 ^
                ((n +
                      Module.finrank
                        FABL.𝔽₂
                        ↥(CryptBoolean.linearKernel
                            f)) /
                    2 -
                  1)))

theorem CryptBoolean.isBalanced_iff_quadraticRadicalSignCharacter_ne_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.IsBalanced f ↔
    CryptBoolean.quadraticRadicalSignCharacter
        f hdegree ≠
      0

theorem CryptBoolean.quadraticRadicalSignCharacter_ne_zero_iff_exists_derivative_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.quadraticRadicalSignCharacter
        f hdegree ≠
      0 ↔
    ∃ a, FABL.booleanDerivative f a = 1

theorem CryptBoolean.isBalanced_iff_exists_booleanDerivative_eq_one_of_degree_le_two
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  CryptBoolean.IsBalanced f ↔
    ∃ a, FABL.booleanDerivative f a = 1

theorem CryptBoolean.mem_linearKernel_and_ne_zero_value_of_booleanDerivative_eq_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n)
  (hderivative :
    FABL.booleanDerivative f a = 1) :
  a ∈ CryptBoolean.linearKernel f ∧
    f a ≠ f 0

theorem CryptBoolean.booleanDerivative_add_affineFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c : FABL.𝔽₂) (u a : FABL.F₂Cube n) :
  FABL.booleanDerivative
      (fun x =>
        f x + FABL.affineFunction c u x)
      a =
    fun x =>
    FABL.booleanDerivative f a x +
      FABL.f₂DotProduct u a

theorem CryptBoolean.linearKernel_add_affineFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c : FABL.𝔽₂) (u : FABL.F₂Cube n) :
  (CryptBoolean.linearKernel fun x =>
      f x + FABL.affineFunction c u x) =
    CryptBoolean.linearKernel f

theorem CryptBoolean.walshTransform_add_linearFunction_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (fun x =>
        f x + FABL.affineFunction 0 u x)
      0 =
    CryptBoolean.walshTransform f u

theorem CryptBoolean.even_dimension_add_finrank_linearKernel_of_degree_le_two
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  Even
    (n +
      Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.linearKernel f))

theorem CryptBoolean.even_codimension_linearKernel_of_degree_le_two
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hdegree :
    FABL.functionAlgebraicDegree f ≤ 2) :
  Even
    (n -
      Module.finrank FABL.𝔽₂
        ↥(CryptBoolean.linearKernel f))

theorem CryptBoolean.isQuadraticOffsetExponent_iff_ceilingHalf
  {n i : ℕ} (hn : 0 < n) :
  CryptBoolean.IsQuadraticOffsetExponent n
      i ↔
    (n + 1) / 2 - 1 ≤ i ∧ i ≤ n - 1

theorem CryptBoolean.isQuadraticOffsetExponent_iff_ceilDiv
  {n i : ℕ} (hn : 0 < n) :
  CryptBoolean.IsQuadraticOffsetExponent n
      i ↔
    n ⌈/⌉ 2 - 1 ≤ i ∧ i ≤ n - 1

theorem CryptBoolean.isQuadraticOffsetExponent_iff_exists_parameters
  {n i : ℕ} (hn : 0 < n) :
  CryptBoolean.IsQuadraticOffsetExponent n
      i ↔
    ∃ d m, n = d + (m + m) ∧ i = d + m - 1

theorem CryptBoolean.hammingWeight_eq_two_pow_pred_of_isBalanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hf : CryptBoolean.IsBalanced f) :
  CryptBoolean.hammingWeight f =
    2 ^ (n - 1)

theorem CryptBoolean.isBalanced_iff_hammingWeight_eq_two_pow_pred
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  CryptBoolean.IsBalanced f ↔
    CryptBoolean.hammingWeight f =
      2 ^ (n - 1)

theorem CryptBoolean.nonlinearity_affineFunction
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) :
  CryptBoolean.nonlinearity
      (FABL.affineFunction b a) =
    0

theorem CryptBoolean.maxWalshMagnitude_affineFunction
  {n : ℕ} (b : FABL.𝔽₂)
  (a : FABL.F₂Cube n) :
  CryptBoolean.maxWalshMagnitude
      (FABL.affineFunction b a) =
    2 ^ n

theorem CryptBoolean.nonlinearity_add_affineFunction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.𝔽₂) (a : FABL.F₂Cube n) :
  CryptBoolean.nonlinearity
      (f + FABL.affineFunction b a) =
    CryptBoolean.nonlinearity f