6.4. Composition on coordinate blocks🔗

Theorem6.4.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 3

Statement dependency previews

Preview

Definition 3.6.1

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-7adding-variableresilient-constructionpage-122fidelity-exact

Adding a variable (Carlet, p. 122). If f:V_r\to\mathbb F_2 is t-resilient, then h(x,z)=f(x)\oplus z is (t+1)-resilient. If f has parameters (r,t,r-t-1,\,2^{r-1}-2^{t+1}), then h has parameters (r+1,t+1,r-t-1,\,2^r-2^{t+2}). The last coordinate direction is a nonzero linear structure of h.

Lean code for Theorem6.4.1●17 declarations

defdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

def CryptBoolean.oneVariableParity : CryptBoolean.BooleanFunction 1

def CryptBoolean.oneVariableParity :
  CryptBoolean.BooleanFunction 1

The parity function on the unique coordinate of the one-dimensional
binary cube.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.oneVariableParity_apply (z : FABL.F₂Cube 1) :
  CryptBoolean.oneVariableParity z = z 0

theorem CryptBoolean.oneVariableParity_apply
  (z : FABL.F₂Cube 1) :
  CryptBoolean.oneVariableParity z = z 0

One-variable parity is the identity function.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.oneVariableParity_eq_booleanFunctionF₂Encoding :
  CryptBoolean.oneVariableParity =
    FABL.booleanFunctionF₂Encoding (FABL.parityFunction Finset.univ)

theorem CryptBoolean.oneVariableParity_eq_booleanFunctionF₂Encoding :
  CryptBoolean.oneVariableParity =
    FABL.booleanFunctionF₂Encoding
      (FABL.parityFunction Finset.univ)

The binary one-variable parity is the canonical encoding of FABL's
sign-valued parity.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.oneVariableParity_eq_affineFunction :
  CryptBoolean.oneVariableParity =
    FABL.affineFunction 0 (FABL.f₂CubeOfFinset Finset.univ)

theorem CryptBoolean.oneVariableParity_eq_affineFunction :
  CryptBoolean.oneVariableParity =
    FABL.affineFunction 0
      (FABL.f₂CubeOfFinset Finset.univ)

One-variable parity is the nonconstant linear function with all-one
coefficient.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.oneVariableParity_isResilient :
  CryptBoolean.IsResilient 0 CryptBoolean.oneVariableParity

theorem CryptBoolean.oneVariableParity_isResilient :
  CryptBoolean.IsResilient 0
    CryptBoolean.oneVariableParity

One-variable parity is zero-resilient.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.nonlinearity_oneVariableParity :
  CryptBoolean.nonlinearity CryptBoolean.oneVariableParity = 0

theorem CryptBoolean.nonlinearity_oneVariableParity :
  CryptBoolean.nonlinearity
      CryptBoolean.oneVariableParity =
    0

One-variable parity is affine and hence has zero nonlinearity.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_oneVariableParity :
  FABL.functionAlgebraicDegree CryptBoolean.oneVariableParity = 1

theorem CryptBoolean.functionAlgebraicDegree_oneVariableParity :
  FABL.functionAlgebraicDegree
      CryptBoolean.oneVariableParity =
    1

One-variable parity has algebraic degree one.

defdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

