4.5. Functions admitting partial covering sequences🔗

Definition4.5.1

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

uses 1

Used by 4

Reverse dependency previews

Preview

Theorem 4.5.2

Loading preview

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

✓L∃∀N

Tagscarletchapter-5definition-5covering-sequencepage-73fidelity-exact-integer-valued

Covering sequences (Carlet, Definition 5, p. 73). Let f:V_n\to\mathbb F_2 and let \lambda=(\lambda_a)_{a\in V_n} be integer-valued. It is a covering sequence of f with level \rho\in \mathbb Z when the integer-valued function x\longmapsto\sum_{a\in V_n}\lambda_a D_af(x) is constantly \rho, where each derivative bit is viewed in \mathbb Z. The sequence is nontrivial when \rho\ne0.

Lean code for Definition4.5.1●4 definitions

defdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

def CryptBoolean.bitValueInt (b : FABL.𝔽₂) : ℤ

def CryptBoolean.bitValueInt (b : FABL.𝔽₂) : ℤ

The canonical integer value of a binary scalar.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

def CryptBoolean.integerWalshTransform {n : ℕ} (coeff : FABL.F₂Cube n → ℤ)
  (b : FABL.F₂Cube n) : ℤ

def CryptBoolean.integerWalshTransform {n : ℕ}
  (coeff : FABL.F₂Cube n → ℤ)
  (b : FABL.F₂Cube n) : ℤ

The unnormalized integer Walsh transform of an integer-valued cube function.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

def CryptBoolean.weightedDerivativeSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (x : FABL.F₂Cube n) : ℤ

def CryptBoolean.weightedDerivativeSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ)
  (x : FABL.F₂Cube n) : ℤ

The integer sum of the derivatives weighted by a sequence.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

def CryptBoolean.IsCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ : ℤ) : Prop

def CryptBoolean.IsCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ) :
  Prop

An integer sequence covers `f` at level `ρ` when its weighted derivative sum is constant.

Carlet's printed definition uses integer coefficients; footnote 31 also permits real or complex coefficients.

Theorem4.5.2

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Theorem 1.7.3

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-5covering-sequencebalancednessreference-94page-73fidelity-exact

Covering sequences and balancedness (Carlet, p. 73). Every Boolean function admitting a nontrivial covering sequence is balanced. Conversely, every balanced n-variable Boolean function admits the constant sequence \lambda_a=1 as a covering sequence of level 2^{n-1}.

Lean code for Theorem4.5.2●4 theorems

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.integerWalshTransform_one {n : ℕ} (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform (fun x => 1) b =
    if b = 0 then 2 ^ n else 0

theorem CryptBoolean.integerWalshTransform_one
  {n : ℕ} (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (fun x => 1) b =
    if b = 0 then 2 ^ n else 0

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isBalanced_of_isCoveringSequence_of_ne_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ : ℤ) (hcover : CryptBoolean.IsCoveringSequence f coeff ρ)
  (hρ : ρ ≠ 0) : CryptBoolean.IsBalanced f

theorem CryptBoolean.isBalanced_of_isCoveringSequence_of_ne_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ)
  (hcover :
    CryptBoolean.IsCoveringSequence f
      coeff ρ)
  (hρ : ρ ≠ 0) : CryptBoolean.IsBalanced f

A covering sequence at a nonzero level forces balancedness.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isCoveringSequence_one_of_isBalanced {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hbalanced : CryptBoolean.IsBalanced f) :
  CryptBoolean.IsCoveringSequence f (fun x => 1) (2 ^ (n - 1))

theorem CryptBoolean.isCoveringSequence_one_of_isBalanced
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hbalanced :
    CryptBoolean.IsBalanced f) :
  CryptBoolean.IsCoveringSequence f
    (fun x => 1) (2 ^ (n - 1))

Every balanced Boolean function is covered by the constant-one sequence at level
`2^(n-1)`.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isBalanced_iff_exists_nontrivialCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBalanced f ↔
    ∃ coeff ρ, CryptBoolean.IsCoveringSequence f coeff ρ ∧ ρ ≠ 0

theorem CryptBoolean.isBalanced_iff_exists_nontrivialCoveringSequence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBalanced f ↔
    ∃ coeff ρ,
      CryptBoolean.IsCoveringSequence f
          coeff ρ ∧
        ρ ≠ 0

A Boolean function is balanced exactly when it admits a covering sequence at a
nonzero level.

Theorem4.5.3

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Definition 1.7.1

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-5covering-sequencewalsh-characterizationreference-94pages-73-74fidelity-exact-with-transform-identities

Walsh characterization of covering sequences (Carlet, pp. 73--74). For an integer sequence \lambda on V_n, define \widehat\lambda(b)=\sum_{a\in V_n}\lambda_a(-1)^{a\mathbin\cdot b}. Then \lambda is a covering sequence of f with level \rho if and only if \widehat\lambda(b)=\widehat\lambda(0)-2\rho for every b with W_f(b)\ne0; equivalently, \widehat\lambda is constant with that value on the Walsh support of f.

