6.5. Secondary constructions🔗

Theorem6.5.1

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.1.1

Loading preview

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

Statement uses 5

Statement dependency previews

Preview

Theorem 1.4.6

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-7tarannikovresilient-constructionpage-125fidelity-exact

Tarannikov's elementary construction (Carlet, p. 125). Let g:V_r\to\mathbb F_2 and define h(x_1,\ldots,x_r,z) =z\oplus g(x_1,\ldots,x_{r-1},x_r\oplus z). Its Walsh transform is zero when the last two frequency coordinates are equal and otherwise is twice the corresponding Walsh coefficient of g. Consequently, \operatorname{nl}(h)=2\operatorname{nl}(g). If g is m-resilient, then h is m-resilient. If additionally W_g(a,1)=0 for every a of weight at most m, then h is (m+1)-resilient. If \deg_{\mathrm{alg}}g\ge1, then \deg_{\mathrm{alg}}h=\deg_{\mathrm{alg}}g. The direction supported on the last two coordinates is a nonzero linear structure of h.

Lean code for Theorem6.5.1●23 declarations

defdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

def CryptBoolean.tarannikovPenultimateIndex (r : ℕ) : Fin (r + 2)

def CryptBoolean.tarannikovPenultimateIndex
  (r : ℕ) : Fin (r + 2)

The penultimate coordinate in an `(r + 2)`-dimensional cube.

defdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

def CryptBoolean.tarannikovLastIndex (r : ℕ) : Fin (r + 2)

def CryptBoolean.tarannikovLastIndex (r : ℕ) :
  Fin (r + 2)

The last coordinate in an `(r + 2)`-dimensional cube.

defdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

def CryptBoolean.tarannikovShearLinearMap (r : ℕ) :
  FABL.F₂Cube (r + 2) →ₗ[FABL.𝔽₂] FABL.F₂Cube (r + 2)

def CryptBoolean.tarannikovShearLinearMap
  (r : ℕ) :
  FABL.F₂Cube (r + 2) →ₗ[FABL.𝔽₂]
    FABL.F₂Cube (r + 2)

The linear endomorphism underlying the Tarannikov shear.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.tarannikovShearLinearMap_involutive (r : ℕ) :
  Function.Involutive ⇑(CryptBoolean.tarannikovShearLinearMap r)

theorem CryptBoolean.tarannikovShearLinearMap_involutive
  (r : ℕ) :
  Function.Involutive
    ⇑(CryptBoolean.tarannikovShearLinearMap
        r)

The Tarannikov shear is an involution.

defdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

def CryptBoolean.tarannikovShearLinearEquiv (r : ℕ) :
  FABL.F₂Cube (r + 2) ≃ₗ[FABL.𝔽₂] FABL.F₂Cube (r + 2)

def CryptBoolean.tarannikovShearLinearEquiv
  (r : ℕ) :
  FABL.F₂Cube (r + 2) ≃ₗ[FABL.𝔽₂]
    FABL.F₂Cube (r + 2)

The involutive shear that adds the final coordinate to the penultimate
coordinate.

defdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

def CryptBoolean.tarannikovCoordinates {r : ℕ} (x : FABL.F₂Cube r)
  (a z : FABL.𝔽₂) : FABL.F₂Cube (r + 2)

def CryptBoolean.tarannikovCoordinates {r : ℕ}
  (x : FABL.F₂Cube r) (a z : FABL.𝔽₂) :
  FABL.F₂Cube (r + 2)

The coordinate tuple consisting of an `r`-bit prefix and two final bits.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.tarannikovCoordinates_eq_append {r : ℕ} (x : FABL.F₂Cube r)
  (a z : FABL.𝔽₂) :
  CryptBoolean.tarannikovCoordinates x a z =
    Fin.append (Fin.append x (CryptBoolean.singletonF₂Cube a))
      (CryptBoolean.singletonF₂Cube z)

theorem CryptBoolean.tarannikovCoordinates_eq_append
  {r : ℕ} (x : FABL.F₂Cube r)
  (a z : FABL.𝔽₂) :
  CryptBoolean.tarannikovCoordinates x a
      z =
    Fin.append
      (Fin.append x
        (CryptBoolean.singletonF₂Cube a))
      (CryptBoolean.singletonF₂Cube z)

The tuple notation agrees with nested binary-cube append.

defdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

def CryptBoolean.tarannikovElementaryConstruction {r : ℕ}
  (g : CryptBoolean.BooleanFunction (r + 1)) :
  CryptBoolean.BooleanFunction (r + 2)

def CryptBoolean.tarannikovElementaryConstruction
  {r : ℕ}
  (g :
    CryptBoolean.BooleanFunction
      (r + 1)) :
  CryptBoolean.BooleanFunction (r + 2)

Tarannikov's elementary function is adding a parity variable followed by
the penultimate-coordinate shear.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.walshTransform_oneVariableParity_singletonF₂Cube
  (b : FABL.𝔽₂) :
  CryptBoolean.walshTransform CryptBoolean.oneVariableParity
      (CryptBoolean.singletonF₂Cube b) =
    if b = 1 then 2 else 0

theorem CryptBoolean.walshTransform_oneVariableParity_singletonF₂Cube
  (b : FABL.𝔽₂) :
  CryptBoolean.walshTransform
      CryptBoolean.oneVariableParity
      (CryptBoolean.singletonF₂Cube b) =
    if b = 1 then 2 else 0

The one-variable parity spectrum in bit coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.f₂DotProduct_tarannikovCoordinates {r : ℕ}
  (a x : FABL.F₂Cube r) (aᵣ aₙ xᵣ xₙ : FABL.𝔽₂) :
  FABL.f₂DotProduct (CryptBoolean.tarannikovCoordinates a aᵣ aₙ)
      (CryptBoolean.tarannikovCoordinates x xᵣ xₙ) =
    FABL.f₂DotProduct a x + aᵣ * xᵣ + aₙ * xₙ

theorem CryptBoolean.f₂DotProduct_tarannikovCoordinates
  {r : ℕ} (a x : FABL.F₂Cube r)
  (aᵣ aₙ xᵣ xₙ : FABL.𝔽₂) :
  FABL.f₂DotProduct
      (CryptBoolean.tarannikovCoordinates
        a aᵣ aₙ)
      (CryptBoolean.tarannikovCoordinates
        x xᵣ xₙ) =
    FABL.f₂DotProduct a x + aᵣ * xᵣ +
      aₙ * xₙ

Dot products split over Tarannikov coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.exists_eq_tarannikovCoordinates {r : ℕ}
  (u : FABL.F₂Cube (r + 2)) :
  ∃ x xᵣ xₙ, CryptBoolean.tarannikovCoordinates x xᵣ xₙ = u

