theorem CryptBoolean.cyclicRotateInput_apply
  {n : ℕ} (x : FABL.F₂Cube n)
  (i : Fin n) :
  CryptBoolean.cyclicRotateInput x i =
    x
      ((CryptBoolean.cyclicCoordinateRotation
          n)
        i)

theorem CryptBoolean.cyclicShiftInput_zero {n : ℕ}
  (x : FABL.F₂Cube n) :
  CryptBoolean.cyclicShiftInput 0 x = x

theorem CryptBoolean.cyclicShiftInput_succ {n : ℕ}
  (k : ℕ) (x : FABL.F₂Cube n) :
  CryptBoolean.cyclicShiftInput (k + 1)
      x =
    CryptBoolean.cyclicRotateInput
      (CryptBoolean.cyclicShiftInput k x)

theorem CryptBoolean.isRotationSymmetric_iff_truthTable_invariant
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsRotationSymmetric f ↔
    ∀ (x : FABL.F₂Cube n),
      f
          (CryptBoolean.cyclicRotateInput
            x) =
        f x

theorem CryptBoolean.isRotationSymmetric_iff_all_cyclicShifts
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsRotationSymmetric f ↔
    ∀ (k : ℕ) (x : FABL.F₂Cube n),
      f
          (CryptBoolean.cyclicShiftInput k
            x) =
        f x

theorem CryptBoolean.cyclicRotateANFIndex_apply
  {n : ℕ} (S : Finset (Fin n)) :
  (CryptBoolean.cyclicRotateANFIndex n)
      S =
    Finset.map
      (Equiv.toEmbedding
        (CryptBoolean.cyclicCoordinateRotation
          n))
      S

theorem CryptBoolean.IsRotationInvariantANF.iterate
  {n : ℕ} {c : FABL.ANFCoefficients n}
  (hc :
    CryptBoolean.IsRotationInvariantANF c)
  (k : ℕ) (S : Finset (Fin n)) :
  c
      ((⇑(CryptBoolean.cyclicRotateANFIndex
              n))^[k]
        S) =
    c S

theorem CryptBoolean.anfMonomial_cyclicRotateInput
  {n : ℕ} (S : Finset (Fin n))
  (x : FABL.F₂Cube n) :
  FABL.anfMonomial S
      (CryptBoolean.cyclicRotateInput x) =
    FABL.anfMonomial
      ((CryptBoolean.cyclicRotateANFIndex
          n)
        S)
      x

theorem CryptBoolean.anfEval_cyclicRotateANFCoefficients
  {n : ℕ} (c : FABL.ANFCoefficients n)
  (x : FABL.F₂Cube n) :
  FABL.anfEval
      (CryptBoolean.cyclicRotateANFCoefficients
        c)
      x =
    FABL.anfEval c
      (CryptBoolean.cyclicRotateInput x)

theorem CryptBoolean.anfCoeff_comp_cyclicRotateInput
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (FABL.anfCoeff fun x =>
      f
        (CryptBoolean.cyclicRotateInput
          x)) =
    CryptBoolean.cyclicRotateANFCoefficients
      (FABL.anfCoeff f)

theorem CryptBoolean.cyclicRotateANFCoefficients_eq_iff
  {n : ℕ} (c : FABL.ANFCoefficients n) :
  CryptBoolean.cyclicRotateANFCoefficients
        c =
      c ↔
    CryptBoolean.IsRotationInvariantANF c

theorem CryptBoolean.isRotationSymmetric_iff_anfInvariant
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsRotationSymmetric f ↔
    CryptBoolean.IsRotationInvariantANF
      (FABL.anfCoeff f)

theorem CryptBoolean.IsRotationSymmetric.anfCoeff_cyclicShift
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsRotationSymmetric f)
  (k : ℕ) (S : Finset (Fin n)) :
  FABL.anfCoeff f
      ((⇑(CryptBoolean.cyclicRotateANFIndex
              n))^[k]
        S) =
    FABL.anfCoeff f S

theorem CryptBoolean.support_card_cyclicRotateInput
  {n : ℕ} (x : FABL.F₂Cube n) :
  (FABL.f₂Support
        (CryptBoolean.cyclicRotateInput
          x)).card =
    (FABL.f₂Support x).card

theorem CryptBoolean.IsSymmetricBooleanFunction.isRotationSymmetric
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsRotationSymmetric f

theorem CryptBoolean.WalshCertificateTree.natAbs_eval_le_of_allNatAbsLe
  {n bound : ℕ}
  (tree :
    CryptBoolean.WalshCertificateTree n)
  (h :
    CryptBoolean.WalshCertificateTree.allNatAbsLe
        bound tree =
      true)
  (a : FABL.F₂Cube n) :
  (tree.eval a).natAbs ≤ bound