Lean code for Theorem4.5.3●12 declarations

defdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

def CryptBoolean.weightedTranslatedSignSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (x : FABL.F₂Cube n) : ℤ

def CryptBoolean.weightedTranslatedSignSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ)
  (x : FABL.F₂Cube n) : ℤ

The sequence-weighted sum of translated signs used in the covering proofs.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.bitSignInt_eq_one_sub_two_mul_bitValueInt (b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt b = 1 - 2 * CryptBoolean.bitValueInt b

theorem CryptBoolean.bitSignInt_eq_one_sub_two_mul_bitValueInt
  (b : FABL.𝔽₂) :
  CryptBoolean.bitSignInt b =
    1 - 2 * CryptBoolean.bitValueInt b

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.bitSignInt_booleanDerivative_mul_left {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (a x : FABL.F₂Cube n) :
  CryptBoolean.bitSignInt (f (x + a)) =
    CryptBoolean.bitSignInt (f x) *
      CryptBoolean.bitSignInt (FABL.booleanDerivative f a x)

theorem CryptBoolean.bitSignInt_booleanDerivative_mul_left
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (a x : FABL.F₂Cube n) :
  CryptBoolean.bitSignInt (f (x + a)) =
    CryptBoolean.bitSignInt (f x) *
      CryptBoolean.bitSignInt
        (FABL.booleanDerivative f a x)

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.weightedTranslatedSignSum_eq {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (x : FABL.F₂Cube n) :
  CryptBoolean.weightedTranslatedSignSum f coeff x =
    CryptBoolean.bitSignInt (f x) *
      (CryptBoolean.integerWalshTransform coeff 0 -
        2 * CryptBoolean.weightedDerivativeSum f coeff x)

theorem CryptBoolean.weightedTranslatedSignSum_eq
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ)
  (x : FABL.F₂Cube n) :
  CryptBoolean.weightedTranslatedSignSum f
      coeff x =
    CryptBoolean.bitSignInt (f x) *
      (CryptBoolean.integerWalshTransform
          coeff 0 -
        2 *
          CryptBoolean.weightedDerivativeSum
            f coeff x)

The shared pointwise sign identity underlying both covering theorems.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.integerWalshTransform_mul_bitSignInt {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (κ : FABL.F₂Cube n → ℤ)
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (fun x => κ x * CryptBoolean.bitSignInt (f x)) b =
    ∑ x, κ x * CryptBoolean.walshTerm f b x

theorem CryptBoolean.integerWalshTransform_mul_bitSignInt
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (κ : FABL.F₂Cube n → ℤ)
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (fun x =>
        κ x *
          CryptBoolean.bitSignInt (f x))
      b =
    ∑ x,
      κ x * CryptBoolean.walshTerm f b x

Transforming a sign-weighted integer function inserts the Walsh summand.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.integerWalshTransform_weightedTranslatedSignSum {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.weightedTranslatedSignSum f coeff) b =
    CryptBoolean.integerWalshTransform coeff b *
      CryptBoolean.walshTransform f b

theorem CryptBoolean.integerWalshTransform_weightedTranslatedSignSum
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ)
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.weightedTranslatedSignSum
        f coeff)
      b =
    CryptBoolean.integerWalshTransform
        coeff b *
      CryptBoolean.walshTransform f b

The Walsh transform of the weighted translated-sign sum factors pointwise.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.integerWalshTransform_const_mul_bitSignInt {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (c : ℤ) (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (fun x => c * CryptBoolean.bitSignInt (f x)) b =
    c * CryptBoolean.walshTransform f b

theorem CryptBoolean.integerWalshTransform_const_mul_bitSignInt
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (c : ℤ) (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (fun x =>
        c * CryptBoolean.bitSignInt (f x))
      b =
    c * CryptBoolean.walshTransform f b

Multiplying the sign of a Boolean function by a constant scales its Walsh transform.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.integerWalshTransform_cast_eq_rawFourierTransform {n : ℕ}
  (coeff : FABL.F₂Cube n → ℤ) (b : FABL.F₂Cube n) :
  ↑(CryptBoolean.integerWalshTransform coeff b) =
    CryptBoolean.rawFourierTransform (fun x => ↑(coeff x)) b

theorem CryptBoolean.integerWalshTransform_cast_eq_rawFourierTransform
  {n : ℕ} (coeff : FABL.F₂Cube n → ℤ)
  (b : FABL.F₂Cube n) :
  ↑(CryptBoolean.integerWalshTransform
        coeff b) =
    CryptBoolean.rawFourierTransform
      (fun x => ↑(coeff x)) b

Casting the integer transform to the reals recovers Chapter 2's raw transform.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.integerWalshTransform_involution {n : ℕ}
  (coeff : FABL.F₂Cube n → ℤ) (x : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.integerWalshTransform coeff) x =
    2 ^ n * coeff x

theorem CryptBoolean.integerWalshTransform_involution
  {n : ℕ} (coeff : FABL.F₂Cube n → ℤ)
  (x : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.integerWalshTransform
        coeff)
      x =
    2 ^ n * coeff x

The integer Walsh transform is involutive up to multiplication by the cube cardinality.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.integerWalshTransform_injective {n : ℕ} :
  Function.Injective CryptBoolean.integerWalshTransform

theorem CryptBoolean.integerWalshTransform_injective
  {n : ℕ} :
  Function.Injective
    CryptBoolean.integerWalshTransform

Equality of integer Walsh transforms implies equality of the original functions.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.isCoveringSequence_iff_integerWalshTransform {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ : ℤ) :
  CryptBoolean.IsCoveringSequence f coeff ρ ↔
    ∀ (b : FABL.F₂Cube n),
      (CryptBoolean.integerWalshTransform coeff b -
              CryptBoolean.integerWalshTransform coeff 0 +
            2 * ρ) *
          CryptBoolean.walshTransform f b =
        0

theorem CryptBoolean.isCoveringSequence_iff_integerWalshTransform
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ) :
  CryptBoolean.IsCoveringSequence f coeff
      ρ ↔
    ∀ (b : FABL.F₂Cube n),
      (CryptBoolean.integerWalshTransform
                coeff b -
              CryptBoolean.integerWalshTransform
                coeff 0 +
            2 * ρ) *
          CryptBoolean.walshTransform f
            b =
        0

Carlet's Walsh-support characterization of a covering sequence.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.isCoveringSequence_iff_transform_eq_on_walshSupport {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ : ℤ) :
  CryptBoolean.IsCoveringSequence f coeff ρ ↔
    ∀ (b : FABL.F₂Cube n),
      CryptBoolean.walshTransform f b ≠ 0 →
        CryptBoolean.integerWalshTransform coeff b =
          CryptBoolean.integerWalshTransform coeff 0 - 2 * ρ

theorem CryptBoolean.isCoveringSequence_iff_transform_eq_on_walshSupport
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ) :
  CryptBoolean.IsCoveringSequence f coeff
      ρ ↔
    ∀ (b : FABL.F₂Cube n),
      CryptBoolean.walshTransform f b ≠
          0 →
        CryptBoolean.integerWalshTransform
            coeff b =
          CryptBoolean.integerWalshTransform
              coeff 0 -
            2 * ρ

Conditional form of the covering characterization on the Walsh support.

Theorem4.5.4

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Theorem 3.4.2

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-5covering-sequenceresiliencyreference-94page-74fidelity-exact-on-feasible-orders

Covering sequences and resiliency (Carlet, p. 74). Suppose \lambda is a covering sequence of f with level \rho, put \mu=\widehat\lambda(0)-2\rho, and suppose k+1 is the minimum Hamming weight of a nonzero b satisfying \widehat\lambda(b)=\mu. Then f is kth-order correlation immune, and if \rho\ne0 it is k-resilient. Conversely, if f is kth-order correlation immune but not (k+1)th-order correlation immune, there is a covering sequence with this minimum equal to k+1; if f is k-resilient but not (k+1)-resilient, such a sequence can be chosen nontrivial.

Lean code for Theorem4.5.4●12 declarations

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.IsMinimumNonzeroTransformFiberWeight {n : ℕ}
  (coeff : FABL.F₂Cube n → ℤ) (μ : ℤ) (weight : ℕ) : Prop

def CryptBoolean.IsMinimumNonzeroTransformFiberWeight
  {n : ℕ} (coeff : FABL.F₂Cube n → ℤ)
  (μ : ℤ) (weight : ℕ) : Prop

A natural number is the minimum weight of a nonzero frequency in an integer
Walsh-transform fiber.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isCorrelationImmune_of_coveringSequence_of_minimumTransformFiberWeight
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ) (hn : 0 < n) (hm : m < n)
  (hcover : CryptBoolean.IsCoveringSequence f coeff ρ)
  (hminimum :
    CryptBoolean.IsMinimumNonzeroTransformFiberWeight coeff
      (CryptBoolean.integerWalshTransform coeff 0 - 2 * ρ) (m + 1)) :
  CryptBoolean.IsCorrelationImmune m f

theorem CryptBoolean.isCorrelationImmune_of_coveringSequence_of_minimumTransformFiberWeight
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ)
  (hn : 0 < n) (hm : m < n)
  (hcover :
    CryptBoolean.IsCoveringSequence f
      coeff ρ)
  (hminimum :
    CryptBoolean.IsMinimumNonzeroTransformFiberWeight
      coeff
      (CryptBoolean.integerWalshTransform
          coeff 0 -
        2 * ρ)
      (m + 1)) :
  CryptBoolean.IsCorrelationImmune m f