theorem CryptBoolean.exists_eq_tarannikovCoordinates
  {r : ℕ} (u : FABL.F₂Cube (r + 2)) :
  ∃ x xᵣ xₙ,
    CryptBoolean.tarannikovCoordinates x
        xᵣ xₙ =
      u

Every vector has a prefix-and-two-bits presentation.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.f₂DotProduct_tarannikovShear {r : ℕ} (a : FABL.F₂Cube r)
  (aᵣ aₙ : FABL.𝔽₂) (u : FABL.F₂Cube (r + 2)) :
  FABL.f₂DotProduct (CryptBoolean.tarannikovCoordinates a aᵣ (aₙ + aᵣ))
      ((CryptBoolean.tarannikovShearLinearEquiv r) u) =
    FABL.f₂DotProduct (CryptBoolean.tarannikovCoordinates a aᵣ aₙ) u

theorem CryptBoolean.f₂DotProduct_tarannikovShear
  {r : ℕ} (a : FABL.F₂Cube r)
  (aᵣ aₙ : FABL.𝔽₂)
  (u : FABL.F₂Cube (r + 2)) :
  FABL.f₂DotProduct
      (CryptBoolean.tarannikovCoordinates
        a aᵣ (aₙ + aᵣ))
      ((CryptBoolean.tarannikovShearLinearEquiv
          r)
        u) =
    FABL.f₂DotProduct
      (CryptBoolean.tarannikovCoordinates
        a aᵣ aₙ)
      u

The dual-frequency shear for the Tarannikov coordinate change.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.walshTransform_tarannikovElementaryConstruction {r : ℕ}
  (g : CryptBoolean.BooleanFunction (r + 1)) (a : FABL.F₂Cube r)
  (aᵣ aₙ : FABL.𝔽₂) :
  CryptBoolean.walshTransform
      (CryptBoolean.tarannikovElementaryConstruction g)
      (CryptBoolean.tarannikovCoordinates a aᵣ aₙ) =
    if aₙ = aᵣ then 0
    else
      2 *
        CryptBoolean.walshTransform g
          (Fin.append a (CryptBoolean.singletonF₂Cube aᵣ))

theorem CryptBoolean.walshTransform_tarannikovElementaryConstruction
  {r : ℕ}
  (g :
    CryptBoolean.BooleanFunction (r + 1))
  (a : FABL.F₂Cube r) (aᵣ aₙ : FABL.𝔽₂) :
  CryptBoolean.walshTransform
      (CryptBoolean.tarannikovElementaryConstruction
        g)
      (CryptBoolean.tarannikovCoordinates
        a aᵣ aₙ) =
    if aₙ = aᵣ then 0
    else
      2 *
        CryptBoolean.walshTransform g
          (Fin.append a
            (CryptBoolean.singletonF₂Cube
              aᵣ))

Tarannikov's exact two-branch Walsh spectrum.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.nonlinearity_tarannikovElementaryConstruction {r : ℕ}
  (g : CryptBoolean.BooleanFunction (r + 1)) :
  CryptBoolean.nonlinearity
      (CryptBoolean.tarannikovElementaryConstruction g) =
    2 * CryptBoolean.nonlinearity g

theorem CryptBoolean.nonlinearity_tarannikovElementaryConstruction
  {r : ℕ}
  (g :
    CryptBoolean.BooleanFunction
      (r + 1)) :
  CryptBoolean.nonlinearity
      (CryptBoolean.tarannikovElementaryConstruction
        g) =
    2 * CryptBoolean.nonlinearity g

Tarannikov's construction doubles nonlinearity.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.card_f₂Support_tarannikovCoordinates {r : ℕ}
  (a : FABL.F₂Cube r) (aᵣ aₙ : FABL.𝔽₂) :
  (FABL.f₂Support (CryptBoolean.tarannikovCoordinates a aᵣ aₙ)).card =
    (FABL.f₂Support a).card +
        (FABL.f₂Support (CryptBoolean.singletonF₂Cube aᵣ)).card +
      (FABL.f₂Support (CryptBoolean.singletonF₂Cube aₙ)).card

theorem CryptBoolean.card_f₂Support_tarannikovCoordinates
  {r : ℕ} (a : FABL.F₂Cube r)
  (aᵣ aₙ : FABL.𝔽₂) :
  (FABL.f₂Support
        (CryptBoolean.tarannikovCoordinates
          a aᵣ aₙ)).card =
    (FABL.f₂Support a).card +
        (FABL.f₂Support
            (CryptBoolean.singletonF₂Cube
              aᵣ)).card +
      (FABL.f₂Support
          (CryptBoolean.singletonF₂Cube
            aₙ)).card

Support weight splits over Tarannikov coordinates.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.card_f₂Support_singletonF₂Cube (b : FABL.𝔽₂) :
  (FABL.f₂Support (CryptBoolean.singletonF₂Cube b)).card =
    if b = 1 then 1 else 0

theorem CryptBoolean.card_f₂Support_singletonF₂Cube
  (b : FABL.𝔽₂) :
  (FABL.f₂Support
        (CryptBoolean.singletonF₂Cube
          b)).card =
    if b = 1 then 1 else 0

A singleton binary cube has support weight equal to its bit.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.isResilient_tarannikovElementaryConstruction {r m : ℕ}
  {g : CryptBoolean.BooleanFunction (r + 1)} (hm : m < r + 1)
  (hg : CryptBoolean.IsResilient m g) :
  CryptBoolean.IsResilient m
    (CryptBoolean.tarannikovElementaryConstruction g)

theorem CryptBoolean.isResilient_tarannikovElementaryConstruction
  {r m : ℕ}
  {g :
    CryptBoolean.BooleanFunction (r + 1)}
  (hm : m < r + 1)
  (hg : CryptBoolean.IsResilient m g) :
  CryptBoolean.IsResilient m
    (CryptBoolean.tarannikovElementaryConstruction
      g)

Tarannikov's construction preserves every resilient order of the source.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.isResilient_succ_tarannikovElementaryConstruction {r m : ℕ}
  {g : CryptBoolean.BooleanFunction (r + 1)} (hm : m < r + 1)
  (hg : CryptBoolean.IsResilient m g)
  (hlast :
    ∀ (a : FABL.F₂Cube r),
      (FABL.f₂Support a).card ≤ m →
        CryptBoolean.walshTransform g
            (Fin.append a (CryptBoolean.singletonF₂Cube 1)) =
          0) :
  CryptBoolean.IsResilient (m + 1)
    (CryptBoolean.tarannikovElementaryConstruction g)

theorem CryptBoolean.isResilient_succ_tarannikovElementaryConstruction
  {r m : ℕ}
  {g :
    CryptBoolean.BooleanFunction (r + 1)}
  (hm : m < r + 1)
  (hg : CryptBoolean.IsResilient m g)
  (hlast :
    ∀ (a : FABL.F₂Cube r),
      (FABL.f₂Support a).card ≤ m →
        CryptBoolean.walshTransform g
            (Fin.append a
              (CryptBoolean.singletonF₂Cube
                1)) =
          0) :
  CryptBoolean.IsResilient (m + 1)
    (CryptBoolean.tarannikovElementaryConstruction
      g)

