theorem CryptBoolean.complementaryPairDirectionLinearMap_apply_append
  {l r : ℕ} (u : FABL.F₂Cube l)
  (y : FABL.F₂Cube r) :
  (CryptBoolean.complementaryPairDirectionLinearMap
        l r)
      (Fin.append u y) =
    Fin.append u (Fin.append u y)

theorem CryptBoolean.complementaryPairDirectionLinearMap_injective
  (l r : ℕ) :
  Function.Injective
    ⇑(CryptBoolean.complementaryPairDirectionLinearMap
        l r)

theorem CryptBoolean.complementaryPairDirectionLinearEquiv_apply_coe
  {l r : ℕ} (z : FABL.F₂Cube (l + r)) :
  ↑((CryptBoolean.complementaryPairDirectionLinearEquiv
          l r)
        z) =
    (CryptBoolean.complementaryPairDirectionLinearMap
        l r)
      z

theorem CryptBoolean.complementaryPairPoint_append
  {l r : ℕ} (u : FABL.F₂Cube l)
  (y : FABL.F₂Cube r) :
  (CryptBoolean.complementaryPairDirectionLinearMap
          l r)
        (Fin.append u y) +
      CryptBoolean.complementaryPairBase l
        r =
    Fin.append u (Fin.append (u + 1) y)

theorem CryptBoolean.card_f₂Support_complementaryPairPoint
  {l r : ℕ} (u : FABL.F₂Cube l)
  (y : FABL.F₂Cube r) :
  (FABL.f₂Support
        (Fin.append u
          (Fin.append (u + 1) y))).card =
    l + (FABL.f₂Support y).card

theorem CryptBoolean.finrank_complementaryPairDirectionSubspace
  (l r : ℕ) :
  Module.finrank FABL.𝔽₂
      ↥(CryptBoolean.complementaryPairDirectionSubspace
          l r) =
    l + r

theorem CryptBoolean.isConstantOnAffineFlat_of_coordinateRestriction_eq_const
  {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)}
  {a : FABL.F₂Cube n}
  {e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E}
  {b : FABL.𝔽₂}
  (hrestriction :
    CryptBoolean.coordinateAffineSubspaceRestriction
        f E a e =
      fun x => b) :
  CryptBoolean.IsConstantOnAffineFlat f E
    a

theorem CryptBoolean.card_f₂Support_eq_middle_of_mem_complementaryPairAffineFlat
  {m : ℕ} (x : FABL.F₂Cube (m + m))
  (hx :
    x ∈
      FABL.binaryAffineSubspace
        (CryptBoolean.complementaryPairDirectionSubspace
          m 0)
        (CryptBoolean.complementaryPairBase
          m 0)) :
  (FABL.f₂Support x).card = m

theorem CryptBoolean.isKNormal_even_of_constant_on_middleLayer
  {m : ℕ}
  {f :
    CryptBoolean.BooleanFunction (m + m)}
  {b : FABL.𝔽₂}
  (hf :
    ∀ (x : FABL.F₂Cube (m + m)),
      (FABL.f₂Support x).card = m →
        f x = b) :
  CryptBoolean.IsKNormal f m

theorem CryptBoolean.IsSymmetricBooleanFunction.isConstantOnComplementaryPairFlat_even
  {m : ℕ}
  {f :
    CryptBoolean.BooleanFunction (m + m)}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsConstantOnAffineFlat f
    (CryptBoolean.complementaryPairDirectionSubspace
      m 0)
    (CryptBoolean.complementaryPairBase m
      0)

theorem CryptBoolean.IsSymmetricBooleanFunction.isKNormal_even
  {m : ℕ}
  {f :
    CryptBoolean.BooleanFunction (m + m)}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsKNormal f m

theorem CryptBoolean.isBent_completeQuadraticBit_add_affineFunction_smul_fullDirection
  {n : ℕ} (hn : Even n) (a b : FABL.𝔽₂) :
  CryptBoolean.IsBent
    (FABL.completeQuadraticBit +
      FABL.affineFunction b
        (a •
          CryptBoolean.fullDirection n))