A covering sequence whose distinguished nonzero transform fiber begins in
weight `m + 1` makes the covered function correlation immune of order `m`.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isResilient_of_coveringSequence_of_minimumTransformFiberWeight
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ) (hn : 0 < n) (hm : m < n)
  (hcover : CryptBoolean.IsCoveringSequence f coeff ρ) (hρ : ρ ≠ 0)
  (hminimum :
    CryptBoolean.IsMinimumNonzeroTransformFiberWeight coeff
      (CryptBoolean.integerWalshTransform coeff 0 - 2 * ρ) (m + 1)) :
  CryptBoolean.IsResilient m f

theorem CryptBoolean.isResilient_of_coveringSequence_of_minimumTransformFiberWeight
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ : ℤ)
  (hn : 0 < n) (hm : m < n)
  (hcover :
    CryptBoolean.IsCoveringSequence f
      coeff ρ)
  (hρ : ρ ≠ 0)
  (hminimum :
    CryptBoolean.IsMinimumNonzeroTransformFiberWeight
      coeff
      (CryptBoolean.integerWalshTransform
          coeff 0 -
        2 * ρ)
      (m + 1)) :
  CryptBoolean.IsResilient m f

At a nonzero covering level, the same minimum-fiber hypothesis makes the
covered function resilient of order `m`.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.walshZeroIndicator {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) : ℤ