Under Carlet's extra last-frequency vanishing hypothesis, Tarannikov's
construction gains one resilient order.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_tarannikovElementaryConstruction
  {r : ℕ} (g : CryptBoolean.BooleanFunction (r + 1))
  (hdegree : 1 ≤ FABL.functionAlgebraicDegree g) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.tarannikovElementaryConstruction g) =
    FABL.functionAlgebraicDegree g

theorem CryptBoolean.functionAlgebraicDegree_tarannikovElementaryConstruction
  {r : ℕ}
  (g :
    CryptBoolean.BooleanFunction (r + 1))
  (hdegree :
    1 ≤ FABL.functionAlgebraicDegree g) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.tarannikovElementaryConstruction
        g) =
    FABL.functionAlgebraicDegree g

If the source is nonconstant, Tarannikov's construction preserves its
algebraic degree.

defdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

def CryptBoolean.tarannikovLinearStructureDirection (r : ℕ) :
  FABL.F₂Cube (r + 2)

def CryptBoolean.tarannikovLinearStructureDirection
  (r : ℕ) : FABL.F₂Cube (r + 2)

The direction with zero prefix and both final coordinates equal to one.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.tarannikovLinearStructureDirection_ne_zero (r : ℕ) :
  CryptBoolean.tarannikovLinearStructureDirection r ≠ 0

theorem CryptBoolean.tarannikovLinearStructureDirection_ne_zero
  (r : ℕ) :
  CryptBoolean.tarannikovLinearStructureDirection
      r ≠
    0

The Tarannikov direction is nonzero.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.tarannikovShearLinearEquiv_direction (r : ℕ) :
  (CryptBoolean.tarannikovShearLinearEquiv r)
      (CryptBoolean.tarannikovLinearStructureDirection r) =
    CryptBoolean.addedVariableDirection (r + 1)

theorem CryptBoolean.tarannikovShearLinearEquiv_direction
  (r : ℕ) :
  (CryptBoolean.tarannikovShearLinearEquiv
        r)
      (CryptBoolean.tarannikovLinearStructureDirection
        r) =
    CryptBoolean.addedVariableDirection
      (r + 1)

The shear sends `(0,…,0,1,1)` to the newly added coordinate direction.

theoremdefined in CryptBoolean/Carlet/Chapter07/Tarannikov.lean

complete

theorem CryptBoolean.tarannikovLinearStructureDirection_isNonzeroLinearStructure
  {r : ℕ} (g : CryptBoolean.BooleanFunction (r + 1)) :
  CryptBoolean.tarannikovLinearStructureDirection r ≠ 0 ∧
    CryptBoolean.IsLinearStructure
      (CryptBoolean.tarannikovElementaryConstruction g)
      (CryptBoolean.tarannikovLinearStructureDirection r)

theorem CryptBoolean.tarannikovLinearStructureDirection_isNonzeroLinearStructure
  {r : ℕ}
  (g :
    CryptBoolean.BooleanFunction
      (r + 1)) :
  CryptBoolean.tarannikovLinearStructureDirection
        r ≠
      0 ∧
    CryptBoolean.IsLinearStructure
      (CryptBoolean.tarannikovElementaryConstruction
        g)
      (CryptBoolean.tarannikovLinearStructureDirection
        r)

The final-two-coordinate direction is a nonzero linear structure of
Tarannikov's construction.

Theorem6.5.2

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.1.1

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Theorem 3.2.3

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-7theorem-14indirect-sumrelations-66-67pages-126-127fidelity-exact

Theorem 14 (Carlet, Relations (66)--(67), pp. 126--127). Let r,s>0, t<r, and m<s. Let f_1,f_2:V_r\to\mathbb F_2 be t-resilient and g_1,g_2:V_s\to\mathbb F_2 be m-resilient. Define h(x,y)=f_1(x)\oplus g_1(y) \oplus(f_1\oplus f_2)(x)(g_1\oplus g_2)(y). Then h is (t+m+1)-resilient and W_h(a,b)=\frac12W_{f_1}(a)(W_{g_1}(b)+W_{g_2}(b)) +\frac12W_{f_2}(a)(W_{g_1}(b)-W_{g_2}(b)). If the Walsh supports of f_1,f_2 are disjoint and likewise those of g_1,g_2, then \operatorname{nl}(h) =\min_{i,j\in\{1,2\}} \left( 2^{r+s-2} +2^{r-1}\operatorname{nl}(g_j) +2^{s-1}\operatorname{nl}(f_i) -\operatorname{nl}(f_i)\operatorname{nl}(g_j) \right).

Lean code for Theorem6.5.2●6 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSum.lean

complete

