7.3. Propagation criteria of order🔗

Theorem7.3.1

Group: Chapter 7: Strict avalanche and propagation criteria (13)

Group member previews

Preview

Theorem 7.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 1.10.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

Tagscarletchapter-8proposition-36propagation-criterionorderwalsh-transformpage-132fidelity-exact

Proposition 36 (Carlet, p. 132). Let \ell+k\le n and f:V_n\to\mathbb F_2. Then f satisfies \mathrm{EPC}(\ell) of order k if and only if, for every a,b\in V_n with w_H(a)\le\ell, w_H(b)\le k, and (a,b)\ne(0,0), \sum_{x\in V_n}(-1)^{f(x)\oplus f(x\oplus a)\oplus b\cdot x}=0. It satisfies \mathrm{PC}(\ell) of order k if and only if the same identity holds whenever, in addition, \operatorname{supp}(a)\cap\operatorname{supp}(b)=\varnothing.

Lean code for Theorem7.3.1●6 theorems

theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean

complete

theorem CryptBoolean.all_coordinateRestrictions_balanced_iff_walshTransform_eq_zero
  {n : ℕ} (g : CryptBoolean.BooleanFunction n) (J : Finset (Fin n)) :
  (∀ (z : FABL.FixedSignCube J),
      CryptBoolean.IsBalanced
        (CryptBoolean.coordinateRestriction g J z)) ↔
    ∀ (b : FABL.F₂Cube n),
      FABL.f₂Support b ⊆ Jᶜ → CryptBoolean.walshTransform g b = 0

theorem CryptBoolean.all_coordinateRestrictions_balanced_iff_walshTransform_eq_zero
  {n : ℕ}
  (g : CryptBoolean.BooleanFunction n)
  (J : Finset (Fin n)) :
  (∀ (z : FABL.FixedSignCube J),
      CryptBoolean.IsBalanced
        (CryptBoolean.coordinateRestriction
          g J z)) ↔
    ∀ (b : FABL.F₂Cube n),
      FABL.f₂Support b ⊆ Jᶜ →
        CryptBoolean.walshTransform g b =
          0

All restrictions obtained by fixing the coordinates outside `J` are
balanced exactly when the raw Walsh spectrum vanishes at every frequency
supported outside `J`.

theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_iff_derivativeRestrictions_balanced
  {n : ℕ} (l k : ℕ) (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f ↔
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          ∀ (J : Finset (Fin n)) (z : FABL.FixedSignCube J),
            Fintype.card (FABL.FixedIndex J) = k →
              FABL.f₂Support a ⊆ J →
                CryptBoolean.IsBalanced
                  (CryptBoolean.coordinateRestriction
                    (FABL.booleanDerivative f a) J z)

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_iff_derivativeRestrictions_balanced
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f ↔
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        (FABL.f₂Support a).card ≤ l →
          ∀ (J : Finset (Fin n))
            (z : FABL.FixedSignCube J),
            Fintype.card
                  (FABL.FixedIndex J) =
                k →
              FABL.f₂Support a ⊆ J →
                CryptBoolean.IsBalanced
                  (CryptBoolean.coordinateRestriction
                    (FABL.booleanDerivative
                      f a)
                    J z)

Order-`k` propagation is equivalently balancedness of every restriction
of each eligible ambient derivative whose direction remains free.

theoremdefined in CryptBoolean/Carlet/Chapter08/OrderCharacterization.lean

complete

theorem CryptBoolean.walshTransform_booleanDerivative_eq_sum_bitSignInt {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a b : FABL.F₂Cube n) :
  CryptBoolean.walshTransform (FABL.booleanDerivative f a) b =
    ∑ x,
      CryptBoolean.bitSignInt (f x + f (x + a) + FABL.f₂DotProduct b x)

theorem CryptBoolean.walshTransform_booleanDerivative_eq_sum_bitSignInt
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a b : FABL.F₂Cube n) :
  CryptBoolean.walshTransform
      (FABL.booleanDerivative f a) b =
    ∑ x,
      CryptBoolean.bitSignInt
        (f x + f (x + a) +
          FABL.f₂DotProduct b x)

The Walsh transform of a derivative is Carlet's displayed signed
derivative character sum.

theoremdefined in CryptBoolean/Carlet/Chapter08/OrderCharacterization.lean

complete

theorem CryptBoolean.walshTransform_booleanDerivative_zero_direction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n)
  (hb : b ≠ 0) :
  CryptBoolean.walshTransform (FABL.booleanDerivative f 0) b = 0

theorem CryptBoolean.walshTransform_booleanDerivative_zero_direction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) (hb : b ≠ 0) :
  CryptBoolean.walshTransform
      (FABL.booleanDerivative f 0) b =
    0

The zero-direction derivative has zero Walsh transform at every nonzero
frequency.

theoremdefined in CryptBoolean/Carlet/Chapter08/OrderCharacterization.lean

complete