def CryptBoolean.walshZeroIndicator {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) : ℤ

The indicator of the zero Walsh spectrum, regarded as an integer sequence.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.walshZeroCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : FABL.F₂Cube n → ℤ

def CryptBoolean.walshZeroCoveringSequence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  FABL.F₂Cube n → ℤ

The inverse integer Walsh transform used in the covering-sequence converses.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.walshZeroCoveringLevel {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℤ

def CryptBoolean.walshZeroCoveringLevel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) : ℤ

The covering level associated with the zero-spectrum construction.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.integerWalshTransform_walshZeroCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.walshZeroCoveringSequence f) b =
    if CryptBoolean.walshTransform f b = 0 then 2 ^ n else 0

theorem CryptBoolean.integerWalshTransform_walshZeroCoveringSequence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.walshZeroCoveringSequence
        f)
      b =
    if
        CryptBoolean.walshTransform f b =
          0 then
      2 ^ n
    else 0

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.integerWalshTransform_walshZeroCoveringSequence_eq_zero_iff
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
        (CryptBoolean.walshZeroCoveringSequence f) b =
      0 ↔
    CryptBoolean.walshTransform f b ≠ 0

theorem CryptBoolean.integerWalshTransform_walshZeroCoveringSequence_eq_zero_iff
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
        (CryptBoolean.walshZeroCoveringSequence
          f)
        b =
      0 ↔
    CryptBoolean.walshTransform f b ≠ 0

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.walshZeroCoveringSequence_transformTarget_eq_zero {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) :
  CryptBoolean.integerWalshTransform
        (CryptBoolean.walshZeroCoveringSequence f) 0 -
      2 * CryptBoolean.walshZeroCoveringLevel f =
    0

theorem CryptBoolean.walshZeroCoveringSequence_transformTarget_eq_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  CryptBoolean.integerWalshTransform
        (CryptBoolean.walshZeroCoveringSequence
          f)
        0 -
      2 *
        CryptBoolean.walshZeroCoveringLevel
          f =
    0

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isCoveringSequence_walshZeroCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) :
  CryptBoolean.IsCoveringSequence f
    (CryptBoolean.walshZeroCoveringSequence f)
    (CryptBoolean.walshZeroCoveringLevel f)

theorem CryptBoolean.isCoveringSequence_walshZeroCoveringSequence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  CryptBoolean.IsCoveringSequence f
    (CryptBoolean.walshZeroCoveringSequence
      f)
    (CryptBoolean.walshZeroCoveringLevel
      f)

The zero-spectrum construction is a covering sequence.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.exists_coveringSequence_of_correlationImmune_not_succ
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hm : m + 1 < n) (himmune : CryptBoolean.IsCorrelationImmune m f)
  (hnotImmune : ¬CryptBoolean.IsCorrelationImmune (m + 1) f) :
  ∃ coeff ρ,
    CryptBoolean.IsCoveringSequence f coeff ρ ∧
      CryptBoolean.IsMinimumNonzeroTransformFiberWeight coeff
        (CryptBoolean.integerWalshTransform coeff 0 - 2 * ρ) (m + 1)

theorem CryptBoolean.exists_coveringSequence_of_correlationImmune_not_succ
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m + 1 < n)
  (himmune :
    CryptBoolean.IsCorrelationImmune m f)
  (hnotImmune :
    ¬CryptBoolean.IsCorrelationImmune
        (m + 1) f) :
  ∃ coeff ρ,
    CryptBoolean.IsCoveringSequence f
        coeff ρ ∧
      CryptBoolean.IsMinimumNonzeroTransformFiberWeight
        coeff
        (CryptBoolean.integerWalshTransform
            coeff 0 -
          2 * ρ)
        (m + 1)