theorem CryptBoolean.two_mul_walshTransform_indirectSum {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  2 *
      CryptBoolean.walshTransform (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)
        (Fin.append a b) =
    CryptBoolean.walshTransform f₁ a *
        (CryptBoolean.walshTransform g₁ b +
          CryptBoolean.walshTransform g₂ b) +
      CryptBoolean.walshTransform f₂ a *
        (CryptBoolean.walshTransform g₁ b -
          CryptBoolean.walshTransform g₂ b)

theorem CryptBoolean.two_mul_walshTransform_indirectSum
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  2 *
      CryptBoolean.walshTransform
        (CryptBoolean.indirectSum f₁ f₂ g₁
          g₂)
        (Fin.append a b) =
    CryptBoolean.walshTransform f₁ a *
        (CryptBoolean.walshTransform g₁
            b +
          CryptBoolean.walshTransform g₂
            b) +
      CryptBoolean.walshTransform f₂ a *
        (CryptBoolean.walshTransform g₁
            b -
          CryptBoolean.walshTransform g₂
            b)

Division-free form of Carlet Relation (66).

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSum.lean

complete

theorem CryptBoolean.walshTransform_indirectSum_cast_eq_relation_66 {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  ↑(CryptBoolean.walshTransform (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)
        (Fin.append a b)) =
    1 / 2 * ↑(CryptBoolean.walshTransform f₁ a) *
        (↑(CryptBoolean.walshTransform g₁ b) +
          ↑(CryptBoolean.walshTransform g₂ b)) +
      1 / 2 * ↑(CryptBoolean.walshTransform f₂ a) *
        (↑(CryptBoolean.walshTransform g₁ b) -
          ↑(CryptBoolean.walshTransform g₂ b))

theorem CryptBoolean.walshTransform_indirectSum_cast_eq_relation_66
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  ↑(CryptBoolean.walshTransform
        (CryptBoolean.indirectSum f₁ f₂ g₁
          g₂)
        (Fin.append a b)) =
    1 / 2 *
          ↑(CryptBoolean.walshTransform f₁
              a) *
        (↑(CryptBoolean.walshTransform g₁
              b) +
          ↑(CryptBoolean.walshTransform g₂
              b)) +
      1 / 2 *
          ↑(CryptBoolean.walshTransform f₂
              a) *
        (↑(CryptBoolean.walshTransform g₁
              b) -
          ↑(CryptBoolean.walshTransform g₂
              b))

Carlet Relation (66) in the source's real-valued half-factor form.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSum.lean

complete

theorem CryptBoolean.isResilient_indirectSum {r s t m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (ht : t < r) (hm : m < s)
  (hf₁ : CryptBoolean.IsResilient t f₁)
  (hf₂ : CryptBoolean.IsResilient t f₂)
  (hg₁ : CryptBoolean.IsResilient m g₁)
  (hg₂ : CryptBoolean.IsResilient m g₂) :
  CryptBoolean.IsResilient (t + m + 1)
    (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)

theorem CryptBoolean.isResilient_indirectSum
  {r s t m : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (ht : t < r) (hm : m < s)
  (hf₁ : CryptBoolean.IsResilient t f₁)
  (hf₂ : CryptBoolean.IsResilient t f₂)
  (hg₁ : CryptBoolean.IsResilient m g₁)
  (hg₂ : CryptBoolean.IsResilient m g₂) :
  CryptBoolean.IsResilient (t + m + 1)
    (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)

Carlet Theorem 14: the indirect sum of a `t`-resilient pair and an
`m`-resilient pair is `(t+m+1)`-resilient.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSum.lean

complete

theorem CryptBoolean.two_mul_maxWalshMagnitude_indirectSum_of_disjointWalshSupport
  {r s : ℕ} (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₂ a = 0)
  (hg :
    ∀ (b : FABL.F₂Cube s),
      CryptBoolean.walshTransform g₁ b = 0 ∨
        CryptBoolean.walshTransform g₂ b = 0) :
  2 *
      CryptBoolean.maxWalshMagnitude
        (CryptBoolean.indirectSum f₁ f₂ g₁ g₂) =
    max (CryptBoolean.maxWalshMagnitude f₁)
        (CryptBoolean.maxWalshMagnitude f₂) *
      max (CryptBoolean.maxWalshMagnitude g₁)
        (CryptBoolean.maxWalshMagnitude g₂)

theorem CryptBoolean.two_mul_maxWalshMagnitude_indirectSum_of_disjointWalshSupport
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₂ a =
          0)
  (hg :
    ∀ (b : FABL.F₂Cube s),
      CryptBoolean.walshTransform g₁ b =
          0 ∨
        CryptBoolean.walshTransform g₂ b =
          0) :
  2 *
      CryptBoolean.maxWalshMagnitude
        (CryptBoolean.indirectSum f₁ f₂ g₁
          g₂) =
    max
        (CryptBoolean.maxWalshMagnitude
          f₁)
        (CryptBoolean.maxWalshMagnitude
          f₂) *
      max
        (CryptBoolean.maxWalshMagnitude
          g₁)
        (CryptBoolean.maxWalshMagnitude
          g₂)

Under disjoint spectra in each pair, twice the maximum Walsh magnitude
of the indirect sum is the product of the two pairwise maximum magnitudes.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSum.lean

complete

theorem CryptBoolean.nonlinearity_indirectSum_cast_eq_relation_67_spectral
  {r s : ℕ} (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₂ a = 0)
  (hg :
    ∀ (b : FABL.F₂Cube s),
      CryptBoolean.walshTransform g₁ b = 0 ∨
        CryptBoolean.walshTransform g₂ b = 0) :
  ↑(CryptBoolean.nonlinearity (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)) =
    2 ^ (r + s) / 2 -
      ↑(max (CryptBoolean.maxWalshMagnitude f₁)
              (CryptBoolean.maxWalshMagnitude f₂)) *
          ↑(max (CryptBoolean.maxWalshMagnitude g₁)
              (CryptBoolean.maxWalshMagnitude g₂)) /
        4

theorem CryptBoolean.nonlinearity_indirectSum_cast_eq_relation_67_spectral
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hf :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₂ a =
          0)
  (hg :
    ∀ (b : FABL.F₂Cube s),
      CryptBoolean.walshTransform g₁ b =
          0 ∨
        CryptBoolean.walshTransform g₂ b =
          0) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.indirectSum f₁ f₂ g₁
          g₂)) =
    2 ^ (r + s) / 2 -
      ↑(max
              (CryptBoolean.maxWalshMagnitude
                f₁)
              (CryptBoolean.maxWalshMagnitude
                f₂)) *
          ↑(max
              (CryptBoolean.maxWalshMagnitude
                g₁)
              (CryptBoolean.maxWalshMagnitude
                g₂)) /
        4

Relation (67) in a normalization-independent spectral form.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSum.lean

complete

theorem CryptBoolean.nonlinearity_indirectSum_cast_eq_relation_67 {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (hr : 0 < r) (hs : 0 < s)
  (hf :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₂ a = 0)
  (hg :
    ∀ (b : FABL.F₂Cube s),
      CryptBoolean.walshTransform g₁ b = 0 ∨
        CryptBoolean.walshTransform g₂ b = 0) :
  ↑(CryptBoolean.nonlinearity (CryptBoolean.indirectSum f₁ f₂ g₁ g₂)) =
    2 ^ (r + s - 2) +
          2 ^ (r - 1) *
            ↑(min (CryptBoolean.nonlinearity g₁)
                (CryptBoolean.nonlinearity g₂)) +
        2 ^ (s - 1) *
          ↑(min (CryptBoolean.nonlinearity f₁)
              (CryptBoolean.nonlinearity f₂)) -
      ↑(min (CryptBoolean.nonlinearity f₁)
            (CryptBoolean.nonlinearity f₂)) *
        ↑(min (CryptBoolean.nonlinearity g₁)
            (CryptBoolean.nonlinearity g₂))

theorem CryptBoolean.nonlinearity_indirectSum_cast_eq_relation_67
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hr : 0 < r) (hs : 0 < s)
  (hf :
    ∀ (a : FABL.F₂Cube r),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₂ a =
          0)
  (hg :
    ∀ (b : FABL.F₂Cube s),
      CryptBoolean.walshTransform g₁ b =
          0 ∨
        CryptBoolean.walshTransform g₂ b =
          0) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.indirectSum f₁ f₂ g₁
          g₂)) =
    2 ^ (r + s - 2) +
          2 ^ (r - 1) *
            ↑(min
                (CryptBoolean.nonlinearity
                  g₁)
                (CryptBoolean.nonlinearity
                  g₂)) +
        2 ^ (s - 1) *
          ↑(min
              (CryptBoolean.nonlinearity
                f₁)
              (CryptBoolean.nonlinearity
                f₂)) -
      ↑(min (CryptBoolean.nonlinearity f₁)
            (CryptBoolean.nonlinearity
              f₂)) *
        ↑(min
            (CryptBoolean.nonlinearity g₁)
            (CryptBoolean.nonlinearity
              g₂))