theorem CryptBoolean.satisfiesExtendedPropagationCriterion_iff_walshTransform_booleanDerivative_eq_zero
  {n : ℕ} (l k : ℕ) (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesExtendedPropagationCriterion l k f ↔
    ∀ (a b : FABL.F₂Cube n),
      (FABL.f₂Support a).card ≤ l →
        (FABL.f₂Support b).card ≤ k →
          (a, b) ≠ (0, 0) →
            CryptBoolean.walshTransform (FABL.booleanDerivative f a) b =
              0

theorem CryptBoolean.satisfiesExtendedPropagationCriterion_iff_walshTransform_booleanDerivative_eq_zero
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesExtendedPropagationCriterion
      l k f ↔
    ∀ (a b : FABL.F₂Cube n),
      (FABL.f₂Support a).card ≤ l →
        (FABL.f₂Support b).card ≤ k →
          (a, b) ≠ (0, 0) →
            CryptBoolean.walshTransform
                (FABL.booleanDerivative f
                  a)
                b =
              0

Carlet Proposition 36, extended form: `EPC(l)` of order `k` is equivalent
to the low-weight Walsh zeros of every directional derivative, including the
automatic boundary `a = 0`, `b ≠ 0`.

theoremdefined in CryptBoolean/Carlet/Chapter08/OrderCharacterization.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_iff_walshTransform_booleanDerivative_eq_zero
  {n : ℕ} (l k : ℕ) (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f ↔
    ∀ (a b : FABL.F₂Cube n),
      (FABL.f₂Support a).card ≤ l →
        (FABL.f₂Support b).card ≤ k →
          (a, b) ≠ (0, 0) →
            Disjoint (FABL.f₂Support a) (FABL.f₂Support b) →
              CryptBoolean.walshTransform (FABL.booleanDerivative f a)
                  b =
                0

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_iff_walshTransform_booleanDerivative_eq_zero
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f ↔
    ∀ (a b : FABL.F₂Cube n),
      (FABL.f₂Support a).card ≤ l →
        (FABL.f₂Support b).card ≤ k →
          (a, b) ≠ (0, 0) →
            Disjoint (FABL.f₂Support a)
                (FABL.f₂Support b) →
              CryptBoolean.walshTransform
                  (FABL.booleanDerivative
                    f a)
                  b =
                0

Carlet Proposition 36, restriction form: `PC(l)` of order `k` is
equivalent to the same derivative Walsh zeros when the direction and frequency
have disjoint supports. The `a = 0`, `b ≠ 0` boundary is retained explicitly.

Theorem7.3.2

Group: Chapter 7: Strict avalanche and propagation criteria (13)

Group member previews

Preview

Theorem 7.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 2

Statement dependency previews

Preview

Corollary 1.8.6

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-8proposition-37propagation-criterionorderwalsh-transformrestrictionpage-133fidelity-exact

Proposition 37 (Carlet, p. 133). Let \ell+k\le n and f:V_n\to\mathbb F_2. For v\in V_n, define W_f^v(w)=\sum_{x\preceq v}(-1)^{f(x)\oplus w\cdot x}. Then f satisfies \mathrm{EPC}(\ell) of order k if and only if, for all u,v\in V_n with w_H(u)\ge n-\ell and w_H(v)\ge n-k, \sum_{w\preceq u}W_f(w)W_f^v(w)=2^{w_H(u)+w_H(v)}. It satisfies \mathrm{PC}(\ell) of order k if and only if the same identity holds whenever \operatorname{supp}(\bar u)\cap\operatorname{supp}(\bar v)=\varnothing.

Lean code for Theorem7.3.2●11 declarations

defdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean

complete

def CryptBoolean.predecessorSubspace {n : ℕ} (u : FABL.F₂Cube n) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n)

def CryptBoolean.predecessorSubspace {n : ℕ}
  (u : FABL.F₂Cube n) :
  Submodule FABL.𝔽₂ (FABL.F₂Cube n)

The coordinate subspace consisting of the binary vectors whose supports
are contained in the support of `u`.

theoremdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean

complete

theorem CryptBoolean.mem_predecessorSubspace_iff {n : ℕ} (u w : FABL.F₂Cube n) :
  w ∈ CryptBoolean.predecessorSubspace u ↔
    CryptBoolean.supportPrecedes w u

theorem CryptBoolean.mem_predecessorSubspace_iff
  {n : ℕ} (u w : FABL.F₂Cube n) :
  w ∈ CryptBoolean.predecessorSubspace u ↔
    CryptBoolean.supportPrecedes w u

Membership in the predecessor subspace is support inclusion.

theoremdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean

complete

theorem CryptBoolean.card_predecessorSubspace {n : ℕ} (u : FABL.F₂Cube n) :
  Nat.card ↥(CryptBoolean.predecessorSubspace u) =
    2 ^ (FABL.f₂Support u).card

theorem CryptBoolean.card_predecessorSubspace
  {n : ℕ} (u : FABL.F₂Cube n) :
  Nat.card
      ↥(CryptBoolean.predecessorSubspace
          u) =
    2 ^ (FABL.f₂Support u).card

The predecessor subspace has cardinality `2` to the Hamming weight of its
indexing vector.

theoremdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean

complete

theorem CryptBoolean.perpendicular_predecessorSubspace {n : ℕ}
  (u : FABL.F₂Cube n) :
  FABL.perpendicularSubspace (CryptBoolean.predecessorSubspace u) =
    FABL.F₂DecisionTree.coordinateZeroSubspace (FABL.f₂Support u)

theorem CryptBoolean.perpendicular_predecessorSubspace
  {n : ℕ} (u : FABL.F₂Cube n) :
  FABL.perpendicularSubspace
      (CryptBoolean.predecessorSubspace
        u) =
    FABL.F₂DecisionTree.coordinateZeroSubspace
      (FABL.f₂Support u)

The perpendicular of the predecessor subspace is the coordinate subspace
supported on the complementary coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter08/AffineFlatWalshCharacterization.lean

complete

theorem CryptBoolean.mem_perpendicular_predecessorSubspace_iff {n : ℕ}
  (u a : FABL.F₂Cube n) :
  a ∈ FABL.perpendicularSubspace (CryptBoolean.predecessorSubspace u) ↔
    FABL.f₂Support a ⊆ (FABL.f₂Support u)ᶜ

theorem CryptBoolean.mem_perpendicular_predecessorSubspace_iff
  {n : ℕ} (u a : FABL.F₂Cube n) :
  a ∈
      FABL.perpendicularSubspace
        (CryptBoolean.predecessorSubspace
          u) ↔
    FABL.f₂Support a ⊆ (FABL.f₂Support u)ᶜ

Membership in the perpendicular predecessor subspace is support inclusion
in the complementary coordinates.

defdefined in CryptBoolean/Carlet/Chapter08/RestrictionWalshCharacterization.lean

complete

def CryptBoolean.coordinateRestrictedWalshTransform {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (v w : FABL.F₂Cube n) : ℝ

def CryptBoolean.coordinateRestrictedWalshTransform
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (v w : FABL.F₂Cube n) : ℝ

The raw Walsh transform of the restriction of `f` to the coordinate
subspace indexed by `v`.

defdefined in CryptBoolean/Carlet/Chapter08/RestrictionWalshCharacterization.lean

complete

def CryptBoolean.predecessorWalshRestrictionProductSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u v : FABL.F₂Cube n) : ℝ

def CryptBoolean.predecessorWalshRestrictionProductSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u v : FABL.F₂Cube n) : ℝ

The product sum in Carlet Proposition 37.

defdefined in CryptBoolean/Carlet/Chapter08/RestrictionWalshCharacterization.lean

complete

def CryptBoolean.derivativeWalshRectangleSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (u v : FABL.F₂Cube n) : ℝ

def CryptBoolean.derivativeWalshRectangleSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u v : FABL.F₂Cube n) : ℝ

The rectangular sum of the derivative Walsh transform over the two
complementary coordinate subspaces.

theoremdefined in CryptBoolean/Carlet/Chapter08/RestrictionWalshCharacterization.lean

complete

theorem CryptBoolean.predecessorWalshRestrictionProductSum_eq_derivativeWalshRectangleSum
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (u v : FABL.F₂Cube n) :
  2 ^ (n - (FABL.f₂Support v).card) *
      CryptBoolean.predecessorWalshRestrictionProductSum f u v =
    2 ^ (FABL.f₂Support u).card *
      CryptBoolean.derivativeWalshRectangleSum f u v

theorem CryptBoolean.predecessorWalshRestrictionProductSum_eq_derivativeWalshRectangleSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u v : FABL.F₂Cube n) :
  2 ^ (n - (FABL.f₂Support v).card) *
      CryptBoolean.predecessorWalshRestrictionProductSum
        f u v =
    2 ^ (FABL.f₂Support u).card *
      CryptBoolean.derivativeWalshRectangleSum
        f u v

Double Poisson summation identifies the restriction-Walsh product sum
with the rectangular derivative-Walsh sum.

theoremdefined in CryptBoolean/Carlet/Chapter08/RestrictionWalshCharacterization.lean

complete