theorem CryptBoolean.symmetric_isBent_iff_completeQuadraticBit_add_affineFunction_smul_fullDirection
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hn : Even n) (hnpos : 0 < n)
  (hsym :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsBent f ↔
    ∃ a b,
      f =
        FABL.completeQuadraticBit +
          FABL.affineFunction b
            (a •
              CryptBoolean.fullDirection
                n)

theorem CryptBoolean.nonlinearity_eq_two_pow_sub_two_pow_half_of_symmetric_isBent
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hn : Even n) (hnpos : 0 < n)
  (_hsym :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hf : CryptBoolean.IsBent f) :
  CryptBoolean.nonlinearity f =
    2 ^ (n - 1) - 2 ^ (n / 2 - 1)

theorem CryptBoolean.coordinateDirection_add_eq_f₂CubeOfFinset_pair
  {n : ℕ} (i j : Fin n) (hij : i ≠ j) :
  CryptBoolean.coordinateDirection i +
      CryptBoolean.coordinateDirection j =
    FABL.f₂CubeOfFinset {i, j}

theorem CryptBoolean.f₂Support_coordinateDirection_add
  {n : ℕ} (i j : Fin n) (hij : i ≠ j) :
  FABL.f₂Support
      (CryptBoolean.coordinateDirection
          i +
        CryptBoolean.coordinateDirection
          j) =
    {i, j}

theorem CryptBoolean.card_f₂Support_coordinateDirection_add
  {n : ℕ} (i j : Fin n) (hij : i ≠ j) :
  (FABL.f₂Support
        (CryptBoolean.coordinateDirection
            i +
          CryptBoolean.coordinateDirection
            j)).card =
    2

theorem CryptBoolean.coordinateDirection_add_ne_zero
  {n : ℕ} (i j : Fin n) (hij : i ≠ j) :
  CryptBoolean.coordinateDirection i +
      CryptBoolean.coordinateDirection j ≠
    0

theorem CryptBoolean.f₂DotProduct_coordinateDirection_add
  {n : ℕ} (i j : Fin n) (hij : i ≠ j)
  (x : FABL.F₂Cube n) :
  FABL.f₂DotProduct
      (CryptBoolean.coordinateDirection
          i +
        CryptBoolean.coordinateDirection
          j)
      x =
    x i + x j

theorem CryptBoolean.isSymmetricBooleanFunction_completeQuadraticBit
  {n : ℕ} :
  CryptBoolean.IsSymmetricBooleanFunction
    FABL.completeQuadraticBit

theorem CryptBoolean.booleanDerivative_coordinateDirection_add_eq_affineFunction_of_symmetric_pc_two
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hsym :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      2 f)
  (i j : Fin n) (hij : i ≠ j) :
  FABL.booleanDerivative f
      (CryptBoolean.coordinateDirection
          i +
        CryptBoolean.coordinateDirection
          j) =
    FABL.affineFunction 1
      (CryptBoolean.coordinateDirection
          i +
        CryptBoolean.coordinateDirection
          j)

theorem CryptBoolean.coordinateSecondDerivatives_eq_one_of_symmetric_pc_two
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hsym :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hpc :
    CryptBoolean.SatisfiesPropagationCriterion
      2 f)
  (i j : Fin n) :
  i ≠ j →
    CryptBoolean.secondBooleanDerivative f
        (CryptBoolean.coordinateDirection
          i)
        (CryptBoolean.coordinateDirection
          j) =
      1

theorem CryptBoolean.f₂DotProduct_smul_fullDirection
  {n : ℕ} (a : FABL.𝔽₂)
  (x : FABL.F₂Cube n) :
  FABL.f₂DotProduct
      (a • CryptBoolean.fullDirection n)
      x =
    a * ↑(FABL.f₂Support x).card

theorem CryptBoolean.isSymmetricBooleanFunction_affineFunction_smul_fullDirection
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.IsSymmetricBooleanFunction
    (FABL.affineFunction b
      (a • CryptBoolean.fullDirection n))