Relation (67), simplified from the minimum over four pairs to the
minimum nonlinearity in each disjoint spectral pair.

Theorem6.5.3

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.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-7theorem-14indirect-sumalgebraic-degreepages-126-127fidelity-corrected-nonconstant-hypotheses

Degree clause of Theorem 14 (Carlet, pp. 126--127). If f_1\oplus f_2 and g_1\oplus g_2 are both nonconstant, then \deg_{\mathrm{alg}}h=\max\bigl( \deg_{\mathrm{alg}}f_1,\deg_{\mathrm{alg}}g_1, \deg_{\mathrm{alg}}(f_1\oplus f_2) +\deg_{\mathrm{alg}}(g_1\oplus g_2) \bigr). If either difference is constant, the corresponding branch reduces to a direct sum and has the degree supplied by that specialization.

Lean code for Theorem6.5.3●8 declarations

defdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

def CryptBoolean.booleanBlockProduct {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.BooleanFunction (r + s)

def CryptBoolean.booleanBlockProduct {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.BooleanFunction (r + s)

Pointwise product of Boolean functions on two disjoint coordinate
blocks.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

theorem CryptBoolean.booleanBlockProduct_append {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) (x : FABL.F₂Cube r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.booleanBlockProduct f g (Fin.append x y) = f x * g y

theorem CryptBoolean.booleanBlockProduct_append
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s)
  (x : FABL.F₂Cube r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.booleanBlockProduct f g
      (Fin.append x y) =
    f x * g y

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_booleanBlockProduct {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) (hf : f ≠ 0) (hg : g ≠ 0) :
  FABL.functionAlgebraicDegree (CryptBoolean.booleanBlockProduct f g) =
    FABL.functionAlgebraicDegree f + FABL.functionAlgebraicDegree g

theorem CryptBoolean.functionAlgebraicDegree_booleanBlockProduct
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s)
  (hf : f ≠ 0) (hg : g ≠ 0) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.booleanBlockProduct f
        g) =
    FABL.functionAlgebraicDegree f +
      FABL.functionAlgebraicDegree g

The algebraic degree of a product on disjoint coordinate blocks is the
sum of the factor degrees, provided neither factor is zero.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_indirectSum {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (hfZero : f₁ + f₂ ≠ 0)
  (hfOne : f₁ + f₂ ≠ 1) (hgZero : g₁ + g₂ ≠ 0) (hgOne : g₁ + g₂ ≠ 1) :
  FABL.functionAlgebraicDegree (CryptBoolean.indirectSum f₁ f₂ g₁ g₂) =
    max
      (max (FABL.functionAlgebraicDegree f₁)
        (FABL.functionAlgebraicDegree g₁))
      (FABL.functionAlgebraicDegree (f₁ + f₂) +
        FABL.functionAlgebraicDegree (g₁ + g₂))

theorem CryptBoolean.functionAlgebraicDegree_indirectSum
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hfZero : f₁ + f₂ ≠ 0)
  (hfOne : f₁ + f₂ ≠ 1)
  (hgZero : g₁ + g₂ ≠ 0)
  (hgOne : g₁ + g₂ ≠ 1) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.indirectSum f₁ f₂ g₁
        g₂) =
    max
      (max
        (FABL.functionAlgebraicDegree f₁)
        (FABL.functionAlgebraicDegree g₁))
      (FABL.functionAlgebraicDegree
          (f₁ + f₂) +
        FABL.functionAlgebraicDegree
          (g₁ + g₂))

Under the corrected nonconstant-difference hypotheses, the degree of an
indirect sum is the maximum of the two base degrees and the sum of the two
difference degrees.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_leftDifference_eq_zero
  {r s : ℕ} (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (hleft : f₁ + f₂ = 0) :
  FABL.functionAlgebraicDegree (CryptBoolean.indirectSum f₁ f₂ g₁ g₂) =
    max (FABL.functionAlgebraicDegree f₁)
      (FABL.functionAlgebraicDegree g₁)

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_leftDifference_eq_zero
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hleft : f₁ + f₂ = 0) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.indirectSum f₁ f₂ g₁
        g₂) =
    max (FABL.functionAlgebraicDegree f₁)
      (FABL.functionAlgebraicDegree g₁)

If the left difference vanishes, the indirect sum specializes to the
direct sum of the first functions.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_leftDifference_eq_one
  {r s : ℕ} (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (hleft : f₁ + f₂ = 1) :
  FABL.functionAlgebraicDegree (CryptBoolean.indirectSum f₁ f₂ g₁ g₂) =
    max (FABL.functionAlgebraicDegree f₁)
      (FABL.functionAlgebraicDegree g₂)

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_leftDifference_eq_one
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hleft : f₁ + f₂ = 1) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.indirectSum f₁ f₂ g₁
        g₂) =
    max (FABL.functionAlgebraicDegree f₁)
      (FABL.functionAlgebraicDegree g₂)

If the left difference is one, the indirect sum specializes to the
direct sum of the first left function and second right function.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_rightDifference_eq_zero
  {r s : ℕ} (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (hright : g₁ + g₂ = 0) :
  FABL.functionAlgebraicDegree (CryptBoolean.indirectSum f₁ f₂ g₁ g₂) =
    max (FABL.functionAlgebraicDegree f₁)
      (FABL.functionAlgebraicDegree g₁)

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_rightDifference_eq_zero
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hright : g₁ + g₂ = 0) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.indirectSum f₁ f₂ g₁
        g₂) =
    max (FABL.functionAlgebraicDegree f₁)
      (FABL.functionAlgebraicDegree g₁)

If the right difference vanishes, the indirect sum specializes to the
direct sum of the first functions.

theoremdefined in CryptBoolean/Carlet/Chapter07/IndirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_rightDifference_eq_one
  {r s : ℕ} (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s) (hright : g₁ + g₂ = 1) :
  FABL.functionAlgebraicDegree (CryptBoolean.indirectSum f₁ f₂ g₁ g₂) =
    max (FABL.functionAlgebraicDegree f₂)
      (FABL.functionAlgebraicDegree g₁)

theorem CryptBoolean.functionAlgebraicDegree_indirectSum_of_rightDifference_eq_one
  {r s : ℕ}
  (f₁ f₂ : CryptBoolean.BooleanFunction r)
  (g₁ g₂ : CryptBoolean.BooleanFunction s)
  (hright : g₁ + g₂ = 1) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.indirectSum f₁ f₂ g₁
        g₂) =
    max (FABL.functionAlgebraicDegree f₂)
      (FABL.functionAlgebraicDegree g₁)