If `f` is correlation immune of order `m` but not of order `m + 1`, then
it admits a covering sequence whose distinguished nonzero transform fiber has
minimum weight `m + 1`.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.exists_nontrivialCoveringSequence_of_resilient_not_succ
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hm : m + 1 < n) (hresilient : CryptBoolean.IsResilient m f)
  (hnotResilient : ¬CryptBoolean.IsResilient (m + 1) f) :
  ∃ coeff ρ,
    CryptBoolean.IsCoveringSequence f coeff ρ ∧
      ρ ≠ 0 ∧
        CryptBoolean.IsMinimumNonzeroTransformFiberWeight coeff
          (CryptBoolean.integerWalshTransform coeff 0 - 2 * ρ) (m + 1)

theorem CryptBoolean.exists_nontrivialCoveringSequence_of_resilient_not_succ
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m + 1 < n)
  (hresilient :
    CryptBoolean.IsResilient m f)
  (hnotResilient :
    ¬CryptBoolean.IsResilient (m + 1) f) :
  ∃ coeff ρ,
    CryptBoolean.IsCoveringSequence f
        coeff ρ ∧
      ρ ≠ 0 ∧
        CryptBoolean.IsMinimumNonzeroTransformFiberWeight
          coeff
          (CryptBoolean.integerWalshTransform
              coeff 0 -
            2 * ρ)
          (m + 1)

If `f` is resilient of order `m` but not of order `m + 1`, the converse
covering sequence can be chosen at a nonzero level.

Definition4.5.5

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 4.5.1

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-5regular-functionscovering-sequenceresiliencyreference-94page-74fidelity-exact-on-positive-natural-levels

Regular functions (Carlet, p. 74). A Boolean function is regular when the indicator of the set of weight-one directions is a covering sequence. If its level is \rho\ge1, then it is (\rho-1)-resilient. More generally, the same conclusion holds when the covering sequence is the indicator of a set of directions with pairwise disjoint supports.

Lean code for Definition4.5.5●10 declarations

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.weightOneDirectionIndicator {n : ℕ} (a : FABL.F₂Cube n) : ℤ

def CryptBoolean.weightOneDirectionIndicator
  {n : ℕ} (a : FABL.F₂Cube n) : ℤ