theorem CryptBoolean.fastWalshCertificateTree_correct
  (n : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  (CryptBoolean.fastWalshCertificateTree n
          f).eval
      a =
    CryptBoolean.walshTransform f a

theorem CryptBoolean.isRotationSymmetric_kavutMaitraYucelRotationFunction9 :
  CryptBoolean.IsRotationSymmetric
    CryptBoolean.kavutMaitraYucelRotationFunction9

theorem CryptBoolean.kavutMaitraYucelRotationFunction9_walsh_bound
  (a : FABL.F₂Cube 9) :
  (CryptBoolean.walshTransform
        CryptBoolean.kavutMaitraYucelRotationFunction9
        a).natAbs ≤
    30

theorem CryptBoolean.kavutMaitraYucelRotationFunction9_walsh_witness :
  CryptBoolean.walshTransform
      CryptBoolean.kavutMaitraYucelRotationFunction9
      (CryptBoolean.f₂CubeOfNat 9 9) =
    -30

theorem CryptBoolean.maxWalshMagnitude_kavutMaitraYucelRotationFunction9 :
  CryptBoolean.maxWalshMagnitude
      CryptBoolean.kavutMaitraYucelRotationFunction9 =
    30

theorem CryptBoolean.nonlinearity_kavutMaitraYucelRotationFunction9 :
  CryptBoolean.nonlinearity
      CryptBoolean.kavutMaitraYucelRotationFunction9 =
    241

theorem CryptBoolean.quadraticBound_lt_nonlinearity_kavutMaitraYucelRotationFunction9 :
  240 <
    CryptBoolean.nonlinearity
      CryptBoolean.kavutMaitraYucelRotationFunction9

theorem CryptBoolean.exists_rotationSymmetric_nonlinearity_eq_241 :
  ∃ f,
    CryptBoolean.IsRotationSymmetric f ∧
      CryptBoolean.nonlinearity f = 241

theorem CryptBoolean.maxWalshMagnitude_kavutMaitraYucelRotationBentExtension
  (m : ℕ) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.kavutMaitraYucelRotationBentExtension
        m) =
    30 * 2 ^ m

theorem CryptBoolean.nonlinearity_kavutMaitraYucelRotationBentExtension
  (m : ℕ) :
  CryptBoolean.nonlinearity
      (CryptBoolean.kavutMaitraYucelRotationBentExtension
        m) =
    2 ^ (8 + (m + m)) - 15 * 2 ^ m

theorem CryptBoolean.quadraticBound_lt_nonlinearity_kavutMaitraYucelRotationBentExtension
  (m : ℕ) :
  2 ^ (8 + (m + m)) - 2 ^ (4 + m) <
    CryptBoolean.nonlinearity
      (CryptBoolean.kavutMaitraYucelRotationBentExtension
        m)

theorem CryptBoolean.nonlinearity_kavutMaitraYucelRotationBentExtension_one :
  CryptBoolean.nonlinearity
      (CryptBoolean.kavutMaitraYucelRotationBentExtension
        1) =
    994

theorem CryptBoolean.nonlinearity_kavutMaitraYucelRotationBentExtension_two :
  CryptBoolean.nonlinearity
      (CryptBoolean.kavutMaitraYucelRotationBentExtension
        2) =
    4036

theorem CryptBoolean.restrictedSupportCardIndex_val
  {n : ℕ} (S : Finset (Fin n))
  (x : FABL.F₂Cube n) :
  ↑(CryptBoolean.restrictedSupportCardIndex
        S x) =
    (FABL.f₂Support x ∩ S).card

theorem CryptBoolean.fullCoordinateProfileIndexEquiv_restrictedSupportCardIndex
  {n : ℕ} (x : FABL.F₂Cube n) :
  (CryptBoolean.fullCoordinateProfileIndexEquiv
        n)
      (CryptBoolean.restrictedSupportCardIndex
        Finset.univ x) =
    CryptBoolean.supportCardIndex x

theorem CryptBoolean.isMatriochkaSymmetric_iff_exists_nestedProfile
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsMatriochkaSymmetric f ↔
    ∃ r,
      ∀ (x : FABL.F₂Cube n),
        f x =
          ∑ j,
            r.profile j
              (CryptBoolean.restrictedSupportCardIndex
                (r.coordinateSet j) x)

theorem CryptBoolean.isMatriochkaSymmetric_zero
  {n : ℕ} :
  CryptBoolean.IsMatriochkaSymmetric 0

theorem CryptBoolean.IsSymmetricBooleanFunction.isMatriochkaSymmetric
  {n : ℕ}
  {f : CryptBoolean.BooleanFunction n}
  (hf :
    CryptBoolean.IsSymmetricBooleanFunction
      f) :
  CryptBoolean.IsMatriochkaSymmetric f