If the right difference is one, the indirect sum specializes to the
direct sum of the second left function and first right function.

Proposition6.5.4

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 3.2.3

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-7proposition-34three-function-constructionrelations-68-69pages-127-128fidelity-exact

Proposition 34 (Carlet, Relations (68)--(69), pp. 127--128). Let n>0 and k<n. Let f_1,f_2,f_3:V_n\to\mathbb F_2 each be correlation immune of order k, respectively k-resilient. Put s_1=f_1\oplus f_2\oplus f_3,\qquad s_2=f_1f_2\oplus f_1f_3\oplus f_2f_3. Then s_1 is correlation immune of order k, respectively k-resilient, if and only if s_2 has the same property. Moreover, \operatorname{nl}(s_2)\ge \frac12\left( \operatorname{nl}(s_1)+ \sum_{i=1}^3\operatorname{nl}(f_i)-2^{n-1} \right).

Lean code for Proposition6.5.4●5 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.isCorrelationImmune_threeFunctionSum_iff_pairwiseProductSum
  {n k : ℕ} (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hk : k < n) (h₁ : CryptBoolean.IsCorrelationImmune k f₁)
  (h₂ : CryptBoolean.IsCorrelationImmune k f₂)
  (h₃ : CryptBoolean.IsCorrelationImmune k f₃) :
  CryptBoolean.IsCorrelationImmune k
      (CryptBoolean.threeFunctionSum f₁ f₂ f₃) ↔
    CryptBoolean.IsCorrelationImmune k
      (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃)

theorem CryptBoolean.isCorrelationImmune_threeFunctionSum_iff_pairwiseProductSum
  {n k : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hk : k < n)
  (h₁ :
    CryptBoolean.IsCorrelationImmune k f₁)
  (h₂ :
    CryptBoolean.IsCorrelationImmune k f₂)
  (h₃ :
    CryptBoolean.IsCorrelationImmune k
      f₃) :
  CryptBoolean.IsCorrelationImmune k
      (CryptBoolean.threeFunctionSum f₁ f₂
        f₃) ↔
    CryptBoolean.IsCorrelationImmune k
      (CryptBoolean.threeFunctionPairwiseProductSum
        f₁ f₂ f₃)

Carlet Proposition 34, correlation-immune form: under three
correlation-immune inputs, their first and second elementary symmetric
functions are correlation immune simultaneously.

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.isResilient_threeFunctionSum_iff_pairwiseProductSum
  {n k : ℕ} (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hk : k < n) (h₁ : CryptBoolean.IsResilient k f₁)
  (h₂ : CryptBoolean.IsResilient k f₂)
  (h₃ : CryptBoolean.IsResilient k f₃) :
  CryptBoolean.IsResilient k (CryptBoolean.threeFunctionSum f₁ f₂ f₃) ↔
    CryptBoolean.IsResilient k
      (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃)

theorem CryptBoolean.isResilient_threeFunctionSum_iff_pairwiseProductSum
  {n k : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hk : k < n)
  (h₁ : CryptBoolean.IsResilient k f₁)
  (h₂ : CryptBoolean.IsResilient k f₂)
  (h₃ : CryptBoolean.IsResilient k f₃) :
  CryptBoolean.IsResilient k
      (CryptBoolean.threeFunctionSum f₁ f₂
        f₃) ↔
    CryptBoolean.IsResilient k
      (CryptBoolean.threeFunctionPairwiseProductSum
        f₁ f₂ f₃)

Carlet Proposition 34, resilient form: under three resilient inputs,
their first and second elementary symmetric functions are resilient
simultaneously.

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.two_mul_maxWalshMagnitude_pairwiseProductSum_le {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) :
  2 *
      CryptBoolean.maxWalshMagnitude
        (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃) ≤
    CryptBoolean.maxWalshMagnitude
            (CryptBoolean.threeFunctionSum f₁ f₂ f₃) +
          CryptBoolean.maxWalshMagnitude f₁ +
        CryptBoolean.maxWalshMagnitude f₂ +
      CryptBoolean.maxWalshMagnitude f₃

theorem CryptBoolean.two_mul_maxWalshMagnitude_pairwiseProductSum_le
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n) :
  2 *
      CryptBoolean.maxWalshMagnitude
        (CryptBoolean.threeFunctionPairwiseProductSum
          f₁ f₂ f₃) ≤
    CryptBoolean.maxWalshMagnitude
            (CryptBoolean.threeFunctionSum
              f₁ f₂ f₃) +
          CryptBoolean.maxWalshMagnitude
            f₁ +
        CryptBoolean.maxWalshMagnitude
          f₂ +
      CryptBoolean.maxWalshMagnitude f₃

Spectral maximum inequality underlying Carlet Relation (68).

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.relation_68_threeFunctionConstruction {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonlinearity (CryptBoolean.threeFunctionSum f₁ f₂ f₃) +
          CryptBoolean.nonlinearity f₁ +
        CryptBoolean.nonlinearity f₂ +
      CryptBoolean.nonlinearity f₃ ≤
    2 ^ n +
      2 *
        CryptBoolean.nonlinearity
          (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃)

theorem CryptBoolean.relation_68_threeFunctionConstruction
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonlinearity
            (CryptBoolean.threeFunctionSum
              f₁ f₂ f₃) +
          CryptBoolean.nonlinearity f₁ +
        CryptBoolean.nonlinearity f₂ +
      CryptBoolean.nonlinearity f₃ ≤
    2 ^ n +
      2 *
        CryptBoolean.nonlinearity
          (CryptBoolean.threeFunctionPairwiseProductSum
            f₁ f₂ f₃)

Division-free natural-number form of Carlet Relation (68).

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.nonlinearity_pairwiseProductSum_cast_lower_bound {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n) (hn : 0 < n) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃)) ≥
    1 / 2 *
        (↑(CryptBoolean.nonlinearity
                  (CryptBoolean.threeFunctionSum f₁ f₂ f₃)) +
              ↑(CryptBoolean.nonlinearity f₁) +
            ↑(CryptBoolean.nonlinearity f₂) +
          ↑(CryptBoolean.nonlinearity f₃)) -
      2 ^ (n - 1)

theorem CryptBoolean.nonlinearity_pairwiseProductSum_cast_lower_bound
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.threeFunctionPairwiseProductSum
          f₁ f₂ f₃)) ≥
    1 / 2 *
        (↑(CryptBoolean.nonlinearity
                  (CryptBoolean.threeFunctionSum
                    f₁ f₂ f₃)) +
              ↑(CryptBoolean.nonlinearity
                  f₁) +
            ↑(CryptBoolean.nonlinearity
                f₂) +
          ↑(CryptBoolean.nonlinearity
              f₃)) -
      2 ^ (n - 1)