The integer indicator of the weight-one directions.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.IsRegularAtLevel {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (ρ : ℤ) : Prop

def CryptBoolean.IsRegularAtLevel {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (ρ : ℤ) : Prop

A Boolean function is regular at level `ρ` when the weight-one direction
indicator covers it at that level.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.IsRegular {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  Prop

def CryptBoolean.IsRegular {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  Prop

Carlet's regular Boolean functions are those regular at some integer level.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.integerWalshTransform_weightOneDirectionIndicator {n : ℕ}
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      CryptBoolean.weightOneDirectionIndicator b =
    ↑n - 2 * ↑(FABL.f₂Support b).card

theorem CryptBoolean.integerWalshTransform_weightOneDirectionIndicator
  {n : ℕ} (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      CryptBoolean.weightOneDirectionIndicator
      b =
    ↑n - 2 * ↑(FABL.f₂Support b).card

The integer Walsh transform of the weight-one direction indicator.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isResilient_natPred_of_isRegularAtLevel {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (ρ : ℕ) (hn : 0 < n) (hρ : 0 < ρ)
  (hregular : CryptBoolean.IsRegularAtLevel f ↑ρ) :
  CryptBoolean.IsResilient (ρ - 1) f

theorem CryptBoolean.isResilient_natPred_of_isRegularAtLevel
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (ρ : ℕ) (hn : 0 < n) (hρ : 0 < ρ)
  (hregular :
    CryptBoolean.IsRegularAtLevel f ↑ρ) :
  CryptBoolean.IsResilient (ρ - 1) f

A regular Boolean function covered at a positive natural level `ρ` is
resilient of order `ρ - 1`.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.directionFamilyIndicator {n : ℕ}
  (directions : Finset (FABL.F₂Cube n)) (a : FABL.F₂Cube n) : ℤ

def CryptBoolean.directionFamilyIndicator
  {n : ℕ}
  (directions : Finset (FABL.F₂Cube n))
  (a : FABL.F₂Cube n) : ℤ

The integer indicator of a finite family of directions.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

def CryptBoolean.HasPairwiseDisjointSupports {n : ℕ}
  (directions : Finset (FABL.F₂Cube n)) : Prop

def CryptBoolean.HasPairwiseDisjointSupports
  {n : ℕ}
  (directions : Finset (FABL.F₂Cube n)) :
  Prop

The supports of distinct directions in a family are disjoint.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.integerWalshTransform_directionFamilyIndicator {n : ℕ}
  (directions : Finset (FABL.F₂Cube n)) (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.directionFamilyIndicator directions) b =
    ↑directions.card -
      2 * ↑{a ∈ directions | FABL.f₂DotProduct a b = 1}.card

theorem CryptBoolean.integerWalshTransform_directionFamilyIndicator
  {n : ℕ}
  (directions : Finset (FABL.F₂Cube n))
  (b : FABL.F₂Cube n) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.directionFamilyIndicator
        directions)
      b =
    ↑directions.card -
      2 *
        ↑{a ∈ directions |
              FABL.f₂DotProduct a b =
                1}.card

The transform of a direction-family indicator counts directions having
odd scalar product with the frequency.

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.integerWalshTransform_directionFamilyIndicator_zero {n : ℕ}
  (directions : Finset (FABL.F₂Cube n)) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.directionFamilyIndicator directions) 0 =
    ↑directions.card

theorem CryptBoolean.integerWalshTransform_directionFamilyIndicator_zero
  {n : ℕ}
  (directions : Finset (FABL.F₂Cube n)) :
  CryptBoolean.integerWalshTransform
      (CryptBoolean.directionFamilyIndicator
        directions)
      0 =
    ↑directions.card

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringConsequences.lean

complete

theorem CryptBoolean.isResilient_natPred_of_pairwiseDisjointSupportCoveringSequence
  {n : ℕ} (directions : Finset (FABL.F₂Cube n))
  (hdisjoint : CryptBoolean.HasPairwiseDisjointSupports directions)
  (f : CryptBoolean.BooleanFunction n) (ρ : ℕ) (hn : 0 < n) (hρ : 0 < ρ)
  (hcover :
    CryptBoolean.IsCoveringSequence f
      (CryptBoolean.directionFamilyIndicator directions) ↑ρ) :
  CryptBoolean.IsResilient (ρ - 1) f

theorem CryptBoolean.isResilient_natPred_of_pairwiseDisjointSupportCoveringSequence
  {n : ℕ}
  (directions : Finset (FABL.F₂Cube n))
  (hdisjoint :
    CryptBoolean.HasPairwiseDisjointSupports
      directions)
  (f : CryptBoolean.BooleanFunction n)
  (ρ : ℕ) (hn : 0 < n) (hρ : 0 < ρ)
  (hcover :
    CryptBoolean.IsCoveringSequence f
      (CryptBoolean.directionFamilyIndicator
        directions)
      ↑ρ) :
  CryptBoolean.IsResilient (ρ - 1) f

If the indicator of a family of directions with pairwise disjoint supports
covers `f` at a positive natural level `ρ`, then `f` is resilient of order
`ρ - 1`.

Definition4.5.6

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

uses 1

Used by 2

Reverse dependency previews

Preview

Theorem 4.5.7

Loading preview

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

✓L∃∀N

Tagscarletchapter-5definition-6partial-covering-sequencereference-68page-74fidelity-exact-integer-valued

Partial covering sequences (Carlet, Definition 6, p. 74). An integer sequence \lambda=(\lambda_a)_{a\in V_n} is a partial covering sequence of f with levels \rho,\rho'\in\mathbb Z when, for every x\in V_n, \sum_{a\in V_n}\lambda_aD_af(x)\in\{\rho,\rho'\}. The levels may coincide. The sequence is nontrivial when at least one level is nonzero.

Lean code for Definition4.5.6●2 definitions

defdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

def CryptBoolean.IsPartialCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ ρ' : ℤ) : Prop

def CryptBoolean.IsPartialCoveringSequence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ ρ' : ℤ) :
  Prop

A partial covering sequence has a weighted derivative sum taking at most two levels.

defdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

def CryptBoolean.partialCoveringExceptionalSet {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ ρ' : ℤ) : Finset (FABL.F₂Cube n)

def CryptBoolean.partialCoveringExceptionalSet
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ ρ' : ℤ) :
  Finset (FABL.F₂Cube n)

The exceptional level set in Carlet's partial-covering identity.

Theorem4.5.7

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Definition 1.10.1

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-5partial-covering-sequencederivative-spacepage-74fidelity-exact

Derivative-space partial covering sequence (Carlet, example after Definition 6, p. 74). Let D be a nonzero finite \mathbb F_2-vector space of Boolean functions, every element of which is a derivative D_af. Then \sum_{g\in D}g(x)\in\{0,|D|/2\} for every x. If E is a set of directions chosen minimally so that a\mapsto D_af is a bijection from E to D, then the indicator of E is a nontrivial partial covering sequence of f with levels 0 and |D|/2.

Lean code for Theorem4.5.7●10 declarations

defdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

def CryptBoolean.IsDerivativeSpace {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n)) : Prop

def CryptBoolean.IsDerivativeSpace {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n)) :
  Prop

A nonzero binary subspace of Boolean functions whose elements are derivatives of `f`.

theoremdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

theorem CryptBoolean.sum_bitValueInt_submodule_eq_zero_or_half {n : ℕ}
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (x : FABL.F₂Cube n) :
  ∑ g, CryptBoolean.bitValueInt (↑g x) = 0 ∨
    ∑ g, CryptBoolean.bitValueInt (↑g x) = ↑(Nat.card ↥D / 2)

theorem CryptBoolean.sum_bitValueInt_submodule_eq_zero_or_half
  {n : ℕ}
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (x : FABL.F₂Cube n) :
  ∑ g, CryptBoolean.bitValueInt (↑g x) =
      0 ∨
    ∑ g, CryptBoolean.bitValueInt (↑g x) =
      ↑(Nat.card ↥D / 2)

At a fixed point, the integer sum over a binary function subspace is either zero or
half the cardinality of the subspace.

defdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

def CryptBoolean.derivativeDirectionRepresentative {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) (g : ↥D) : FABL.F₂Cube n

def CryptBoolean.derivativeDirectionRepresentative
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D)
  (g : ↥D) : FABL.F₂Cube n

A chosen direction representing a prescribed derivative in a derivative space.

theoremdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

theorem CryptBoolean.booleanDerivative_derivativeDirectionRepresentative {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) (g : ↥D) :
  FABL.booleanDerivative f
      (CryptBoolean.derivativeDirectionRepresentative f D hD g) =
    ↑g

theorem CryptBoolean.booleanDerivative_derivativeDirectionRepresentative
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D)
  (g : ↥D) :
  FABL.booleanDerivative f
      (CryptBoolean.derivativeDirectionRepresentative
        f D hD g) =
    ↑g

theoremdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

theorem CryptBoolean.derivativeDirectionRepresentative_injective {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) :
  Function.Injective
    (CryptBoolean.derivativeDirectionRepresentative f D hD)

theorem CryptBoolean.derivativeDirectionRepresentative_injective
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D) :
  Function.Injective
    (CryptBoolean.derivativeDirectionRepresentative
      f D hD)

Distinct derivatives receive distinct representative directions.

defdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

def CryptBoolean.derivativeRepresentativeDirections {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) : Finset (FABL.F₂Cube n)

def CryptBoolean.derivativeRepresentativeDirections
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D) :
  Finset (FABL.F₂Cube n)

One chosen direction for every derivative in `D`.

theoremdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

theorem CryptBoolean.card_derivativeRepresentativeDirections {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) :
  (CryptBoolean.derivativeRepresentativeDirections f D hD).card =
    Nat.card ↥D

theorem CryptBoolean.card_derivativeRepresentativeDirections
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D) :
  (CryptBoolean.derivativeRepresentativeDirections
        f D hD).card =
    Nat.card ↥D

The representative direction set has exactly one element for every member of `D`.

theoremdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

theorem CryptBoolean.bijOn_booleanDerivative_derivativeRepresentativeDirections
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) :
  Set.BijOn (FABL.booleanDerivative f)
    ↑(CryptBoolean.derivativeRepresentativeDirections f D hD) ↑D

theorem CryptBoolean.bijOn_booleanDerivative_derivativeRepresentativeDirections
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D) :
  Set.BijOn (FABL.booleanDerivative f)
    ↑(CryptBoolean.derivativeRepresentativeDirections
        f D hD)
    ↑D

The derivative map restricts to a bijection from the chosen directions onto `D`.

theoremdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

theorem CryptBoolean.sum_derivativeRepresentativeDirections {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) (x : FABL.F₂Cube n) :
  ∑ a ∈ CryptBoolean.derivativeRepresentativeDirections f D hD,
      CryptBoolean.bitValueInt (FABL.booleanDerivative f a x) =
    ∑ g, CryptBoolean.bitValueInt (↑g x)

theorem CryptBoolean.sum_derivativeRepresentativeDirections
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D)
  (x : FABL.F₂Cube n) :
  ∑
      a ∈
        CryptBoolean.derivativeRepresentativeDirections
          f D hD,
      CryptBoolean.bitValueInt
        (FABL.booleanDerivative f a x) =
    ∑ g, CryptBoolean.bitValueInt (↑g x)

Summing over the chosen directions is the same as summing over the derivative space.

theoremdefined in CryptBoolean/Carlet/Chapter05/DerivativeSpacePartialCovering.lean

complete

theorem CryptBoolean.isPartialCoveringSequence_derivativeRepresentativeDirections
  {n : ℕ} (f : CryptBoolean.BooleanFunction n)
  (D : Submodule FABL.𝔽₂ (CryptBoolean.BooleanFunction n))
  (hD : CryptBoolean.IsDerivativeSpace f D) :
  CryptBoolean.IsPartialCoveringSequence f
      (CryptBoolean.directionFamilyIndicator
        (CryptBoolean.derivativeRepresentativeDirections f D hD))
      0 ↑(Nat.card ↥D / 2) ∧
    ↑(Nat.card ↥D / 2) ≠ 0

theorem CryptBoolean.isPartialCoveringSequence_derivativeRepresentativeDirections
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (D :
    Submodule FABL.𝔽₂
      (CryptBoolean.BooleanFunction n))
  (hD :
    CryptBoolean.IsDerivativeSpace f D) :
  CryptBoolean.IsPartialCoveringSequence f
      (CryptBoolean.directionFamilyIndicator
        (CryptBoolean.derivativeRepresentativeDirections
          f D hD))
      0 ↑(Nat.card ↥D / 2) ∧
    ↑(Nat.card ↥D / 2) ≠ 0