def CryptBoolean.addingVariable {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  CryptBoolean.BooleanFunction (r + 1)

def CryptBoolean.addingVariable {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  CryptBoolean.BooleanFunction (r + 1)

Adding a variable is the Boolean direct sum with one-variable parity.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.addingVariable_append {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) (x : FABL.F₂Cube r)
  (z : FABL.F₂Cube 1) :
  CryptBoolean.addingVariable f (Fin.append x z) = f x + z 0

theorem CryptBoolean.addingVariable_append {r : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (x : FABL.F₂Cube r)
  (z : FABL.F₂Cube 1) :
  CryptBoolean.addingVariable f
      (Fin.append x z) =
    f x + z 0

Adding a variable evaluates as `f(x) ⊕ z`.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.isResilient_addingVariable {r t : ℕ}
  {f : CryptBoolean.BooleanFunction r} (ht : t < r)
  (hf : CryptBoolean.IsResilient t f) :
  CryptBoolean.IsResilient (t + 1) (CryptBoolean.addingVariable f)

theorem CryptBoolean.isResilient_addingVariable
  {r t : ℕ}
  {f : CryptBoolean.BooleanFunction r}
  (ht : t < r)
  (hf : CryptBoolean.IsResilient t f) :
  CryptBoolean.IsResilient (t + 1)
    (CryptBoolean.addingVariable f)

Adding a variable raises the resilient order by one.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.nonlinearity_addingVariable {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  CryptBoolean.nonlinearity (CryptBoolean.addingVariable f) =
    2 * CryptBoolean.nonlinearity f

theorem CryptBoolean.nonlinearity_addingVariable
  {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  CryptBoolean.nonlinearity
      (CryptBoolean.addingVariable f) =
    2 * CryptBoolean.nonlinearity f

Adding a variable doubles nonlinearity.

defdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

def CryptBoolean.addedVariableDirection (r : ℕ) : FABL.F₂Cube (r + 1)

def CryptBoolean.addedVariableDirection
  (r : ℕ) : FABL.F₂Cube (r + 1)

The direction of the newly added final coordinate.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.addedVariableDirection_ne_zero (r : ℕ) :
  CryptBoolean.addedVariableDirection r ≠ 0

theorem CryptBoolean.addedVariableDirection_ne_zero
  (r : ℕ) :
  CryptBoolean.addedVariableDirection r ≠
    0

The newly added coordinate direction is nonzero.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.addedVariableDirection_isNonzeroLinearStructure {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  CryptBoolean.addedVariableDirection r ≠ 0 ∧
    CryptBoolean.IsLinearStructure (CryptBoolean.addingVariable f)
      (CryptBoolean.addedVariableDirection r)

theorem CryptBoolean.addedVariableDirection_isNonzeroLinearStructure
  {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  CryptBoolean.addedVariableDirection r ≠
      0 ∧
    CryptBoolean.IsLinearStructure
      (CryptBoolean.addingVariable f)
      (CryptBoolean.addedVariableDirection
        r)

The newly added final coordinate is a nonzero linear structure.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_addingVariable_eq {r t : ℕ}
  {f : CryptBoolean.BooleanFunction r} (ht : t < r - 1)
  (hf : CryptBoolean.IsResilient t f)
  (hdegree : r - t - 1 ≤ FABL.functionAlgebraicDegree f) :
  FABL.functionAlgebraicDegree (CryptBoolean.addingVariable f) =
    FABL.functionAlgebraicDegree f

theorem CryptBoolean.functionAlgebraicDegree_addingVariable_eq
  {r t : ℕ}
  {f : CryptBoolean.BooleanFunction r}
  (ht : t < r - 1)
  (hf : CryptBoolean.IsResilient t f)
  (hdegree :
    r - t - 1 ≤
      FABL.functionAlgebraicDegree f) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.addingVariable f) =
    FABL.functionAlgebraicDegree f

In the source parameter range, adding a variable preserves algebraic
degree.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_addingVariable_eq_source {r t : ℕ}
  {f : CryptBoolean.BooleanFunction r} (ht : t < r - 1)
  (hf : CryptBoolean.IsResilient t f)
  (hdegree : FABL.functionAlgebraicDegree f = r - t - 1) :
  FABL.functionAlgebraicDegree (CryptBoolean.addingVariable f) =
    r - t - 1

theorem CryptBoolean.functionAlgebraicDegree_addingVariable_eq_source
  {r t : ℕ}
  {f : CryptBoolean.BooleanFunction r}
  (ht : t < r - 1)
  (hf : CryptBoolean.IsResilient t f)
  (hdegree :
    FABL.functionAlgebraicDegree f =
      r - t - 1) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.addingVariable f) =
    r - t - 1

In Carlet's sharp source case, the preserved degree is `r - t - 1`.

theoremdefined in CryptBoolean/Carlet/Chapter07/AddingVariable.lean

complete

theorem CryptBoolean.nonlinearity_addingVariable_ge_source {r t : ℕ}
  (f : CryptBoolean.BooleanFunction r) (ht : t < r - 1)
  (hnonlinearity :
    2 ^ (r - 1) - 2 ^ (t + 1) ≤ CryptBoolean.nonlinearity f) :
  2 ^ r - 2 ^ (t + 2) ≤
    CryptBoolean.nonlinearity (CryptBoolean.addingVariable f)

theorem CryptBoolean.nonlinearity_addingVariable_ge_source
  {r t : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (ht : t < r - 1)
  (hnonlinearity :
    2 ^ (r - 1) - 2 ^ (t + 1) ≤
      CryptBoolean.nonlinearity f) :
  2 ^ r - 2 ^ (t + 2) ≤
    CryptBoolean.nonlinearity
      (CryptBoolean.addingVariable f)

The sharp source lower bound on nonlinearity is preserved with the
expected doubled scale.

Theorem6.4.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 2

Reverse dependency previews

Preview

Theorem 6.4.3

Loading preview

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

✓L∃∀N

Tagscarletchapter-7direct-sumresilient-constructionpages-122-123fidelity-exact

Direct sum (Carlet, pp. 122--123). Let f:V_r\to\mathbb F_2 be t-resilient and g:V_s\to\mathbb F_2 be m-resilient, where t<r and m<s. Then h(x,y)=f(x)\oplus g(y) is (t+m+1)-resilient and W_h(a,b)=W_f(a)W_g(b). Moreover, \begin{aligned} \operatorname{nl}(h) &=2^{r+s-1} -\frac12(2^r-2\operatorname{nl}(f)) (2^s-2\operatorname{nl}(g))\\ &=2^r\operatorname{nl}(g)+2^s\operatorname{nl}(f) -2\operatorname{nl}(f)\operatorname{nl}(g). \end{aligned} Finally, h has no nonzero linear structure if and only if neither f nor g has a nonzero linear structure.

Lean code for Theorem6.4.2●11 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.card_f₂Support_append {r s : ℕ} (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  (FABL.f₂Support (Fin.append a b)).card =
    (FABL.f₂Support a).card + (FABL.f₂Support b).card

theorem CryptBoolean.card_f₂Support_append
  {r s : ℕ} (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  (FABL.f₂Support (Fin.append a b)).card =
    (FABL.f₂Support a).card +
      (FABL.f₂Support b).card

Hamming weight is additive under the canonical concatenation of binary cubes.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.walshTransform_natAbs_le_maxWalshMagnitude {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) (a : FABL.F₂Cube r) :
  (CryptBoolean.walshTransform f a).natAbs ≤
    CryptBoolean.maxWalshMagnitude f

theorem CryptBoolean.walshTransform_natAbs_le_maxWalshMagnitude
  {r : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (a : FABL.F₂Cube r) :
  (CryptBoolean.walshTransform f
        a).natAbs ≤
    CryptBoolean.maxWalshMagnitude f

Every raw Walsh magnitude is bounded by the maximum Walsh magnitude.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.maxWalshMagnitude_booleanDirectSum {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.maxWalshMagnitude (CryptBoolean.booleanDirectSum f g) =
    CryptBoolean.maxWalshMagnitude f * CryptBoolean.maxWalshMagnitude g

theorem CryptBoolean.maxWalshMagnitude_booleanDirectSum
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.booleanDirectSum f
        g) =
    CryptBoolean.maxWalshMagnitude f *
      CryptBoolean.maxWalshMagnitude g

The maximum raw Walsh magnitude of a direct sum is the product of the
maximum magnitudes of its summands.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

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

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

The direct sum of a `t`-resilient function and an `m`-resilient function
is `(t + m + 1)`-resilient.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.two_mul_nonlinearity_booleanDirectSum_add_product {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  2 * CryptBoolean.nonlinearity (CryptBoolean.booleanDirectSum f g) +
      (2 ^ r - 2 * CryptBoolean.nonlinearity f) *
        (2 ^ s - 2 * CryptBoolean.nonlinearity g) =
    2 ^ (r + s)

theorem CryptBoolean.two_mul_nonlinearity_booleanDirectSum_add_product
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  2 *
        CryptBoolean.nonlinearity
          (CryptBoolean.booleanDirectSum f
            g) +
      (2 ^ r -
          2 *
            CryptBoolean.nonlinearity f) *
        (2 ^ s -
          2 *
            CryptBoolean.nonlinearity g) =
    2 ^ (r + s)

Division-free nonlinearity identity for a Boolean direct sum.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.nonlinearity_booleanDirectSum_cast_eq_half_product
  {r s : ℕ} (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  ↑(CryptBoolean.nonlinearity (CryptBoolean.booleanDirectSum f g)) =
    2 ^ (r + s) / 2 -
      (2 ^ r - 2 * ↑(CryptBoolean.nonlinearity f)) *
          (2 ^ s - 2 * ↑(CryptBoolean.nonlinearity g)) /
        2

theorem CryptBoolean.nonlinearity_booleanDirectSum_cast_eq_half_product
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.booleanDirectSum f
          g)) =
    2 ^ (r + s) / 2 -
      (2 ^ r -
            2 *
              ↑(CryptBoolean.nonlinearity
                  f)) *
          (2 ^ s -
            2 *
              ↑(CryptBoolean.nonlinearity
                  g)) /
        2

Carlet's first direct-sum nonlinearity formula, in a total real-valued
form that retains the factor one half.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.nonlinearity_booleanDirectSum_cast_eq_source {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) (hsum : 0 < r + s) :
  ↑(CryptBoolean.nonlinearity (CryptBoolean.booleanDirectSum f g)) =
    2 ^ (r + s - 1) -
      (2 ^ r - 2 * ↑(CryptBoolean.nonlinearity f)) *
          (2 ^ s - 2 * ↑(CryptBoolean.nonlinearity g)) /
        2

theorem CryptBoolean.nonlinearity_booleanDirectSum_cast_eq_source
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s)
  (hsum : 0 < r + s) :
  ↑(CryptBoolean.nonlinearity
        (CryptBoolean.booleanDirectSum f
          g)) =
    2 ^ (r + s - 1) -
      (2 ^ r -
            2 *
              ↑(CryptBoolean.nonlinearity
                  f)) *
          (2 ^ s -
            2 *
              ↑(CryptBoolean.nonlinearity
                  g)) /
        2

Carlet's first displayed direct-sum formula in its positive-dimensional
source form.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.nonlinearity_booleanDirectSum {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.nonlinearity (CryptBoolean.booleanDirectSum f g) =
    2 ^ r * CryptBoolean.nonlinearity g +
        2 ^ s * CryptBoolean.nonlinearity f -
      2 * CryptBoolean.nonlinearity f * CryptBoolean.nonlinearity g

theorem CryptBoolean.nonlinearity_booleanDirectSum
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  CryptBoolean.nonlinearity
      (CryptBoolean.booleanDirectSum f
        g) =
    2 ^ r * CryptBoolean.nonlinearity g +
        2 ^ s *
          CryptBoolean.nonlinearity f -
      2 * CryptBoolean.nonlinearity f *
        CryptBoolean.nonlinearity g

Carlet's second direct-sum nonlinearity formula over the natural numbers.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.booleanDerivative_booleanDirectSum_append {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  FABL.booleanDerivative (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) =
    CryptBoolean.booleanDirectSum (FABL.booleanDerivative f a)
      (FABL.booleanDerivative g b)

theorem CryptBoolean.booleanDerivative_booleanDirectSum_append
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  FABL.booleanDerivative
      (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) =
    CryptBoolean.booleanDirectSum
      (FABL.booleanDerivative f a)
      (FABL.booleanDerivative g b)

Binary derivatives split over the two blocks of a Boolean direct sum.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.isLinearStructure_booleanDirectSum_append {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  CryptBoolean.IsLinearStructure (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) ↔
    CryptBoolean.IsLinearStructure f a ∧
      CryptBoolean.IsLinearStructure g b

theorem CryptBoolean.isLinearStructure_booleanDirectSum_append
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  CryptBoolean.IsLinearStructure
      (CryptBoolean.booleanDirectSum f g)
      (Fin.append a b) ↔
    CryptBoolean.IsLinearStructure f a ∧
      CryptBoolean.IsLinearStructure g b

A concatenated direction is a linear structure of a direct sum exactly
when both block directions are linear structures of their summands.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSum.lean

complete

theorem CryptBoolean.noNonzeroLinearStructure_booleanDirectSum {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  (∀ (e : FABL.F₂Cube (r + s)),
      e ≠ 0 →
        ¬CryptBoolean.IsLinearStructure
            (CryptBoolean.booleanDirectSum f g) e) ↔
    (∀ (a : FABL.F₂Cube r),
        a ≠ 0 → ¬CryptBoolean.IsLinearStructure f a) ∧
      ∀ (b : FABL.F₂Cube s), b ≠ 0 → ¬CryptBoolean.IsLinearStructure g b

theorem CryptBoolean.noNonzeroLinearStructure_booleanDirectSum
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  (∀ (e : FABL.F₂Cube (r + s)),
      e ≠ 0 →
        ¬CryptBoolean.IsLinearStructure
            (CryptBoolean.booleanDirectSum
              f g)
            e) ↔
    (∀ (a : FABL.F₂Cube r),
        a ≠ 0 →
          ¬CryptBoolean.IsLinearStructure
              f a) ∧
      ∀ (b : FABL.F₂Cube s),
        b ≠ 0 →
          ¬CryptBoolean.IsLinearStructure
              g b

A direct sum has no nonzero linear structure exactly when neither summand
has a nonzero linear structure.

Theorem6.4.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 2

Statement dependency previews

Preview

Definition 1.4.1

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-7direct-sumalgebraic-degreepage-123fidelity-exact

Degree of a direct sum (Carlet, p. 123). For Boolean functions f:V_r\to\mathbb F_2 and g:V_s\to\mathbb F_2 on disjoint coordinate blocks, \deg_{\mathrm{alg}}(f\oplus g) =\max(\deg_{\mathrm{alg}}f,\deg_{\mathrm{alg}}g).

Lean code for Theorem6.4.3●4 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_add_constant_eq {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) (c : FABL.𝔽₂) :
  FABL.functionAlgebraicDegree (f + fun x => c) =
    FABL.functionAlgebraicDegree f

theorem CryptBoolean.functionAlgebraicDegree_add_constant_eq
  {r : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (c : FABL.𝔽₂) :
  FABL.functionAlgebraicDegree
      (f + fun x => c) =
    FABL.functionAlgebraicDegree f

Adding a binary constant does not change the algebraic degree of a
Boolean function.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_eq_zero_iff_exists_constant {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  FABL.functionAlgebraicDegree f = 0 ↔ ∃ c, f = fun x => c

theorem CryptBoolean.functionAlgebraicDegree_eq_zero_iff_exists_constant
  {r : ℕ}
  (f : CryptBoolean.BooleanFunction r) :
  FABL.functionAlgebraicDegree f = 0 ↔
    ∃ c, f = fun x => c

A Boolean function has algebraic degree zero exactly when it is
constant.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_add_eq_right_of_lt {r : ℕ}
  (f g : CryptBoolean.BooleanFunction r)
  (hdegree :
    FABL.functionAlgebraicDegree f < FABL.functionAlgebraicDegree g) :
  FABL.functionAlgebraicDegree (f + g) = FABL.functionAlgebraicDegree g

theorem CryptBoolean.functionAlgebraicDegree_add_eq_right_of_lt
  {r : ℕ}
  (f g : CryptBoolean.BooleanFunction r)
  (hdegree :
    FABL.functionAlgebraicDegree f <
      FABL.functionAlgebraicDegree g) :
  FABL.functionAlgebraicDegree (f + g) =
    FABL.functionAlgebraicDegree g

Adding a strictly lower-degree Boolean function cannot change the
larger algebraic degree.

theoremdefined in CryptBoolean/Carlet/Chapter07/DirectSumDegree.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_booleanDirectSum {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  FABL.functionAlgebraicDegree (CryptBoolean.booleanDirectSum f g) =
    max (FABL.functionAlgebraicDegree f)
      (FABL.functionAlgebraicDegree g)

theorem CryptBoolean.functionAlgebraicDegree_booleanDirectSum
  {r s : ℕ}
  (f : CryptBoolean.BooleanFunction r)
  (g : CryptBoolean.BooleanFunction s) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.booleanDirectSum f
        g) =
    max (FABL.functionAlgebraicDegree f)
      (FABL.functionAlgebraicDegree g)

A Boolean direct sum has algebraic degree equal to the larger degree of
its two summands.

Theorem6.4.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 2

Statement dependency previews

Preview

Definition 1.7.1

Loading preview

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

Used by 3

Reverse dependency previews

Preview

Theorem 6.4.5

Loading preview

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

✓L∃∀N

Tagscarletchapter-7relation-65concatenationpage-123fidelity-exact

Relation (65) (Carlet, p. 123). For f,g:V_r\to\mathbb F_2, define h(x,z)=(z\oplus1)f(x)\oplus zg(x). Then W_h(a,c)=W_f(a)+(-1)^cW_g(a). If f and g are both m-resilient, then h is m-resilient. If additionally W_f(a)+W_g(a)=0 for every frequency a of weight m+1, then h is (m+1)-resilient.

Lean code for Theorem6.4.4●3 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/Concatenation.lean

complete

theorem CryptBoolean.walshTransform_hyperplaneExtension_append {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n)
  (b : FABL.𝔽₂) :
  CryptBoolean.walshTransform (CryptBoolean.hyperplaneExtension f g)
      (Fin.append a (CryptBoolean.singletonF₂Cube b)) =
    CryptBoolean.walshTransform f a +
      CryptBoolean.bitSignInt b * CryptBoolean.walshTransform g a

theorem CryptBoolean.walshTransform_hyperplaneExtension_append
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) (b : FABL.𝔽₂) :
  CryptBoolean.walshTransform
      (CryptBoolean.hyperplaneExtension f
        g)
      (Fin.append a
        (CryptBoolean.singletonF₂Cube
          b)) =
    CryptBoolean.walshTransform f a +
      CryptBoolean.bitSignInt b *
        CryptBoolean.walshTransform g a

Carlet Relation (65): the Walsh transform of the concatenation of `f`
and `g` is the sum or difference of their Walsh transforms according to the
last frequency coordinate.

theoremdefined in CryptBoolean/Carlet/Chapter07/Concatenation.lean

complete

theorem CryptBoolean.isResilient_hyperplaneExtension {n m : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (hm : m < n)
  (hf : CryptBoolean.IsResilient m f)
  (hg : CryptBoolean.IsResilient m g) :
  CryptBoolean.IsResilient m (CryptBoolean.hyperplaneExtension f g)

theorem CryptBoolean.isResilient_hyperplaneExtension
  {n m : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hm : m < n)
  (hf : CryptBoolean.IsResilient m f)
  (hg : CryptBoolean.IsResilient m g) :
  CryptBoolean.IsResilient m
    (CryptBoolean.hyperplaneExtension f g)

Concatenating two `m`-resilient functions preserves `m`-resiliency.

theoremdefined in CryptBoolean/Carlet/Chapter07/Concatenation.lean

complete

theorem CryptBoolean.isResilient_succ_hyperplaneExtension_of_walshCancellation
  {n m : ℕ} (f g : CryptBoolean.BooleanFunction n) (hm : m < n)
  (hf : CryptBoolean.IsResilient m f)
  (hg : CryptBoolean.IsResilient m g)
  (hcancel :
    ∀ (a : FABL.F₂Cube n),
      (FABL.f₂Support a).card = m + 1 →
        CryptBoolean.walshTransform f a +
            CryptBoolean.walshTransform g a =
          0) :
  CryptBoolean.IsResilient (m + 1)
    (CryptBoolean.hyperplaneExtension f g)

theorem CryptBoolean.isResilient_succ_hyperplaneExtension_of_walshCancellation
  {n m : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hm : m < n)
  (hf : CryptBoolean.IsResilient m f)
  (hg : CryptBoolean.IsResilient m g)
  (hcancel :
    ∀ (a : FABL.F₂Cube n),
      (FABL.f₂Support a).card = m + 1 →
        CryptBoolean.walshTransform f a +
            CryptBoolean.walshTransform g
              a =
          0) :
  CryptBoolean.IsResilient (m + 1)
    (CryptBoolean.hyperplaneExtension f g)

If the two spectra also cancel at every frequency of weight `m+1`, their
concatenation is `(m+1)`-resilient.

Theorem6.4.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-7concatenationnonlinearitypages-123-124fidelity-exact

Nonlinearity of concatenation (Carlet, pp. 123--124). For the preceding function h, \operatorname{nl}(h) \ge\operatorname{nl}(f)+\operatorname{nl}(g). If the Walsh supports of f and g are disjoint, then \operatorname{nl}(h) =2^{r-1}+\min(\operatorname{nl}(f),\operatorname{nl}(g)).

Lean code for Theorem6.4.5●3 theorems

theoremdefined in CryptBoolean/Carlet/Chapter07/Concatenation.lean

complete

theorem CryptBoolean.nonlinearity_add_le_hyperplaneExtension {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonlinearity f + CryptBoolean.nonlinearity g ≤
    CryptBoolean.nonlinearity (CryptBoolean.hyperplaneExtension f g)

theorem CryptBoolean.nonlinearity_add_le_hyperplaneExtension
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.nonlinearity f +
      CryptBoolean.nonlinearity g ≤
    CryptBoolean.nonlinearity
      (CryptBoolean.hyperplaneExtension f
        g)

The nonlinearity of a concatenation is at least the sum of the
nonlinearities of its two restrictions.

theoremdefined in CryptBoolean/Carlet/Chapter07/Concatenation.lean

complete

theorem CryptBoolean.maxWalshMagnitude_hyperplaneExtension_of_disjointWalshSupport
  {n : ℕ} (f g : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f a = 0 ∨
        CryptBoolean.walshTransform g a = 0) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.hyperplaneExtension f g) =
    max (CryptBoolean.maxWalshMagnitude f)
      (CryptBoolean.maxWalshMagnitude g)

theorem CryptBoolean.maxWalshMagnitude_hyperplaneExtension_of_disjointWalshSupport
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hdisjoint :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f a =
          0 ∨
        CryptBoolean.walshTransform g a =
          0) :
  CryptBoolean.maxWalshMagnitude
      (CryptBoolean.hyperplaneExtension f
        g) =
    max (CryptBoolean.maxWalshMagnitude f)
      (CryptBoolean.maxWalshMagnitude g)

Disjoint Walsh supports make the maximum Walsh magnitude of a
concatenation the larger of the two restriction magnitudes.

theoremdefined in CryptBoolean/Carlet/Chapter07/Concatenation.lean

complete

theorem CryptBoolean.nonlinearity_hyperplaneExtension_of_disjointWalshSupport
  {n : ℕ} (f g : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hdisjoint :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f a = 0 ∨
        CryptBoolean.walshTransform g a = 0) :
  CryptBoolean.nonlinearity (CryptBoolean.hyperplaneExtension f g) =
    2 ^ (n - 1) +
      min (CryptBoolean.nonlinearity f) (CryptBoolean.nonlinearity g)

theorem CryptBoolean.nonlinearity_hyperplaneExtension_of_disjointWalshSupport
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hn : 0 < n)
  (hdisjoint :
    ∀ (a : FABL.F₂Cube n),
      CryptBoolean.walshTransform f a =
          0 ∨
        CryptBoolean.walshTransform g a =
          0) :
  CryptBoolean.nonlinearity
      (CryptBoolean.hyperplaneExtension f
        g) =
    2 ^ (n - 1) +
      min (CryptBoolean.nonlinearity f)
        (CryptBoolean.nonlinearity g)

With disjoint Walsh supports, Carlet's concatenation has the exact
nonlinearity `2^(n-1) + min(nl(f), nl(g))`.

Theorem6.4.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.4.1

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-7concatenationalgebraic-degreelinear-structurespage-124fidelity-corrected-degenerate-cases

Degree and linear structures of concatenation (Carlet, p. 124). Put q=f\oplus g. Then h(x,z)=f(x)\oplus zq(x) and D_{(a,c)}h(x,z) =D_af(x)\oplus cq(x)\oplus zD_aq(x)\oplus cD_aq(x). If q\ne0 and \deg_{\mathrm{alg}}q=\max(\deg_{\mathrm{alg}}f,\deg_{\mathrm{alg}}g), then \deg_{\mathrm{alg}}h =1+\max(\deg_{\mathrm{alg}}f,\deg_{\mathrm{alg}}g). If 0<\deg_{\mathrm{alg}}q and \deg_{\mathrm{alg}}q\ge\deg_{\mathrm{alg}}f, no direction (a,1) is a linear structure. A direction (a,0) is a linear structure exactly when a is a common linear structure of f and g with the same derivative constant. Thus, under these hypotheses, absence of such a nonzero a implies that h has no nonzero linear structure.

Lean code for Theorem6.4.6●8 declarations

theoremdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

theorem CryptBoolean.hyperplaneExtension_append_eq_add_mul_difference {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (x : FABL.F₂Cube n)
  (z : FABL.𝔽₂) :
  CryptBoolean.hyperplaneExtension f g
      (Fin.append x (CryptBoolean.singletonF₂Cube z)) =
    f x + z * (f + g) x

theorem CryptBoolean.hyperplaneExtension_append_eq_add_mul_difference
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (x : FABL.F₂Cube n) (z : FABL.𝔽₂) :
  CryptBoolean.hyperplaneExtension f g
      (Fin.append x
        (CryptBoolean.singletonF₂Cube
          z)) =
    f x + z * (f + g) x

Concatenation is `f(x) + z(f+g)(x)` in polynomial form.

theoremdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

theorem CryptBoolean.hyperplaneExtension_eq_booleanDirectSum_add_booleanBlockProduct
  {n : ℕ} (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hyperplaneExtension f g =
    CryptBoolean.booleanDirectSum f 0 +
      CryptBoolean.booleanBlockProduct (f + g)
        CryptBoolean.oneVariableParity

theorem CryptBoolean.hyperplaneExtension_eq_booleanDirectSum_add_booleanBlockProduct
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) :
  CryptBoolean.hyperplaneExtension f g =
    CryptBoolean.booleanDirectSum f 0 +
      CryptBoolean.booleanBlockProduct
        (f + g)
        CryptBoolean.oneVariableParity

Polynomial decomposition of concatenation into a lifted restriction and
the product of the difference with the last coordinate.

theoremdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

theorem CryptBoolean.booleanDerivative_hyperplaneExtension_append {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (a x : FABL.F₂Cube n)
  (c z : FABL.𝔽₂) :
  FABL.booleanDerivative (CryptBoolean.hyperplaneExtension f g)
      (Fin.append a (CryptBoolean.singletonF₂Cube c))
      (Fin.append x (CryptBoolean.singletonF₂Cube z)) =
    FABL.booleanDerivative f a x + c * (f + g) x +
        z * FABL.booleanDerivative (f + g) a x +
      c * FABL.booleanDerivative (f + g) a x

theorem CryptBoolean.booleanDerivative_hyperplaneExtension_append
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (a x : FABL.F₂Cube n) (c z : FABL.𝔽₂) :
  FABL.booleanDerivative
      (CryptBoolean.hyperplaneExtension f
        g)
      (Fin.append a
        (CryptBoolean.singletonF₂Cube c))
      (Fin.append x
        (CryptBoolean.singletonF₂Cube
          z)) =
    FABL.booleanDerivative f a x +
          c * (f + g) x +
        z *
          FABL.booleanDerivative (f + g) a
            x +
      c *
        FABL.booleanDerivative (f + g) a x

The derivative of a concatenation in a split direction, in the source's
four-term form.

defdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

def CryptBoolean.HaveEqualConstantDerivative {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) : Prop

def CryptBoolean.HaveEqualConstantDerivative
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) : Prop

Two Boolean functions have the same constant derivative in direction
`a`.

theoremdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

theorem CryptBoolean.isLinearStructure_hyperplaneExtension_append_zero_iff
  {n : ℕ} (f g : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n) :
  CryptBoolean.IsLinearStructure (CryptBoolean.hyperplaneExtension f g)
      (Fin.append a (CryptBoolean.singletonF₂Cube 0)) ↔
    CryptBoolean.HaveEqualConstantDerivative f g a

theorem CryptBoolean.isLinearStructure_hyperplaneExtension_append_zero_iff
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n) :
  CryptBoolean.IsLinearStructure
      (CryptBoolean.hyperplaneExtension f
        g)
      (Fin.append a
        (CryptBoolean.singletonF₂Cube
          0)) ↔
    CryptBoolean.HaveEqualConstantDerivative
      f g a

A direction contained in the original coordinate block is a linear
structure of the concatenation exactly when the two restrictions have the
same constant derivative in that direction.

theoremdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

theorem CryptBoolean.functionAlgebraicDegree_hyperplaneExtension_eq_succ_max
  {n : ℕ} (f g : CryptBoolean.BooleanFunction n)
  (hdifference : f + g ≠ 0)
  (hdegree :
    FABL.functionAlgebraicDegree (f + g) =
      max (FABL.functionAlgebraicDegree f)
        (FABL.functionAlgebraicDegree g)) :
  FABL.functionAlgebraicDegree (CryptBoolean.hyperplaneExtension f g) =
    1 +
      max (FABL.functionAlgebraicDegree f)
        (FABL.functionAlgebraicDegree g)

theorem CryptBoolean.functionAlgebraicDegree_hyperplaneExtension_eq_succ_max
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hdifference : f + g ≠ 0)
  (hdegree :
    FABL.functionAlgebraicDegree (f + g) =
      max (FABL.functionAlgebraicDegree f)
        (FABL.functionAlgebraicDegree
          g)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.hyperplaneExtension f
        g) =
    1 +
      max (FABL.functionAlgebraicDegree f)
        (FABL.functionAlgebraicDegree g)

If the two restrictions differ in their highest-degree terms, the
concatenation gains one algebraic degree.

theoremdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

theorem CryptBoolean.not_isLinearStructure_hyperplaneExtension_append_one
  {n : ℕ} (f g : CryptBoolean.BooleanFunction n) (a : FABL.F₂Cube n)
  (hpositive : 0 < FABL.functionAlgebraicDegree (f + g))
  (hdegree :
    FABL.functionAlgebraicDegree f ≤
      FABL.functionAlgebraicDegree (f + g)) :
  ¬CryptBoolean.IsLinearStructure (CryptBoolean.hyperplaneExtension f g)
      (Fin.append a (CryptBoolean.singletonF₂Cube 1))

theorem CryptBoolean.not_isLinearStructure_hyperplaneExtension_append_one
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (a : FABL.F₂Cube n)
  (hpositive :
    0 <
      FABL.functionAlgebraicDegree
        (f + g))
  (hdegree :
    FABL.functionAlgebraicDegree f ≤
      FABL.functionAlgebraicDegree
        (f + g)) :
  ¬CryptBoolean.IsLinearStructure
      (CryptBoolean.hyperplaneExtension f
        g)
      (Fin.append a
        (CryptBoolean.singletonF₂Cube 1))

Under the source's positive-degree hypothesis, no direction crossing the
two restrictions can be a linear structure.

theoremdefined in CryptBoolean/Carlet/Chapter07/ConcatenationStructure.lean

complete

theorem CryptBoolean.no_nonzero_linearStructure_hyperplaneExtension {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hpositive : 0 < FABL.functionAlgebraicDegree (f + g))
  (hdegree :
    FABL.functionAlgebraicDegree f ≤
      FABL.functionAlgebraicDegree (f + g))
  (hcommon :
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 → ¬CryptBoolean.HaveEqualConstantDerivative f g a)
  (u : FABL.F₂Cube (n + 1)) :
  u ≠ 0 →
    ¬CryptBoolean.IsLinearStructure
        (CryptBoolean.hyperplaneExtension f g) u

theorem CryptBoolean.no_nonzero_linearStructure_hyperplaneExtension
  {n : ℕ}
  (f g : CryptBoolean.BooleanFunction n)
  (hpositive :
    0 <
      FABL.functionAlgebraicDegree
        (f + g))
  (hdegree :
    FABL.functionAlgebraicDegree f ≤
      FABL.functionAlgebraicDegree
        (f + g))
  (hcommon :
    ∀ (a : FABL.F₂Cube n),
      a ≠ 0 →
        ¬CryptBoolean.HaveEqualConstantDerivative
            f g a)
  (u : FABL.F₂Cube (n + 1)) :
  u ≠ 0 →
    ¬CryptBoolean.IsLinearStructure
        (CryptBoolean.hyperplaneExtension
          f g)
        u

If neither a crossing direction nor a nonzero common constant-derivative
direction is available, the concatenation has no nonzero linear structure.

Theorem6.4.7

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.4.2

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-7generalized-concatenationresiliencypage-124fidelity-exact

Generalized concatenation (Carlet, p. 124). Let (f_y)_{y\in V_s} be a family of r-variable m-resilient functions and define F(x,y)=f_y(x). Then F is m-resilient, and for every a\in V_r and b\in V_s, W_F(a,b)=\sum_{y\in V_s}(-1)^{b\cdot y}W_{f_y}(a).

Lean code for Theorem6.4.7●5 declarations

defdefined in CryptBoolean/Carlet/Chapter07/GeneralConcatenation.lean

complete

def CryptBoolean.familyConcatenation {r s : ℕ}
  (f : FABL.F₂Cube s → CryptBoolean.BooleanFunction r) :
  CryptBoolean.BooleanFunction (r + s)

def CryptBoolean.familyConcatenation {r s : ℕ}
  (f :
    FABL.F₂Cube s →
      CryptBoolean.BooleanFunction r) :
  CryptBoolean.BooleanFunction (r + s)

A family indexed by the second coordinate block defines a Boolean
function on the joined cube.

theoremdefined in CryptBoolean/Carlet/Chapter07/GeneralConcatenation.lean

complete

theorem CryptBoolean.familyConcatenation_append {r s : ℕ}
  (f : FABL.F₂Cube s → CryptBoolean.BooleanFunction r)
  (x : FABL.F₂Cube r) (y : FABL.F₂Cube s) :
  CryptBoolean.familyConcatenation f (Fin.append x y) = f y x

theorem CryptBoolean.familyConcatenation_append
  {r s : ℕ}
  (f :
    FABL.F₂Cube s →
      CryptBoolean.BooleanFunction r)
  (x : FABL.F₂Cube r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.familyConcatenation f
      (Fin.append x y) =
    f y x

theoremdefined in CryptBoolean/Carlet/Chapter07/GeneralConcatenation.lean

complete

theorem CryptBoolean.firstBlockSlice_familyConcatenation {r s : ℕ}
  (f : FABL.F₂Cube s → CryptBoolean.BooleanFunction r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.firstBlockSlice (CryptBoolean.familyConcatenation f) y =
    f y

theorem CryptBoolean.firstBlockSlice_familyConcatenation
  {r s : ℕ}
  (f :
    FABL.F₂Cube s →
      CryptBoolean.BooleanFunction r)
  (y : FABL.F₂Cube s) :
  CryptBoolean.firstBlockSlice
      (CryptBoolean.familyConcatenation f)
      y =
    f y

theoremdefined in CryptBoolean/Carlet/Chapter07/GeneralConcatenation.lean

complete

theorem CryptBoolean.walshTransform_familyConcatenation_append {r s : ℕ}
  (f : FABL.F₂Cube s → CryptBoolean.BooleanFunction r)
  (a : FABL.F₂Cube r) (b : FABL.F₂Cube s) :
  CryptBoolean.walshTransform (CryptBoolean.familyConcatenation f)
      (Fin.append a b) =
    ∑ y,
      CryptBoolean.bitSignInt (FABL.f₂DotProduct b y) *
        CryptBoolean.walshTransform (f y) a

theorem CryptBoolean.walshTransform_familyConcatenation_append
  {r s : ℕ}
  (f :
    FABL.F₂Cube s →
      CryptBoolean.BooleanFunction r)
  (a : FABL.F₂Cube r)
  (b : FABL.F₂Cube s) :
  CryptBoolean.walshTransform
      (CryptBoolean.familyConcatenation f)
      (Fin.append a b) =
    ∑ y,
      CryptBoolean.bitSignInt
          (FABL.f₂DotProduct b y) *
        CryptBoolean.walshTransform (f y)
          a

The Walsh transform of a generalized concatenation is the signed sum of
the Walsh transforms of its slices.

theoremdefined in CryptBoolean/Carlet/Chapter07/GeneralConcatenation.lean

complete

theorem CryptBoolean.isResilient_familyConcatenation {r s m : ℕ}
  (f : FABL.F₂Cube s → CryptBoolean.BooleanFunction r) (hm : m < r)
  (hf : ∀ (y : FABL.F₂Cube s), CryptBoolean.IsResilient m (f y)) :
  CryptBoolean.IsResilient m (CryptBoolean.familyConcatenation f)

theorem CryptBoolean.isResilient_familyConcatenation
  {r s m : ℕ}
  (f :
    FABL.F₂Cube s →
      CryptBoolean.BooleanFunction r)
  (hm : m < r)
  (hf :
    ∀ (y : FABL.F₂Cube s),
      CryptBoolean.IsResilient m (f y)) :
  CryptBoolean.IsResilient m
    (CryptBoolean.familyConcatenation f)

A generalized concatenation of `m`-resilient slices is
`m`-resilient.