theorem CryptBoolean.eq_zero_or_eq_fullDirection_of_isSymmetric_affineFunction
  {n : ℕ} (hn : 0 < n) (c : FABL.𝔽₂)
  (u : FABL.F₂Cube n)
  (hsym :
    CryptBoolean.IsSymmetricBooleanFunction
      (FABL.affineFunction c u)) :
  u = 0 ∨ u = CryptBoolean.fullDirection n

theorem CryptBoolean.isSymmetricBooleanFunction_completeQuadraticBit_add_affineFunction_smul_fullDirection
  {n : ℕ} (a b : FABL.𝔽₂) :
  CryptBoolean.IsSymmetricBooleanFunction
    (FABL.completeQuadraticBit +
      FABL.affineFunction b
        (a •
          CryptBoolean.fullDirection n))

theorem CryptBoolean.symmetric_satisfiesPropagationCriterion_two_iff
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hn : Even n) (hnpos : 0 < n)
  (hsym :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.SatisfiesPropagationCriterion
      2 f ↔
    ∃ a b,
      f =
        FABL.completeQuadraticBit +
          FABL.affineFunction b
            (a •
              CryptBoolean.fullDirection
                n)

theorem CryptBoolean.isAffineOnAffineFlat_of_coordinateRestriction_eq_affineFunction
  {n k : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  {E : Submodule FABL.𝔽₂ (FABL.F₂Cube n)}
  {a : FABL.F₂Cube n}
  {e : FABL.F₂Cube k ≃ₗ[FABL.𝔽₂] ↥E}
  {b : FABL.𝔽₂} {c : FABL.F₂Cube k}
  (hrestriction :
    CryptBoolean.coordinateAffineSubspaceRestriction
        f E a e =
      FABL.affineFunction b c) :
  CryptBoolean.IsAffineOnAffineFlat f E a

theorem CryptBoolean.IsSymmetricBooleanFunction.isAffineOnComplementaryPairFlat_odd
  {m : ℕ}
  {f :
    CryptBoolean.BooleanFunction
      (m + (m + 1))}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsAffineOnAffineFlat f
    (CryptBoolean.complementaryPairDirectionSubspace
      m 1)
    (CryptBoolean.complementaryPairBase m
      1)

theorem CryptBoolean.IsSymmetricBooleanFunction.isKWeaklyNormal_odd
  {m : ℕ}
  {f :
    CryptBoolean.BooleanFunction
      (m + (m + 1))}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsKWeaklyNormal f (m + 1)

theorem CryptBoolean.IsSymmetricBooleanFunction.nonlinearity_le_odd
  {m : ℕ}
  {f :
    CryptBoolean.BooleanFunction
      (m + (m + 1))}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.nonlinearity f ≤
    2 ^ (m + (m + 1) - 1) - 2 ^ m

theorem CryptBoolean.completeQuadraticBit_odd_eq_hyperplaneExtension
  (m : ℕ) :
  FABL.completeQuadraticBit =
    CryptBoolean.hyperplaneExtension
      FABL.completeQuadraticBit
      (FABL.completeQuadraticBit +
        FABL.affineFunction 0 1)

theorem CryptBoolean.nonlinearity_completeQuadraticBit_odd
  (m : ℕ) :
  CryptBoolean.nonlinearity
      FABL.completeQuadraticBit =
    2 ^ (m + (m + 1) - 1) - 2 ^ m

theorem CryptBoolean.symmetricQuadraticNormalForm_eq_completeQuadratic_add_affineFunction
  (n : ℕ) (a b : FABL.𝔽₂) :
  CryptBoolean.symmetricQuadraticNormalForm
      n a b =
    FABL.completeQuadraticBit +
      FABL.affineFunction b
        (a • CryptBoolean.fullDirection n)

theorem CryptBoolean.nonlinearity_symmetricQuadraticNormalForm_odd
  (m : ℕ) (a b : FABL.𝔽₂) :
  CryptBoolean.nonlinearity
      (CryptBoolean.symmetricQuadraticNormalForm
        (m + (m + 1)) a b) =
    2 ^ (m + (m + 1) - 1) - 2 ^ m

theorem CryptBoolean.nonlinearity_eq_odd_quadraticBound_of_eq_symmetricQuadraticNormalForm
  {m : ℕ}
  {f :
    CryptBoolean.BooleanFunction
      (m + (m + 1))}
  (hform :
    ∃ a b,
      f =
        CryptBoolean.symmetricQuadraticNormalForm
          (m + (m + 1)) a b) :
  CryptBoolean.nonlinearity f =
    2 ^ (m + (m + 1) - 1) - 2 ^ m

theorem CryptBoolean.completeQuadraticPolarFrequency_fullDirection_odd
  (m : ℕ) :
  CryptBoolean.completeQuadraticPolarFrequency
      (CryptBoolean.fullDirection
        (m + (m + 1))) =
    0

theorem CryptBoolean.domainTranslate_completeQuadraticBit_add_affineFunction
  {n : ℕ} (b : FABL.𝔽₂)
  (a t : FABL.F₂Cube n) :
  FABL.domainTranslate
      (FABL.completeQuadraticBit +
        FABL.affineFunction b a)
      t =
    FABL.completeQuadraticBit +
      FABL.affineFunction
        (FABL.completeQuadraticBit t + b +
          FABL.f₂DotProduct a t)
        (CryptBoolean.completeQuadraticPolarFrequency
            t +
          a)

theorem CryptBoolean.exists_affineFunction_hammingDistance_eq_nonlinearity
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  ∃ b a,
    CryptBoolean.hammingDistance f
        (FABL.affineFunction b a) =
      CryptBoolean.nonlinearity f

theorem CryptBoolean.exists_completeQuadraticBit_minimumAffineError_one_at_endpoints_odd
  (m : ℕ) (hm : 0 < m) :
  ∃ b a,
    CryptBoolean.hammingWeight
          (FABL.completeQuadraticBit +
            FABL.affineFunction b a) =
        2 ^ (m + (m + 1) - 1) - 2 ^ m ∧
      (FABL.completeQuadraticBit +
              FABL.affineFunction b a)
            0 =
          1 ∧
        (FABL.completeQuadraticBit +
              FABL.affineFunction b a)
            (CryptBoolean.fullDirection
              (m + (m + 1))) =
          1

theorem CryptBoolean.hammingWeight_add_lt_of_support_nonempty_of_subset
  {n : ℕ}
  (e d : CryptBoolean.BooleanFunction n)
  (hd : (CryptBoolean.support d).Nonempty)
  (hde :
    CryptBoolean.support d ⊆
      CryptBoolean.support e) :
  CryptBoolean.hammingWeight (e + d) <
    CryptBoolean.hammingWeight e

theorem CryptBoolean.exists_symmetricQuadraticNormalForm_of_odd_optimal_nonlinearity
  (m : ℕ)
  {f :
    CryptBoolean.BooleanFunction
      (m + (m + 1))}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (hnonlinearity :
    CryptBoolean.nonlinearity f =
      2 ^ (m + (m + 1) - 1) - 2 ^ m) :
  ∃ a b,
    f =
      CryptBoolean.symmetricQuadraticNormalForm
        (m + (m + 1)) a b

theorem CryptBoolean.symmetric_odd_optimal_nonlinearity_iff_symmetricQuadraticNormalForm
  (m : ℕ)
  {f :
    CryptBoolean.BooleanFunction
      (m + (m + 1))}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.nonlinearity f =
      2 ^ (m + (m + 1) - 1) - 2 ^ m ↔
    ∃ a b,
      f =
        CryptBoolean.symmetricQuadraticNormalForm
          (m + (m + 1)) a b

theorem CryptBoolean.IsSymmetricBooleanFunction.eq_complementaryPairRestriction
  {l r : ℕ}
  {f :
    CryptBoolean.BooleanFunction
      (l + (l + r))}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f)
  (u : FABL.F₂Cube l)
  (y : FABL.F₂Cube r) :
  f
      (Fin.append u
        (Fin.append (u + 1) y)) =
    CryptBoolean.complementaryPairRestriction
      f y