Carlet Relation (68) in the source's real-valued half-factor form.

Theorem6.5.5

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.1.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Theorem 3.2.3

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-7relation-69three-function-constructiondisjoint-walsh-supportpage-128fidelity-exact

Relation (69) (Carlet, p. 128). Under the hypotheses of Proposition 34, suppose the Walsh supports of f_1,f_2,f_3 are pairwise disjoint. Then \operatorname{nl}(s_2)\ge \frac12\left( \operatorname{nl}(s_1)+ \min_{1\le i\le3}\operatorname{nl}(f_i) \right).

Lean code for Theorem6.5.5●3 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.two_mul_maxWalshMagnitude_pairwiseProductSum_le_of_pairwiseDisjoint
  {n : ℕ} (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n)
  (h₁₂ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₂ a = 0)
  (h₁₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₃ a = 0)
  (h₂₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₂ a = 0 ∨
        CryptBoolean.walshTransform f₃ a = 0) :
  2 *
      CryptBoolean.maxWalshMagnitude
        (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃) ≤
    CryptBoolean.maxWalshMagnitude
        (CryptBoolean.threeFunctionSum f₁ f₂ f₃) +
      max (CryptBoolean.maxWalshMagnitude f₁)
        (max (CryptBoolean.maxWalshMagnitude f₂)
          (CryptBoolean.maxWalshMagnitude f₃))

theorem CryptBoolean.two_mul_maxWalshMagnitude_pairwiseProductSum_le_of_pairwiseDisjoint
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (h₁₂ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₂ a =
          0)
  (h₁₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₃ a =
          0)
  (h₂₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₂ a =
          0 ∨
        CryptBoolean.walshTransform f₃ a =
          0) :
  2 *
      CryptBoolean.maxWalshMagnitude
        (CryptBoolean.threeFunctionPairwiseProductSum
          f₁ f₂ f₃) ≤
    CryptBoolean.maxWalshMagnitude
        (CryptBoolean.threeFunctionSum f₁
          f₂ f₃) +
      max
        (CryptBoolean.maxWalshMagnitude
          f₁)
        (max
          (CryptBoolean.maxWalshMagnitude
            f₂)
          (CryptBoolean.maxWalshMagnitude
            f₃))

Spectral maximum inequality for Proposition 34 under pairwise disjoint
input Walsh supports.

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.relation_69_threeFunctionConstruction {n : ℕ}
  (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n)
  (h₁₂ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₂ a = 0)
  (h₁₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₃ a = 0)
  (h₂₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₂ a = 0 ∨
        CryptBoolean.walshTransform f₃ a = 0) :
  CryptBoolean.nonlinearity (CryptBoolean.threeFunctionSum f₁ f₂ f₃) +
      min (CryptBoolean.nonlinearity f₁)
        (min (CryptBoolean.nonlinearity f₂)
          (CryptBoolean.nonlinearity f₃)) ≤
    2 *
      CryptBoolean.nonlinearity
        (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃)

theorem CryptBoolean.relation_69_threeFunctionConstruction
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (h₁₂ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₂ a =
          0)
  (h₁₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₃ a =
          0)
  (h₂₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₂ a =
          0 ∨
        CryptBoolean.walshTransform f₃ a =
          0) :
  CryptBoolean.nonlinearity
        (CryptBoolean.threeFunctionSum f₁
          f₂ f₃) +
      min (CryptBoolean.nonlinearity f₁)
        (min
          (CryptBoolean.nonlinearity f₂)
          (CryptBoolean.nonlinearity
            f₃)) ≤
    2 *
      CryptBoolean.nonlinearity
        (CryptBoolean.threeFunctionPairwiseProductSum
          f₁ f₂ f₃)

Division-free natural-number form of Carlet Relation (69).

theoremdefined in CryptBoolean/Carlet/Chapter07/ThreeFunctionConstruction.lean

complete

theorem CryptBoolean.nonlinearity_pairwiseProductSum_cast_lower_bound_of_pairwiseDisjoint
  {n : ℕ} (f₁ f₂ f₃ : CryptBoolean.BooleanFunction n)
  (h₁₂ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₂ a = 0)
  (h₁₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a = 0 ∨
        CryptBoolean.walshTransform f₃ a = 0)
  (h₂₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₂ a = 0 ∨
        CryptBoolean.walshTransform f₃ a = 0) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.threeFunctionPairwiseProductSum f₁ f₂ f₃)) ≥
    1 / 2 *
      (↑(CryptBoolean.nonlinearity
            (CryptBoolean.threeFunctionSum f₁ f₂ f₃)) +
        ↑(min (CryptBoolean.nonlinearity f₁)
            (min (CryptBoolean.nonlinearity f₂)
              (CryptBoolean.nonlinearity f₃))))

theorem CryptBoolean.nonlinearity_pairwiseProductSum_cast_lower_bound_of_pairwiseDisjoint
  {n : ℕ}
  (f₁ f₂ f₃ :
    CryptBoolean.BooleanFunction n)
  (h₁₂ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₂ a =
          0)
  (h₁₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₁ a =
          0 ∨
        CryptBoolean.walshTransform f₃ a =
          0)
  (h₂₃ :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f₂ a =
          0 ∨
        CryptBoolean.walshTransform f₃ a =
          0) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.threeFunctionPairwiseProductSum
          f₁ f₂ f₃)) ≥
    1 / 2 *
      (↑(CryptBoolean.nonlinearity
            (CryptBoolean.threeFunctionSum
              f₁ f₂ f₃)) +
        ↑(min
            (CryptBoolean.nonlinearity f₁)
            (min
              (CryptBoolean.nonlinearity
                f₂)
              (CryptBoolean.nonlinearity
                f₃))))

Carlet Relation (69) in the source's real-valued half-factor form.

Theorem6.5.6

Group: Chapter 6: Resilient functions (38)

Group member previews

Preview

Theorem 6.1.1

Loading preview

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

Statement uses 4

Statement dependency previews

Preview

Definition 1.1.2

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-7disjoint-supportresiliencynonlinearityalgebraic-degreepage-128fidelity-exact

Sums with disjoint truth supports (Carlet, p. 128). Let g,h:V_n\to\mathbb F_2 have disjoint truth supports and put f=g\oplus h. Then f is balanced exactly when w_H(g)+w_H(h)=2^{n-1}. If g and h are correlation immune of order m and f is balanced, then f is m-resilient and \operatorname{nl}(f) \ge\operatorname{nl}(g)+\operatorname{nl}(h)-2^{n-1}. Also \deg_{\mathrm{alg}}f \le\max(\deg_{\mathrm{alg}}g,\deg_{\mathrm{alg}}h), and equality can occur.