theorem CryptBoolean.satisfiesExtendedPropagationCriterion_iff_predecessorWalshRestrictionProductSum
  {n : ℕ} (l k : ℕ) (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesExtendedPropagationCriterion l k f ↔
    ∀ (u v : FABL.F₂Cube n),
      n - l ≤ (FABL.f₂Support u).card →
        n - k ≤ (FABL.f₂Support v).card →
          CryptBoolean.predecessorWalshRestrictionProductSum f u v =
            2 ^ ((FABL.f₂Support u).card + (FABL.f₂Support v).card)

theorem CryptBoolean.satisfiesExtendedPropagationCriterion_iff_predecessorWalshRestrictionProductSum
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesExtendedPropagationCriterion
      l k f ↔
    ∀ (u v : FABL.F₂Cube n),
      n - l ≤ (FABL.f₂Support u).card →
        n - k ≤ (FABL.f₂Support v).card →
          CryptBoolean.predecessorWalshRestrictionProductSum
              f u v =
            2 ^
              ((FABL.f₂Support u).card +
                (FABL.f₂Support v).card)

Carlet Proposition 37, extended form: `EPC(l)` of order `k` is
equivalent to the restriction-Walsh product identity on all qualifying
coordinate subspaces.

theoremdefined in CryptBoolean/Carlet/Chapter08/RestrictionWalshCharacterization.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_iff_predecessorWalshRestrictionProductSum
  {n : ℕ} (l k : ℕ) (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f ↔
    ∀ (u v : FABL.F₂Cube n),
      n - l ≤ (FABL.f₂Support u).card →
        n - k ≤ (FABL.f₂Support v).card →
          Disjoint (FABL.f₂Support u)ᶜ (FABL.f₂Support v)ᶜ →
            CryptBoolean.predecessorWalshRestrictionProductSum f u v =
              2 ^ ((FABL.f₂Support u).card + (FABL.f₂Support v).card)

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_iff_predecessorWalshRestrictionProductSum
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f ↔
    ∀ (u v : FABL.F₂Cube n),
      n - l ≤ (FABL.f₂Support u).card →
        n - k ≤ (FABL.f₂Support v).card →
          Disjoint (FABL.f₂Support u)ᶜ
              (FABL.f₂Support v)ᶜ →
            CryptBoolean.predecessorWalshRestrictionProductSum
                f u v =
              2 ^
                ((FABL.f₂Support u).card +
                  (FABL.f₂Support v).card)

Carlet Proposition 37, coordinate-restriction form: `PC(l)` of order `k`
is equivalent to the restriction-Walsh product identity when the complements
of the two indexing supports are disjoint.

Theorem7.3.3

Group: Chapter 7: Strict avalanche and propagation criteria (13)

Group member previews

Preview

Theorem 7.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 1.4.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-8strict-avalanche-criterionorderalgebraic-degreepage-133fidelity-explicit-valid-dimension-range

Algebraic degree under SAC of order k (Carlet, p. 133). Let k+3\le n, and let f:V_n\to\mathbb F_2 satisfy the strict avalanche criterion of order k. Every restriction obtained by fixing k input coordinates has algebraic degree at most n-k-1; in particular, \deg(f)\le n-k-1.

Lean code for Theorem7.3.3●4 theorems

theoremdefined in CryptBoolean/Carlet/Chapter04/PropagationCriteria.lean

complete

theorem CryptBoolean.coordinateRestriction_zeroFixed_apply {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (J : Finset (Fin n))
  (x : FABL.F₂Cube J.card) :
  CryptBoolean.coordinateRestriction f J (fun x => 1) x =
    f (Function.extend (⇑(FABL.freeCoordinateEmbedding J)) x 0)

theorem CryptBoolean.coordinateRestriction_zeroFixed_apply
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (J : Finset (Fin n))
  (x : FABL.F₂Cube J.card) :
  CryptBoolean.coordinateRestriction f J
      (fun x => 1) x =
    f
      (Function.extend
        (⇑(FABL.freeCoordinateEmbedding
            J))
        x 0)

Fixing every complementary coordinate to binary zero realizes the canonical
coordinate restriction by extension along the free-coordinate embedding.

theoremdefined in CryptBoolean/Carlet/Chapter08/OrderAlgebraicDegree.lean

complete

theorem CryptBoolean.anfCoeff_coordinateRestriction_zeroFixed_univ {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (J : Finset (Fin n)) :
  FABL.anfCoeff (CryptBoolean.coordinateRestriction f J fun x => 1)
      Finset.univ =
    FABL.anfCoeff f J

theorem CryptBoolean.anfCoeff_coordinateRestriction_zeroFixed_univ
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (J : Finset (Fin n)) :
  FABL.anfCoeff
      (CryptBoolean.coordinateRestriction
        f J fun x => 1)
      Finset.univ =
    FABL.anfCoeff f J

The top ANF coefficient of a zero-fixed coordinate restriction is the
ambient coefficient on its free-coordinate set.

theoremdefined in CryptBoolean/Carlet/Chapter08/OrderAlgebraicDegree.lean

complete

theorem CryptBoolean.coordinateRestriction_degree_le_of_satisfiesStrictAvalancheCriterionOfOrder
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (k : ℕ) (hkn : k + 3 ≤ n)
  (hf : CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder k f)
  (J : Finset (Fin n)) (z : FABL.FixedSignCube J)
  (hfixed : Fintype.card (FABL.FixedIndex J) = k) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.coordinateRestriction f J z) ≤
    n - k - 1

theorem CryptBoolean.coordinateRestriction_degree_le_of_satisfiesStrictAvalancheCriterionOfOrder
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) (hkn : k + 3 ≤ n)
  (hf :
    CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder
      k f)
  (J : Finset (Fin n))
  (z : FABL.FixedSignCube J)
  (hfixed :
    Fintype.card (FABL.FixedIndex J) =
      k) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.coordinateRestriction
        f J z) ≤
    n - k - 1

Every restriction fixing exactly `k` coordinates of a function satisfying
SAC of order `k` has degree at most `n-k-1`, provided at least three
coordinates remain free.

theoremdefined in CryptBoolean/Carlet/Chapter08/OrderAlgebraicDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_le_of_satisfiesStrictAvalancheCriterionOfOrder
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (k : ℕ) (hkn : k + 3 ≤ n)
  (hf : CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder k f) :
  FABL.functionAlgebraicDegree f ≤ n - k - 1

theorem CryptBoolean.functionAlgebraicDegree_le_of_satisfiesStrictAvalancheCriterionOfOrder
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (k : ℕ) (hkn : k + 3 ≤ n)
  (hf :
    CryptBoolean.SatisfiesStrictAvalancheCriterionOfOrder
      k f) :
  FABL.functionAlgebraicDegree f ≤
    n - k - 1

Preneel's corrected SAC-of-order bound: if `k+3 ≤ n`, then a
function satisfying SAC of order `k` has degree at most `n-k-1`.

Theorem7.3.4

Group: Chapter 7: Strict avalanche and propagation criteria (13)

Group member previews

Preview

Theorem 7.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 6

Statement dependency previews

Preview

Definition 1.4.5

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Tagscarletchapter-8propagation-criterionordercomplete-quadraticclassificationpage-133fidelity-reviewed-inclusive-ranges

Extremal propagation criteria of order (Carlet, p. 133). Let f:V_n\to\mathbb F_2 and suppose either

n\ge6, \ell is positive and even, and \ell\le n-4; or
n\ge10, \ell is odd, and 5\le\ell\le n-5.

Then f satisfies \mathrm{PC}(\ell) of order n-\ell-2 if and only if there exists an affine function h:V_n\to\mathbb F_2 such that f(x_1,\ldots,x_n)= \bigoplus_{1\le i<j\le n}x_ix_j\oplus h(x_1,\ldots,x_n).

Lean code for Theorem7.3.4●57 declarations

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean

complete

theorem CryptBoolean.isBalanced_add_constant_iff {m : ℕ}
  (g : CryptBoolean.BooleanFunction m) (c : FABL.𝔽₂) :
  (CryptBoolean.IsBalanced fun x => g x + c) ↔ CryptBoolean.IsBalanced g

theorem CryptBoolean.isBalanced_add_constant_iff
  {m : ℕ}
  (g : CryptBoolean.BooleanFunction m)
  (c : FABL.𝔽₂) :
  (CryptBoolean.IsBalanced fun x =>
      g x + c) ↔
    CryptBoolean.IsBalanced g

Adding a Boolean constant preserves balancedness.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalPropagation.lean

complete

theorem CryptBoolean.eq_constant_of_coordinateDerivatives_eq_zero {n : ℕ}
  (h : CryptBoolean.BooleanFunction n)
  (hderivative :
    ∀ (i : Fin n),
      FABL.booleanDerivative h (CryptBoolean.coordinateDirection i) = 0)
  (x : FABL.F₂Cube n) : h x = h 0

theorem CryptBoolean.eq_constant_of_coordinateDerivatives_eq_zero
  {n : ℕ}
  (h : CryptBoolean.BooleanFunction n)
  (hderivative :
    ∀ (i : Fin n),
      FABL.booleanDerivative h
          (CryptBoolean.coordinateDirection
            i) =
        0)
  (x : FABL.F₂Cube n) : h x = h 0

A Boolean function whose derivative vanishes in every coordinate
direction is constant.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.completeQuadraticPolarFrequency_apply_eq_sum_add {n : ℕ}
  (a : FABL.F₂Cube n) (i : Fin n) :
  CryptBoolean.completeQuadraticPolarFrequency a i = ∑ j, a j + a i

theorem CryptBoolean.completeQuadraticPolarFrequency_apply_eq_sum_add
  {n : ℕ} (a : FABL.F₂Cube n)
  (i : Fin n) :
  CryptBoolean.completeQuadraticPolarFrequency
      a i =
    ∑ j, a j + a i

The polar frequency of the complete quadratic function is the total
coordinate sum plus the corresponding coordinate.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.booleanDerivative_completeQuadraticBit_eq_affineFunction
  {n : ℕ} (a : FABL.F₂Cube n) :
  FABL.booleanDerivative FABL.completeQuadraticBit a =
    FABL.affineFunction (FABL.completeQuadraticBit a)
      (CryptBoolean.completeQuadraticPolarFrequency a)

theorem CryptBoolean.booleanDerivative_completeQuadraticBit_eq_affineFunction
  {n : ℕ} (a : FABL.F₂Cube n) :
  FABL.booleanDerivative
      FABL.completeQuadraticBit a =
    FABL.affineFunction
      (FABL.completeQuadraticBit a)
      (CryptBoolean.completeQuadraticPolarFrequency
        a)

Every derivative of the complete quadratic function is the affine
function whose linear part is its polar frequency.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.ne_completeQuadraticPolarFrequency_of_disjoint_of_support_card_add_lt
  {n : ℕ} (a b : FABL.F₂Cube n) (hab : (a, b) ≠ (0, 0))
  (hdisjoint : Disjoint (FABL.f₂Support a) (FABL.f₂Support b))
  (hcard : (FABL.f₂Support a).card + (FABL.f₂Support b).card < n) :
  b ≠ CryptBoolean.completeQuadraticPolarFrequency a

theorem CryptBoolean.ne_completeQuadraticPolarFrequency_of_disjoint_of_support_card_add_lt
  {n : ℕ} (a b : FABL.F₂Cube n)
  (hab : (a, b) ≠ (0, 0))
  (hdisjoint :
    Disjoint (FABL.f₂Support a)
      (FABL.f₂Support b))
  (hcard :
    (FABL.f₂Support a).card +
        (FABL.f₂Support b).card <
      n) :
  b ≠
    CryptBoolean.completeQuadraticPolarFrequency
      a

Disjoint directions and frequencies whose combined support omits a
coordinate cannot coincide through the complete-quadratic polar map.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.booleanDerivative_domainTranslate {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (z a : FABL.F₂Cube n) :
  FABL.booleanDerivative (FABL.domainTranslate f z) a =
    FABL.domainTranslate (FABL.booleanDerivative f a) z

theorem CryptBoolean.booleanDerivative_domainTranslate
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (z a : FABL.F₂Cube n) :
  FABL.booleanDerivative
      (FABL.domainTranslate f z) a =
    FABL.domainTranslate
      (FABL.booleanDerivative f a) z

Binary differentiation commutes with translation of the input domain.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_domainTranslate_iff
  {n : ℕ} (l k : ℕ) (f : CryptBoolean.BooleanFunction n)
  (z : FABL.F₂Cube n) (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k
      (FABL.domainTranslate f z) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_domainTranslate_iff
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (z : FABL.F₂Cube n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k (FABL.domainTranslate f z) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f

Translating the input preserves propagation criteria at every fixed
coordinate order in the nonvacuous Walsh-characterization range.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_add_affineFunction_iff
  {n : ℕ} (l k : ℕ) (f : CryptBoolean.BooleanFunction n) (c : FABL.𝔽₂)
  (u : FABL.F₂Cube n) (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k
      (f + FABL.affineFunction c u) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_add_affineFunction_iff
  {n : ℕ} (l k : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (c : FABL.𝔽₂) (u : FABL.F₂Cube n)
  (hparameters : l + k ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k (f + FABL.affineFunction c u) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f

Adding an affine function preserves propagation criteria at every fixed
order in the nonvacuous Walsh-characterization range.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_completeQuadraticBit
  {n : ℕ} (l k : ℕ) (hparameters : l + k < n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k
    FABL.completeQuadraticBit

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_completeQuadraticBit
  {n : ℕ} (l k : ℕ)
  (hparameters : l + k < n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l k FABL.completeQuadraticBit

The complete quadratic function satisfies `PC(l)` of order `k` whenever
the eligible direction and frequency supports cannot cover every coordinate.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_completeQuadraticBit_add_affineFunction
  {n : ℕ} (l k : ℕ) (c : FABL.𝔽₂) (u : FABL.F₂Cube n)
  (hparameters : l + k < n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k
    (FABL.completeQuadraticBit + FABL.affineFunction c u)

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_completeQuadraticBit_add_affineFunction
  {n : ℕ} (l k : ℕ) (c : FABL.𝔽₂)
  (u : FABL.F₂Cube n)
  (hparameters : l + k < n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l k
    (FABL.completeQuadraticBit +
      FABL.affineFunction c u)

Every affine translate of the complete quadratic function satisfies the
same order propagation criterion below the support-covering boundary.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderCompleteQuadratic.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_completeQuadraticBit_add_affineFunction
  {n : ℕ} (l : ℕ) (c : FABL.𝔽₂) (u : FABL.F₂Cube n) (hl : l + 2 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l - 2)
    (FABL.completeQuadraticBit + FABL.affineFunction c u)

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_completeQuadraticBit_add_affineFunction
  {n : ℕ} (l : ℕ) (c : FABL.𝔽₂)
  (u : FABL.F₂Cube n) (hl : l + 2 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l (n - l - 2)
    (FABL.completeQuadraticBit +
      FABL.affineFunction c u)

The complete quadratic function plus an arbitrary affine function
satisfies Carlet's extremal criterion `PC(l)` of order `n-l-2`.

theoremdefined in CryptBoolean/Carlet/Chapter08/CoordinateQuadraticRigidity.lean

complete

theorem CryptBoolean.completeQuadraticBit_finAppend {r s : ℕ}
  (x : FABL.F₂Cube r) (y : FABL.F₂Cube s) :
  FABL.completeQuadraticBit (Fin.append x y) =
    FABL.completeQuadraticBit x + FABL.completeQuadraticBit y +
      (∑ i, x i) * ∑ j, y j

theorem CryptBoolean.completeQuadraticBit_finAppend
  {r s : ℕ} (x : FABL.F₂Cube r)
  (y : FABL.F₂Cube s) :
  FABL.completeQuadraticBit
      (Fin.append x y) =
    FABL.completeQuadraticBit x +
        FABL.completeQuadraticBit y +
      (∑ i, x i) * ∑ j, y j

The complete quadratic function on appended coordinate blocks is the sum
of the two block quadratics and their coordinate-sum product.

theoremdefined in CryptBoolean/Carlet/Chapter08/CoordinateQuadraticRigidity.lean

complete

theorem CryptBoolean.secondBooleanDerivative_same_direction {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  CryptBoolean.secondBooleanDerivative f a a = 0

theorem CryptBoolean.secondBooleanDerivative_same_direction
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.secondBooleanDerivative f a
      a =
    0

A second derivative in the same direction vanishes.

theoremdefined in CryptBoolean/Carlet/Chapter08/CoordinateQuadraticRigidity.lean

complete

theorem CryptBoolean.secondBooleanDerivative_add {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (a e : FABL.F₂Cube n) :
  CryptBoolean.secondBooleanDerivative (f + g) a e =
    CryptBoolean.secondBooleanDerivative f a e +
      CryptBoolean.secondBooleanDerivative g a e

theorem CryptBoolean.secondBooleanDerivative_add
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (a e : FABL.F₂Cube n) :
  CryptBoolean.secondBooleanDerivative
      (f + g) a e =
    CryptBoolean.secondBooleanDerivative f
        a e +
      CryptBoolean.secondBooleanDerivative
        g a e

Second differentiation distributes over pointwise addition.

theoremdefined in CryptBoolean/Carlet/Chapter08/CoordinateQuadraticRigidity.lean

complete

theorem CryptBoolean.secondBooleanDerivative_completeQuadraticBit_coordinateDirections_eq_one
  {n : ℕ} (i j : Fin n) (hij : i ≠ j) :
  CryptBoolean.secondBooleanDerivative FABL.completeQuadraticBit
      (CryptBoolean.coordinateDirection i)
      (CryptBoolean.coordinateDirection j) =
    1

theorem CryptBoolean.secondBooleanDerivative_completeQuadraticBit_coordinateDirections_eq_one
  {n : ℕ} (i j : Fin n) (hij : i ≠ j) :
  CryptBoolean.secondBooleanDerivative
      FABL.completeQuadraticBit
      (CryptBoolean.coordinateDirection i)
      (CryptBoolean.coordinateDirection
        j) =
    1

Distinct coordinate directions have constant mixed derivative one for
the complete quadratic function.

theoremdefined in CryptBoolean/Carlet/Chapter08/CoordinateQuadraticRigidity.lean

complete

theorem CryptBoolean.exists_completeQuadraticBit_add_affineFunction_of_coordinateSecondDerivatives_eq_one
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hpairs :
    ∀ (i j : Fin n),
      i ≠ j →
        CryptBoolean.secondBooleanDerivative f
            (CryptBoolean.coordinateDirection i)
            (CryptBoolean.coordinateDirection j) =
          1) :
  ∃ c u, f = FABL.completeQuadraticBit + FABL.affineFunction c u

theorem CryptBoolean.exists_completeQuadraticBit_add_affineFunction_of_coordinateSecondDerivatives_eq_one
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hpairs :
    ∀ (i j : Fin n),
      i ≠ j →
        CryptBoolean.secondBooleanDerivative
            f
            (CryptBoolean.coordinateDirection
              i)
            (CryptBoolean.coordinateDirection
              j) =
          1) :
  ∃ c u,
    f =
      FABL.completeQuadraticBit +
        FABL.affineFunction c u

A Boolean function whose mixed derivatives in every pair of distinct
coordinate directions equal one is the complete quadratic function plus an
affine function.

theoremdefined in CryptBoolean/Carlet/Chapter08/CoordinateQuadraticRigidity.lean

complete

theorem CryptBoolean.exists_firstBlockSlice_completeQuadraticBit_add_affineFunction
  {r s : ℕ} (c : FABL.𝔽₂) (u : FABL.F₂Cube (r + s))
  (y : FABL.F₂Cube s) :
  ∃ c' u',
    CryptBoolean.firstBlockSlice
        (FABL.completeQuadraticBit + FABL.affineFunction c u) y =
      FABL.completeQuadraticBit + FABL.affineFunction c' u'

theorem CryptBoolean.exists_firstBlockSlice_completeQuadraticBit_add_affineFunction
  {r s : ℕ} (c : FABL.𝔽₂)
  (u : FABL.F₂Cube (r + s))
  (y : FABL.F₂Cube s) :
  ∃ c' u',
    CryptBoolean.firstBlockSlice
        (FABL.completeQuadraticBit +
          FABL.affineFunction c u)
        y =
      FABL.completeQuadraticBit +
        FABL.affineFunction c' u'

Every two-coordinate-block slice of the complete quadratic function plus
an affine function is again a complete quadratic function plus an affine
function.

theoremdefined in CryptBoolean/Carlet/Chapter08/CoordinateQuadraticRigidity.lean

complete

theorem CryptBoolean.isBent_firstBlockSlice_completeQuadraticBit_add_affineFunction
  {r s : ℕ} (hr : Even r) (c : FABL.𝔽₂) (u : FABL.F₂Cube (r + s))
  (y : FABL.F₂Cube s) :
  CryptBoolean.IsBent
    (CryptBoolean.firstBlockSlice
      (FABL.completeQuadraticBit + FABL.affineFunction c u) y)

theorem CryptBoolean.isBent_firstBlockSlice_completeQuadraticBit_add_affineFunction
  {r s : ℕ} (hr : Even r) (c : FABL.𝔽₂)
  (u : FABL.F₂Cube (r + s))
  (y : FABL.F₂Cube s) :
  CryptBoolean.IsBent
    (CryptBoolean.firstBlockSlice
      (FABL.completeQuadraticBit +
        FABL.affineFunction c u)
      y)

In even first-block dimension, all first-block slices of the complete
quadratic function plus an affine function are bent.

defdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

def CryptBoolean.cubeReindexLinearEquiv {r s : ℕ} (e : Fin r ≃ Fin s) :
  FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] FABL.F₂Cube s

def CryptBoolean.cubeReindexLinearEquiv
  {r s : ℕ} (e : Fin r ≃ Fin s) :
  FABL.F₂Cube r ≃ₗ[FABL.𝔽₂] FABL.F₂Cube s

Reindex a binary cube along an equivalence of its coordinate types.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.hammingWeight_comp_cubeReindexLinearEquiv {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s) (e : Fin r ≃ Fin s) :
  CryptBoolean.hammingWeight
      (f ∘ ⇑(CryptBoolean.cubeReindexLinearEquiv e)) =
    CryptBoolean.hammingWeight f

theorem CryptBoolean.hammingWeight_comp_cubeReindexLinearEquiv
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (e : Fin r ≃ Fin s) :
  CryptBoolean.hammingWeight
      (f ∘
        ⇑(CryptBoolean.cubeReindexLinearEquiv
            e)) =
    CryptBoolean.hammingWeight f

Reindexing the coordinates of a Boolean function preserves its Hamming
weight.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.isBalanced_comp_cubeReindexLinearEquiv_iff {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s) (e : Fin r ≃ Fin s) :
  CryptBoolean.IsBalanced
      (f ∘ ⇑(CryptBoolean.cubeReindexLinearEquiv e)) ↔
    CryptBoolean.IsBalanced f

theorem CryptBoolean.isBalanced_comp_cubeReindexLinearEquiv_iff
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (e : Fin r ≃ Fin s) :
  CryptBoolean.IsBalanced
      (f ∘
        ⇑(CryptBoolean.cubeReindexLinearEquiv
            e)) ↔
    CryptBoolean.IsBalanced f

Reindexing the coordinates of a Boolean function preserves balancedness.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.card_f₂Support_cubeReindexLinearEquiv {r s : ℕ}
  (e : Fin r ≃ Fin s) (a : FABL.F₂Cube r) :
  (FABL.f₂Support ((CryptBoolean.cubeReindexLinearEquiv e) a)).card =
    (FABL.f₂Support a).card

theorem CryptBoolean.card_f₂Support_cubeReindexLinearEquiv
  {r s : ℕ} (e : Fin r ≃ Fin s)
  (a : FABL.F₂Cube r) :
  (FABL.f₂Support
        ((CryptBoolean.cubeReindexLinearEquiv
            e)
          a)).card =
    (FABL.f₂Support a).card

Coordinate reindexing preserves the support cardinality of a direction.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.f₂Support_cubeReindexLinearEquiv {r s : ℕ}
  (e : Fin r ≃ Fin s) (a : FABL.F₂Cube r) :
  FABL.f₂Support ((CryptBoolean.cubeReindexLinearEquiv e) a) =
    Finset.map e.toEmbedding (FABL.f₂Support a)

theorem CryptBoolean.f₂Support_cubeReindexLinearEquiv
  {r s : ℕ} (e : Fin r ≃ Fin s)
  (a : FABL.F₂Cube r) :
  FABL.f₂Support
      ((CryptBoolean.cubeReindexLinearEquiv
          e)
        a) =
    Finset.map e.toEmbedding
      (FABL.f₂Support a)

Coordinate reindexing maps the support of a direction by the same
coordinate equivalence.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.booleanDerivative_comp_cubeReindexLinearEquiv {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s) (e : Fin r ≃ Fin s)
  (a : FABL.F₂Cube r) :
  FABL.booleanDerivative (f ∘ ⇑(CryptBoolean.cubeReindexLinearEquiv e))
      a =
    FABL.booleanDerivative f
        ((CryptBoolean.cubeReindexLinearEquiv e) a) ∘
      ⇑(CryptBoolean.cubeReindexLinearEquiv e)

theorem CryptBoolean.booleanDerivative_comp_cubeReindexLinearEquiv
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (e : Fin r ≃ Fin s)
  (a : FABL.F₂Cube r) :
  FABL.booleanDerivative
      (f ∘
        ⇑(CryptBoolean.cubeReindexLinearEquiv
            e))
      a =
    FABL.booleanDerivative f
        ((CryptBoolean.cubeReindexLinearEquiv
            e)
          a) ∘
      ⇑(CryptBoolean.cubeReindexLinearEquiv
          e)

Binary differentiation commutes with coordinate reindexing.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterion_comp_cubeReindexLinearEquiv_iff
  {r s l : ℕ} (f : CryptBoolean.BooleanFunction s) (e : Fin r ≃ Fin s) :
  CryptBoolean.SatisfiesPropagationCriterion l
      (f ∘ ⇑(CryptBoolean.cubeReindexLinearEquiv e)) ↔
    CryptBoolean.SatisfiesPropagationCriterion l f

theorem CryptBoolean.satisfiesPropagationCriterion_comp_cubeReindexLinearEquiv_iff
  {r s l : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (e : Fin r ≃ Fin s) :
  CryptBoolean.SatisfiesPropagationCriterion
      l
      (f ∘
        ⇑(CryptBoolean.cubeReindexLinearEquiv
            e)) ↔
    CryptBoolean.SatisfiesPropagationCriterion
      l f

Coordinate reindexing preserves every propagation criterion.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_comp_cubeReindexLinearEquiv_iff
  {r s l k : ℕ} (f : CryptBoolean.BooleanFunction s) (e : Fin r ≃ Fin s)
  (hparameters : l + k ≤ r) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k
      (f ∘ ⇑(CryptBoolean.cubeReindexLinearEquiv e)) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_comp_cubeReindexLinearEquiv_iff
  {r s l k : ℕ}
  (f : CryptBoolean.BooleanFunction s)
  (e : Fin r ≃ Fin s)
  (hparameters : l + k ≤ r) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k
      (f ∘
        ⇑(CryptBoolean.cubeReindexLinearEquiv
            e)) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f

Reindexing the input coordinates preserves every propagation criterion
at every fixed-coordinate order.

defdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

def CryptBoolean.embeddingFinsetEquiv {n r : ℕ} (e : Fin r ↪ Fin n) :
  Fin r ≃ ↥(Finset.map e Finset.univ)

def CryptBoolean.embeddingFinsetEquiv
  {n r : ℕ} (e : Fin r ↪ Fin n) :
  Fin r ≃ ↥(Finset.map e Finset.univ)

The coordinate image of an embedding, indexed by its original finite
domain.

defdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

def CryptBoolean.canonicalEmbeddingReindexEquiv {n r : ℕ}
  (e : Fin r ↪ Fin n) : Fin r ≃ Fin (Finset.map e Finset.univ).card

def CryptBoolean.canonicalEmbeddingReindexEquiv
  {n r : ℕ} (e : Fin r ↪ Fin n) :
  Fin r ≃
    Fin (Finset.map e Finset.univ).card

The change from an arbitrary enumeration of free coordinates to FABL's
canonical increasing enumeration of the same finite set.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.freeCoordinateEmbedding_canonicalEmbeddingReindexEquiv
  {n r : ℕ} (e : Fin r ↪ Fin n) (i : Fin r) :
  (FABL.freeCoordinateEmbedding (Finset.map e Finset.univ))
      ((CryptBoolean.canonicalEmbeddingReindexEquiv e) i) =
    e i

theorem CryptBoolean.freeCoordinateEmbedding_canonicalEmbeddingReindexEquiv
  {n r : ℕ} (e : Fin r ↪ Fin n)
  (i : Fin r) :
  (FABL.freeCoordinateEmbedding
        (Finset.map e Finset.univ))
      ((CryptBoolean.canonicalEmbeddingReindexEquiv
          e)
        i) =
    e i

defdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

def CryptBoolean.embeddedCoordinateRestriction {n r : ℕ}
  (f : CryptBoolean.BooleanFunction n) (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) : CryptBoolean.BooleanFunction r

def CryptBoolean.embeddedCoordinateRestriction
  {n r : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.BooleanFunction r

Restrict a Boolean function along an arbitrary injective enumeration of
free coordinates, taking every other value from an ambient point.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterion_embeddedCoordinateRestriction_of_order
  {n r k l : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f)
  (hrk : r + k = n) (e : Fin r ↪ Fin n) (x₀ : FABL.F₂Cube n) :
  CryptBoolean.SatisfiesPropagationCriterion l
    (CryptBoolean.embeddedCoordinateRestriction f e x₀)

theorem CryptBoolean.satisfiesPropagationCriterion_embeddedCoordinateRestriction_of_order
  {n r k l : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f)
  (hrk : r + k = n) (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.SatisfiesPropagationCriterion
    l
    (CryptBoolean.embeddedCoordinateRestriction
      f e x₀)

An arbitrary free-coordinate enumeration realizes the propagation
criterion supplied by the complementary ambient coordinate order.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_embeddedCoordinateRestriction
  {n r l k k' : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f)
  (horders : r + k = n + k') (e : Fin r ↪ Fin n) (x₀ : FABL.F₂Cube n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k'
    (CryptBoolean.embeddedCoordinateRestriction f e x₀)

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_embeddedCoordinateRestriction
  {n r l k k' : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f)
  (horders : r + k = n + k')
  (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l k'
    (CryptBoolean.embeddedCoordinateRestriction
      f e x₀)

Restricting an order propagation criterion to an embedded coordinate
subcube subtracts the coordinates already fixed outside that subcube.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.isBent_comp_cubeReindexLinearEquiv_iff {r s : ℕ}
  (hrs : r = s) (f : CryptBoolean.BooleanFunction s)
  (e : Fin r ≃ Fin s) :
  CryptBoolean.IsBent (f ∘ ⇑(CryptBoolean.cubeReindexLinearEquiv e)) ↔
    CryptBoolean.IsBent f

theorem CryptBoolean.isBent_comp_cubeReindexLinearEquiv_iff
  {r s : ℕ} (hrs : r = s)
  (f : CryptBoolean.BooleanFunction s)
  (e : Fin r ≃ Fin s) :
  CryptBoolean.IsBent
      (f ∘
        ⇑(CryptBoolean.cubeReindexLinearEquiv
            e)) ↔
    CryptBoolean.IsBent f

Reindexing equivalent coordinate types preserves bentness.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.isBent_embeddedCoordinateRestriction_iff {n r : ℕ}
  (f : CryptBoolean.BooleanFunction n) (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.IsBent
      (CryptBoolean.embeddedCoordinateRestriction f e x₀) ↔
    CryptBoolean.IsBent
      (CryptBoolean.coordinateRestriction f (Finset.map e Finset.univ)
        (CryptBoolean.coordinateFixedSignAssignment
          (Finset.map e Finset.univ) x₀))

theorem CryptBoolean.isBent_embeddedCoordinateRestriction_iff
  {n r : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.IsBent
      (CryptBoolean.embeddedCoordinateRestriction
        f e x₀) ↔
    CryptBoolean.IsBent
      (CryptBoolean.coordinateRestriction
        f (Finset.map e Finset.univ)
        (CryptBoolean.coordinateFixedSignAssignment
          (Finset.map e Finset.univ) x₀))

Bentness of an arbitrarily enumerated coordinate restriction agrees with
bentness of the canonical restriction on the same free-coordinate set.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.isBent_embeddedCoordinateRestriction_of_order_dimension
  {n r k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder r k f)
  (hrk : r + k = n) (e : Fin r ↪ Fin n) (x₀ : FABL.F₂Cube n) :
  CryptBoolean.IsBent
    (CryptBoolean.embeddedCoordinateRestriction f e x₀)

theorem CryptBoolean.isBent_embeddedCoordinateRestriction_of_order_dimension
  {n r k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      r k f)
  (hrk : r + k = n) (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.IsBent
    (CryptBoolean.embeddedCoordinateRestriction
      f e x₀)

Full-level propagation at the complementary coordinate order makes every
arbitrarily enumerated restriction bent.

theoremdefined in CryptBoolean/Carlet/Chapter08/EmbeddedCoordinateRestrictions.lean

complete

theorem CryptBoolean.isBent_embeddedCoordinateRestriction_of_order_pred_two
  {n r k : ℕ} (f : CryptBoolean.BooleanFunction n)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder (r - 2) k f)
  (hrk : r + k = n) (hr : 4 ≤ r) (heven : Even r) (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.IsBent
    (CryptBoolean.embeddedCoordinateRestriction f e x₀)

theorem CryptBoolean.isBent_embeddedCoordinateRestriction_of_order_pred_two
  {n r k : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      (r - 2) k f)
  (hrk : r + k = n) (hr : 4 ≤ r)
  (heven : Even r) (e : Fin r ↪ Fin n)
  (x₀ : FABL.F₂Cube n) :
  CryptBoolean.IsBent
    (CryptBoolean.embeddedCoordinateRestriction
      f e x₀)

For an even restriction dimension at least four, `PC(r-2)` at the
complementary coordinate order makes every arbitrarily enumerated restriction
bent.

defdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderPeriod.lean

complete

def CryptBoolean.standardPredThreeDirection (k : ℕ) :
  FABL.F₂Cube (2 * k + 2)

def CryptBoolean.standardPredThreeDirection
  (k : ℕ) : FABL.F₂Cube (2 * k + 2)

The standard weight-`2k` direction in dimension `2k+2`, with its final
two coordinates equal to zero.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderPeriod.lean

complete

theorem CryptBoolean.false_of_satisfiesPropagationCriterionOfOrder_pred_three_of_standardDirection_linearStructure
  (k : ℕ) (hk : 3 ≤ k) (f : CryptBoolean.BooleanFunction (2 * k + 2))
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder (2 * k - 1) 1 f)
  (hperiod :
    FABL.booleanDerivative f
        (CryptBoolean.standardPredThreeDirection k) =
      0) :
  False

theorem CryptBoolean.false_of_satisfiesPropagationCriterionOfOrder_pred_three_of_standardDirection_linearStructure
  (k : ℕ) (hk : 3 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 2))
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      (2 * k - 1) 1 f)
  (hperiod :
    FABL.booleanDerivative f
        (CryptBoolean.standardPredThreeDirection
          k) =
      0) :
  False

In dimension `2k+2` with `k≥3`, the standard weight-`2k` direction
cannot be a linear structure of a function satisfying `PC(2k-1)` of order
one.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterion_firstBlockSlice_of_order_one
  {n : ℕ} (f : CryptBoolean.BooleanFunction (n + 1)) (l : ℕ)
  (hparameters : l + 1 ≤ n + 1)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder l 1 f)
  (b : FABL.𝔽₂) :
  CryptBoolean.SatisfiesPropagationCriterion l
    (CryptBoolean.firstBlockSlice f (CryptBoolean.singletonF₂Cube b))

theorem CryptBoolean.satisfiesPropagationCriterion_firstBlockSlice_of_order_one
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (l : ℕ) (hparameters : l + 1 ≤ n + 1)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l 1 f)
  (b : FABL.𝔽₂) :
  CryptBoolean.SatisfiesPropagationCriterion
    l
    (CryptBoolean.firstBlockSlice f
      (CryptBoolean.singletonF₂Cube b))

Fixing the last coordinate of a function satisfying `PC(l)` of order one
produces a function satisfying `PC(l)`.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.isLinearStructure_or_isBalanced_of_satisfiesPropagationCriterion_pred_two_odd
  (k : ℕ) (hk : 1 ≤ k) (f : CryptBoolean.BooleanFunction (2 * k + 1))
  (hf : CryptBoolean.SatisfiesPropagationCriterion (2 * k - 1) f)
  (a : FABL.F₂Cube (2 * k + 1)) (ha : a ≠ 0) :
  CryptBoolean.IsLinearStructure f a ∨
    CryptBoolean.IsBalanced (FABL.booleanDerivative f a)

theorem CryptBoolean.isLinearStructure_or_isBalanced_of_satisfiesPropagationCriterion_pred_two_odd
  (k : ℕ) (hk : 1 ≤ k)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 1))
  (hf :
    CryptBoolean.SatisfiesPropagationCriterion
      (2 * k - 1) f)
  (a : FABL.F₂Cube (2 * k + 1))
  (ha : a ≠ 0) :
  CryptBoolean.IsLinearStructure f a ∨
    CryptBoolean.IsBalanced
      (FABL.booleanDerivative f a)

In odd dimension, the extremal propagation criterion makes every
nonzero derivative either constant or balanced.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.hammingWeight_eq_add_firstBlockSlices {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1)) :
  CryptBoolean.hammingWeight f =
    CryptBoolean.hammingWeight
        (CryptBoolean.firstBlockSlice f
          (CryptBoolean.singletonF₂Cube 0)) +
      CryptBoolean.hammingWeight
        (CryptBoolean.firstBlockSlice f
          (CryptBoolean.singletonF₂Cube 1))

theorem CryptBoolean.hammingWeight_eq_add_firstBlockSlices
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction
      (n + 1)) :
  CryptBoolean.hammingWeight f =
    CryptBoolean.hammingWeight
        (CryptBoolean.firstBlockSlice f
          (CryptBoolean.singletonF₂Cube
            0)) +
      CryptBoolean.hammingWeight
        (CryptBoolean.firstBlockSlice f
          (CryptBoolean.singletonF₂Cube
            1))

Hamming weight splits over the two values of the last coordinate.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.isBalanced_of_firstBlockSlices {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1))
  (hzero :
    CryptBoolean.IsBalanced
      (CryptBoolean.firstBlockSlice f (CryptBoolean.singletonF₂Cube 0)))
  (hone :
    CryptBoolean.IsBalanced
      (CryptBoolean.firstBlockSlice f
        (CryptBoolean.singletonF₂Cube 1))) :
  CryptBoolean.IsBalanced f

theorem CryptBoolean.isBalanced_of_firstBlockSlices
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (hzero :
    CryptBoolean.IsBalanced
      (CryptBoolean.firstBlockSlice f
        (CryptBoolean.singletonF₂Cube 0)))
  (hone :
    CryptBoolean.IsBalanced
      (CryptBoolean.firstBlockSlice f
        (CryptBoolean.singletonF₂Cube
          1))) :
  CryptBoolean.IsBalanced f

Balancedness glues across the two values of the last coordinate.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.firstBlockSlice_eq_complement_of_isBalanced {n : ℕ}
  (f : CryptBoolean.BooleanFunction (n + 1))
  (hf : CryptBoolean.IsBalanced f) (c : FABL.𝔽₂)
  (hzero :
    CryptBoolean.firstBlockSlice f (CryptBoolean.singletonF₂Cube 0) =
      fun x => c) :
  CryptBoolean.firstBlockSlice f (CryptBoolean.singletonF₂Cube 1) =
    fun x => c + 1

theorem CryptBoolean.firstBlockSlice_eq_complement_of_isBalanced
  {n : ℕ}
  (f :
    CryptBoolean.BooleanFunction (n + 1))
  (hf : CryptBoolean.IsBalanced f)
  (c : FABL.𝔽₂)
  (hzero :
    CryptBoolean.firstBlockSlice f
        (CryptBoolean.singletonF₂Cube 0) =
      fun x => c) :
  CryptBoolean.firstBlockSlice f
      (CryptBoolean.singletonF₂Cube 1) =
    fun x => c + 1

If a balanced function is constant on one last-coordinate slice, it is
the complementary constant on the other slice.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_comp_coordinateSwapLinearEquiv_iff
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l k : ℕ)
  (hparameters : l + k ≤ n) (i j : Fin n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l k
      (f ∘ ⇑(CryptBoolean.coordinateSwapLinearEquiv i j)) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_comp_coordinateSwapLinearEquiv_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l k : ℕ) (hparameters : l + k ≤ n)
  (i j : Fin n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k
      (f ∘
        ⇑(CryptBoolean.coordinateSwapLinearEquiv
            i j)) ↔
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f

Permuting two input coordinates preserves every propagation criterion
of order.

defdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

def CryptBoolean.lastTwoCoordinateProduct (m : ℕ) :
  CryptBoolean.BooleanFunction (m + 2)

def CryptBoolean.lastTwoCoordinateProduct
  (m : ℕ) :
  CryptBoolean.BooleanFunction (m + 2)

The product of the last two input coordinates.

defdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

def CryptBoolean.standardDirectionInsertion (r : ℕ) : FABL.F₂Cube (r + 4)

def CryptBoolean.standardDirectionInsertion
  (r : ℕ) : FABL.F₂Cube (r + 4)

The standard direction supported on all but the final two coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.false_of_satisfiesPropagationCriterionOfOrder_pred_three_of_standardDirection_product
  (k : ℕ) (f : CryptBoolean.BooleanFunction (2 * k + 4))
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder (2 * k + 1) 1 f)
  (hderivative :
    FABL.booleanDerivative f
        (CryptBoolean.standardDirectionInsertion (2 * k)) =
      CryptBoolean.lastTwoCoordinateProduct (2 * k + 2)) :
  False

theorem CryptBoolean.false_of_satisfiesPropagationCriterionOfOrder_pred_three_of_standardDirection_product
  (k : ℕ)
  (f :
    CryptBoolean.BooleanFunction
      (2 * k + 4))
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      (2 * k + 1) 1 f)
  (hderivative :
    FABL.booleanDerivative f
        (CryptBoolean.standardDirectionInsertion
          (2 * k)) =
      CryptBoolean.lastTwoCoordinateProduct
        (2 * k + 2)) :
  False

The nonzero quadratic derivative branch is impossible at extremal
order one.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderBent.lean

complete

theorem CryptBoolean.isBent_of_satisfiesPropagationCriterionOfOrder_pred_three_of_even
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (hn : 8 ≤ n)
  (heven : Even n)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder (n - 3) 1 f) :
  CryptBoolean.IsBent f

theorem CryptBoolean.isBent_of_satisfiesPropagationCriterionOfOrder_pred_three_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 8 ≤ n) (heven : Even n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      (n - 3) 1 f) :
  CryptBoolean.IsBent f

Carlet Proposition 4: in even dimension at least eight, `PC(n-3)` of
order one forces bentness.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_dimension_completeQuadraticBit_add_affineFunction
  {n : ℕ} (l : ℕ) (heven : Even l) (hl : l ≤ n) (c : FABL.𝔽₂)
  (u : FABL.F₂Cube n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l)
    (FABL.completeQuadraticBit + FABL.affineFunction c u)

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_dimension_completeQuadraticBit_add_affineFunction
  {n : ℕ} (l : ℕ) (heven : Even l)
  (hl : l ≤ n) (c : FABL.𝔽₂)
  (u : FABL.F₂Cube n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    l (n - l)
    (FABL.completeQuadraticBit +
      FABL.affineFunction c u)

The complete quadratic function plus an affine summand satisfies the
maximal coordinate order at every even propagation level.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.exists_completeQuadraticBit_add_affineFunction_of_order_dimension
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hl : 2 ≤ l)
  (heven : Even l) (hlRange : l + 2 ≤ n)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l) f) :
  ∃ c u, f = FABL.completeQuadraticBit + FABL.affineFunction c u

theorem CryptBoolean.exists_completeQuadraticBit_add_affineFunction_of_order_dimension
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hl : 2 ≤ l) (heven : Even l)
  (hlRange : l + 2 ≤ n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l (n - l) f) :
  ∃ c u,
    f =
      FABL.completeQuadraticBit +
        FABL.affineFunction c u

Carlet Proposition 2, necessary direction: at a positive even level, the
maximal coordinate order forces the complete quadratic function up to an
affine summand.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_dimension_iff_completeQuadratic_add_affine
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hl : 2 ≤ l)
  (heven : Even l) (hlRange : l + 2 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l) f ↔
    ∃ c u, f = FABL.completeQuadraticBit + FABL.affineFunction c u

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_dimension_iff_completeQuadratic_add_affine
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hl : 2 ≤ l) (heven : Even l)
  (hlRange : l + 2 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l (n - l) f ↔
    ∃ c u,
      f =
        FABL.completeQuadraticBit +
          FABL.affineFunction c u

Carlet Proposition 2: at a positive even level, maximal coordinate-order
propagation is equivalent to the complete quadratic function up to an affine
summand.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_add_two_of_even
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l k : ℕ) (hl : 2 ≤ l)
  (heven : Even l) (hparameters : l + k + 2 = n)
  (hf : CryptBoolean.SatisfiesPropagationCriterionOfOrder l k f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder (l + 2) k f

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_add_two_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l k : ℕ) (hl : 2 ≤ l) (heven : Even l)
  (hparameters : l + k + 2 = n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l k f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    (l + 2) k f

If every restriction to `l+2` free coordinates satisfies `PC(l)`, with
`l` positive and even, then every such restriction is bent and hence satisfies
the full propagation criterion `PC(l+2)`.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_add_two_of_even
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hl : 2 ≤ l)
  (heven : Even l) (hlRange : l + 2 ≤ n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l - 2) f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder (l + 2) (n - l - 2)
    f

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_add_two_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hl : 2 ≤ l) (heven : Even l)
  (hlRange : l + 2 ≤ n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l (n - l - 2) f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    (l + 2) (n - l - 2) f

At Carlet's extremal order, a positive even propagation level upgrades by
two while keeping the same fixed-coordinate order.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_iff_completeQuadratic_of_even
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hl : 0 < l)
  (heven : Even l) (hlRange : l + 4 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l - 2) f ↔
    ∃ c u, f = FABL.completeQuadraticBit + FABL.affineFunction c u

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_iff_completeQuadratic_of_even
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hl : 0 < l) (heven : Even l)
  (hlRange : l + 4 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l (n - l - 2) f ↔
    ∃ c u,
      f =
        FABL.completeQuadraticBit +
          FABL.affineFunction c u

The even-level case of Carlet Theorem 5: two below maximal coordinate
order, only the complete quadratic function and its affine translates occur.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_add_three_of_odd
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hl : 5 ≤ l)
  (hodd : Odd l) (hlRange : l + 5 ≤ n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l - 2) f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder (l + 3) (n - l - 3)
    f

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_add_three_of_odd
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hl : 5 ≤ l) (hodd : Odd l)
  (hlRange : l + 5 ≤ n)
  (hf :
    CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l (n - l - 2) f) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
    (l + 3) (n - l - 3) f