The chosen representative directions give Carlet's nontrivial partial covering sequence
with levels zero and half the derivative-space cardinality.

Choosing one direction for each element of the finite binary derivative space gives a bijection onto D and hence a minimal representative set. Since D is nonzero, the second level is nonzero.

Theorem4.5.8

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Definition 1.7.1

Loading preview

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

used by 1✓L∃∀N

Tagscarletchapter-5partial-covering-sequencetheorem-6relation-43reference-68pages-75-76fidelity-exact

Partial-covering Walsh identity (Carlet, Theorem 6 and Relation (43), pp. 75--76). Let \lambda be a partial covering sequence of f with levels \rho,\rho'. If \rho'\ne\rho, set A=\left\{x\in V_n:\sum_a\lambda_aD_af(x)=\rho'\right\}; if \rho'=\rho, set A=\varnothing. Then, for every b\in V_n, \bigl(\widehat\lambda(b)-\widehat\lambda(0)+2\rho\bigr)W_f(b) =2(\rho-\rho')\sum_{x\in A}(-1)^{f(x)+b\mathbin\cdot x}.

Lean code for Theorem4.5.8●1 theorem

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.theorem_6_partialCoveringSequence {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ ρ' : ℤ)
  (hpartial : CryptBoolean.IsPartialCoveringSequence f coeff ρ ρ')
  (b : FABL.F₂Cube n) :
  (CryptBoolean.integerWalshTransform coeff b -
          CryptBoolean.integerWalshTransform coeff 0 +
        2 * ρ) *
      CryptBoolean.walshTransform f b =
    2 * (ρ - ρ') *
      ∑ x ∈ CryptBoolean.partialCoveringExceptionalSet f coeff ρ ρ',
        CryptBoolean.walshTerm f b x

theorem CryptBoolean.theorem_6_partialCoveringSequence
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ ρ' : ℤ)
  (hpartial :
    CryptBoolean.IsPartialCoveringSequence
      f coeff ρ ρ')
  (b : FABL.F₂Cube n) :
  (CryptBoolean.integerWalshTransform
            coeff b -
          CryptBoolean.integerWalshTransform
            coeff 0 +
        2 * ρ) *
      CryptBoolean.walshTransform f b =
    2 * (ρ - ρ') *
      ∑
        x ∈
          CryptBoolean.partialCoveringExceptionalSet
            f coeff ρ ρ',
        CryptBoolean.walshTerm f b x

Carlet Theorem 6: the raw spectral identity supplied by a partial covering sequence.

Corollary4.5.9

Group: Chapter 4: Classes with Provable Spectra and Weights (30)

Group member previews

Preview

Theorem 4.1.1

Loading preview

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

Statement uses 2

Statement dependency previews

Preview

Theorem 1.7.3

Loading preview

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

used by 0✓L∃∀N

Tagscarletchapter-5partial-covering-sequencetheorem-6weightreference-68page-76fidelity-strengthened-division-free

Partial-covering weight identity (Carlet, consequence of Theorem 6, p. 76). Under the hypotheses and notation of Theorem 6, if \rho\ne0, then 2^n-2w_H(f)=W_f(0) =\left(1-\frac{\rho'}{\rho}\right) \sum_{x\in A}(-1)^{f(x)}.

Lean code for Corollary4.5.9●1 theorem

theoremdefined in CryptBoolean/Carlet/Chapter05/CoveringSequences.lean

complete

theorem CryptBoolean.theorem_6_weight_identity {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (coeff : FABL.F₂Cube n → ℤ)
  (ρ ρ' : ℤ)
  (hpartial : CryptBoolean.IsPartialCoveringSequence f coeff ρ ρ') :
  ρ * CryptBoolean.walshTransform f 0 =
    (ρ - ρ') *
      ∑ x ∈ CryptBoolean.partialCoveringExceptionalSet f coeff ρ ρ',
        CryptBoolean.bitSignInt (f x)

theorem CryptBoolean.theorem_6_weight_identity
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (coeff : FABL.F₂Cube n → ℤ) (ρ ρ' : ℤ)
  (hpartial :
    CryptBoolean.IsPartialCoveringSequence
      f coeff ρ ρ') :
  ρ * CryptBoolean.walshTransform f 0 =
    (ρ - ρ') *
      ∑
        x ∈
          CryptBoolean.partialCoveringExceptionalSet
            f coeff ρ ρ',
        CryptBoolean.bitSignInt (f x)

Division-free form of the weight consequence of Carlet Theorem 6.

Multiplying by \rho gives the equivalent identity \rho W_f(0)=(\rho-\rho')\sum_{x\in A}(-1)^{f(x)} without assuming \rho\ne0.