Lean code for Theorem6.5.6●9 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.hammingWeight_add_eq_of_disjoint_truthSupport {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h)) :
  CryptBoolean.hammingWeight (g + h) =
    CryptBoolean.hammingWeight g + CryptBoolean.hammingWeight h

theorem CryptBoolean.hammingWeight_add_eq_of_disjoint_truthSupport
  {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h)) :
  CryptBoolean.hammingWeight (g + h) =
    CryptBoolean.hammingWeight g +
      CryptBoolean.hammingWeight h

Disjoint truth supports make Hamming weight additive.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.isBalanced_add_iff_hammingWeight_add_eq_two_pow_pred
  {n : ℕ} (g h : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h)) :
  CryptBoolean.IsBalanced (g + h) ↔
    CryptBoolean.hammingWeight g + CryptBoolean.hammingWeight h =
      2 ^ (n - 1)

theorem CryptBoolean.isBalanced_add_iff_hammingWeight_add_eq_two_pow_pred
  {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h)) :
  CryptBoolean.IsBalanced (g + h) ↔
    CryptBoolean.hammingWeight g +
        CryptBoolean.hammingWeight h =
      2 ^ (n - 1)

The sum of two functions with disjoint truth supports is balanced exactly
when their weights add to half the cube.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.walshTransform_add_of_disjoint_truthSupport {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h))
  (a : FABL.F₂Cube n) (ha : a ≠ 0) :
  CryptBoolean.walshTransform (g + h) a =
    CryptBoolean.walshTransform g a + CryptBoolean.walshTransform h a

theorem CryptBoolean.walshTransform_add_of_disjoint_truthSupport
  {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h))
  (a : FABL.F₂Cube n) (ha : a ≠ 0) :
  CryptBoolean.walshTransform (g + h) a =
    CryptBoolean.walshTransform g a +
      CryptBoolean.walshTransform h a

Away from the zero frequency, the Walsh transform of a sum with disjoint
truth supports is the sum of the two Walsh transforms.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.isResilient_add_of_disjoint_truthSupport {n m : ℕ}
  (g h : CryptBoolean.BooleanFunction n) (hn : 0 < n) (hm : m < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h))
  (hg : CryptBoolean.IsCorrelationImmune m g)
  (hh : CryptBoolean.IsCorrelationImmune m h)
  (hbalanced : CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.IsResilient m (g + h)

theorem CryptBoolean.isResilient_add_of_disjoint_truthSupport
  {n m : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h))
  (hg :
    CryptBoolean.IsCorrelationImmune m g)
  (hh :
    CryptBoolean.IsCorrelationImmune m h)
  (hbalanced :
    CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.IsResilient m (g + h)

Two correlation-immune functions of the same order whose disjoint-support
sum is balanced yield a resilient function of that order.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.maxWalshMagnitude_add_le_of_disjoint_truthSupport {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h))
  (hbalanced : CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.maxWalshMagnitude (g + h) ≤
    CryptBoolean.maxWalshMagnitude g + CryptBoolean.maxWalshMagnitude h

theorem CryptBoolean.maxWalshMagnitude_add_le_of_disjoint_truthSupport
  {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h))
  (hbalanced :
    CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.maxWalshMagnitude (g + h) ≤
    CryptBoolean.maxWalshMagnitude g +
      CryptBoolean.maxWalshMagnitude h

The Walsh maximum of a balanced disjoint-support sum is at most the sum
of the two Walsh maxima.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.nonlinearity_add_le_two_pow_pred_add_of_disjoint_truthSupport
  {n : ℕ} (g h : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h))
  (hbalanced : CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.nonlinearity g + CryptBoolean.nonlinearity h ≤
    2 ^ (n - 1) + CryptBoolean.nonlinearity (g + h)

theorem CryptBoolean.nonlinearity_add_le_two_pow_pred_add_of_disjoint_truthSupport
  {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h))
  (hbalanced :
    CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.nonlinearity g +
      CryptBoolean.nonlinearity h ≤
    2 ^ (n - 1) +
      CryptBoolean.nonlinearity (g + h)

Division-free form of the nonlinearity lower bound for a balanced sum
with disjoint truth supports.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.nonlinearity_add_sub_two_pow_pred_le_of_disjoint_truthSupport
  {n : ℕ} (g h : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h))
  (hbalanced : CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.nonlinearity g + CryptBoolean.nonlinearity h -
      2 ^ (n - 1) ≤
    CryptBoolean.nonlinearity (g + h)

theorem CryptBoolean.nonlinearity_add_sub_two_pow_pred_le_of_disjoint_truthSupport
  {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h))
  (hbalanced :
    CryptBoolean.IsBalanced (g + h)) :
  CryptBoolean.nonlinearity g +
        CryptBoolean.nonlinearity h -
      2 ^ (n - 1) ≤
    CryptBoolean.nonlinearity (g + h)

Carlet's nonlinearity lower bound for a balanced sum with disjoint truth
supports.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_add_le_max_of_disjoint_truthSupport
  {n : ℕ} (g h : CryptBoolean.BooleanFunction n)
  (_hdisjoint :
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h)) :
  FABL.functionAlgebraicDegree (g + h) ≤
    max (FABL.functionAlgebraicDegree g)
      (FABL.functionAlgebraicDegree h)

theorem CryptBoolean.functionAlgebraicDegree_add_le_max_of_disjoint_truthSupport
  {n : ℕ}
  (g h : CryptBoolean.BooleanFunction n)
  (_hdisjoint :
    Disjoint (CryptBoolean.support g)
      (CryptBoolean.support h)) :
  FABL.functionAlgebraicDegree (g + h) ≤
    max (FABL.functionAlgebraicDegree g)
      (FABL.functionAlgebraicDegree h)

Algebraic degree is submaximal under a sum with disjoint truth supports.

theoremdefined in CryptBoolean/Carlet/Chapter07/DisjointTruthSupport.lean

complete

theorem CryptBoolean.exists_disjoint_truthSupport_functionAlgebraicDegree_add_eq_max :
  ∃ g h,
    Disjoint (CryptBoolean.support g) (CryptBoolean.support h) ∧
      g ≠ 0 ∧
        FABL.functionAlgebraicDegree (g + h) =
          max (FABL.functionAlgebraicDegree g)
            (FABL.functionAlgebraicDegree h)

theorem CryptBoolean.exists_disjoint_truthSupport_functionAlgebraicDegree_add_eq_max :
  ∃ g h,
    Disjoint (CryptBoolean.support g)
        (CryptBoolean.support h) ∧
      g ≠ 0 ∧
        FABL.functionAlgebraicDegree
            (g + h) =
          max
            (FABL.functionAlgebraicDegree
              g)
            (FABL.functionAlgebraicDegree
              h)

Algebraic-degree equality occurs for a nonzero one-variable summand and
the zero summand, whose truth supports are disjoint.