At Carlet's extremal order, an odd propagation level at least five
upgrades by three while reducing the fixed-coordinate order by one.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_iff_completeQuadratic_of_odd
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ) (hl : 5 ≤ l)
  (hodd : Odd l) (hlRange : l + 5 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l - 2) f ↔
    ∃ c u, f = FABL.completeQuadraticBit + FABL.affineFunction c u

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_iff_completeQuadratic_of_odd
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ) (hl : 5 ≤ l) (hodd : Odd l)
  (hlRange : l + 5 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l (n - l - 2) f ↔
    ∃ c u,
      f =
        FABL.completeQuadraticBit +
          FABL.affineFunction c u

The odd-level case of Carlet Theorem 5: two below maximal coordinate
order, only the complete quadratic function and its affine translates occur.

theoremdefined in CryptBoolean/Carlet/Chapter08/ExtremalOrderNecessity.lean

complete

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_iff_completeQuadratic
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (l : ℕ)
  (hrange :
    6 ≤ n ∧ 0 < l ∧ Even l ∧ l + 4 ≤ n ∨
      10 ≤ n ∧ 5 ≤ l ∧ Odd l ∧ l + 5 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder l (n - l - 2) f ↔
    ∃ c u, f = FABL.completeQuadraticBit + FABL.affineFunction c u

theorem CryptBoolean.satisfiesPropagationCriterionOfOrder_extremal_iff_completeQuadratic
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (l : ℕ)
  (hrange :
    6 ≤ n ∧ 0 < l ∧ Even l ∧ l + 4 ≤ n ∨
      10 ≤ n ∧
        5 ≤ l ∧ Odd l ∧ l + 5 ≤ n) :
  CryptBoolean.SatisfiesPropagationCriterionOfOrder
      l (n - l - 2) f ↔
    ∃ c u,
      f =
        FABL.completeQuadraticBit +
          FABL.affineFunction c u

Carlet Theorem 5: in the stated even and odd ranges, the extremal
propagation criterion characterizes the complete quadratic function up to an
affine summand.