Cryptographic Boolean Functions in Lean

3.4. Balancedness and resiliency🔗

Definition3.4.1
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 6
Reverse dependency previews
Preview
Theorem 3.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-4definition-3resiliencycorrelation-immunitypages-55-56fidelity-exact

Definition 3 (Carlet, pp. 55--56). Let n>0 and 0\le m<n. A function f:V_n\to\mathbb F_2 is m-resilient if every restriction obtained by fixing at most m input coordinates is balanced. It is correlation immune of order m if fixing any such inputs leaves the output distribution unchanged. Fixing exactly m coordinates is equivalent in both definitions.

Lean code for Definition3.4.1●10 declarations
  • defdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    def CryptBoolean.signCubeView {n : ℕ} (f : CryptBoolean.BooleanFunction n) :
  FABL.BooleanFunction n
    def CryptBoolean.signCubeView {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  FABL.BooleanFunction n
    The sign-cube view of a bit-valued Boolean function.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.signCubeView_toReal {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (CryptBoolean.signCubeView f).toReal =
    FABL.binaryFunctionOnSignCube (CryptBoolean.realSignView f)
    theorem CryptBoolean.signCubeView_toReal {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  (CryptBoolean.signCubeView f).toReal =
    FABL.binaryFunctionOnSignCube
      (CryptBoolean.realSignView f)
    The real view of `signCubeView` is the canonical binary sign encoding transported
across FABL's cube equivalence.
  • defdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    def CryptBoolean.IsCorrelationImmune {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.IsCorrelationImmune {n : ℕ}
  (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    A bit-valued Boolean function is correlation immune of order `m` when fixing at most
`m` input coordinates leaves its output distribution unchanged.
  • defdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    def CryptBoolean.IsResilient {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) : Prop
    def CryptBoolean.IsResilient {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  Prop
    A bit-valued Boolean function is resilient of order `m` when it is correlation immune
of order `m` and balanced.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.isCorrelationImmune_iff_fabl {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    FABL.IsCorrelationImmune m (CryptBoolean.signCubeView f)
    theorem CryptBoolean.isCorrelationImmune_iff_fabl
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    FABL.IsCorrelationImmune m
      (CryptBoolean.signCubeView f)
    The coordinate-restriction definition of correlation immunity is exactly FABL's
zero low-degree Fourier regularity predicate after decoding to the sign cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.isBalanced_iff_fabl {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBalanced f ↔
    FABL.IsBalanced (CryptBoolean.signCubeView f).toReal
    theorem CryptBoolean.isBalanced_iff_fabl {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsBalanced f ↔
    FABL.IsBalanced
      (CryptBoolean.signCubeView f).toReal
    Carlet balancedness agrees with FABL balancedness after decoding to the sign cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.isResilient_iff_fabl {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsResilient m f ↔
    FABL.IsResilient m (CryptBoolean.signCubeView f)
    theorem CryptBoolean.isResilient_iff_fabl {n : ℕ}
  (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) :
  CryptBoolean.IsResilient m f ↔
    FABL.IsResilient m
      (CryptBoolean.signCubeView f)
    Carlet resiliency agrees with FABL resiliency after decoding to the sign cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.isResilient_iff_forall_coordinateRestriction_balanced
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n) (_hn : 0 < n)
  (_hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    ∀ (J : Finset (Fin n)) (z : FABL.FixedSignCube J),
      Fintype.card (FABL.FixedIndex J) ≤ m →
        FABL.IsBalanced
          (FABL.signRestriction (CryptBoolean.signCubeView f).toReal J
            z)
    theorem CryptBoolean.isResilient_iff_forall_coordinateRestriction_balanced
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (_hn : 0 < n) (_hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    ∀ (J : Finset (Fin n))
      (z : FABL.FixedSignCube J),
      Fintype.card (FABL.FixedIndex J) ≤
          m →
        FABL.IsBalanced
          (FABL.signRestriction
            (CryptBoolean.signCubeView
                f).toReal
            J z)
    Carlet Definition 3: when `n > 0` and `m < n`, resiliency is equivalent to
balancedness of every restriction obtained by fixing at most `m` coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.isCorrelationImmune_iff_fixing_exactly {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) (_hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    ∀ (J : Finset (Fin n)) (z : FABL.FixedSignCube J),
      Fintype.card (FABL.FixedIndex J) = m →
        FABL.mean
            (FABL.signRestriction (CryptBoolean.signCubeView f).toReal J
              z) =
          FABL.mean (CryptBoolean.signCubeView f).toReal
    theorem CryptBoolean.isCorrelationImmune_iff_fixing_exactly
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (_hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    ∀ (J : Finset (Fin n))
      (z : FABL.FixedSignCube J),
      Fintype.card (FABL.FixedIndex J) =
          m →
        FABL.mean
            (FABL.signRestriction
              (CryptBoolean.signCubeView
                  f).toReal
              J z) =
          FABL.mean
            (CryptBoolean.signCubeView
                f).toReal
    Carlet Definition 3, footnote 24: for `n > 0` and `m < n`, requiring
unchanged output distribution after fixing exactly `m` coordinates is equivalent
to correlation immunity under all restrictions fixing at most `m` coordinates.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.isResilient_iff_fixing_exactly {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    ∀ (J : Finset (Fin n)) (z : FABL.FixedSignCube J),
      Fintype.card (FABL.FixedIndex J) = m →
        FABL.IsBalanced
          (FABL.signRestriction (CryptBoolean.signCubeView f).toReal J
            z)
    theorem CryptBoolean.isResilient_iff_fixing_exactly
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    ∀ (J : Finset (Fin n))
      (z : FABL.FixedSignCube J),
      Fintype.card (FABL.FixedIndex J) =
          m →
        FABL.IsBalanced
          (FABL.signRestriction
            (CryptBoolean.signCubeView
                f).toReal
            J z)
    Carlet Definition 3, footnote 25: for `n > 0` and `m < n`, requiring
balancedness after fixing exactly `m` coordinates is equivalent to resiliency
under all restrictions fixing at most `m` coordinates.
Theorem3.4.2
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Definition 1.7.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 21
Reverse dependency previews
Preview
Corollary 3.4.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-4theorem-3resiliencypage-57fidelity-exact

Theorem 3 (Carlet, p. 57). A Boolean function f is m-resilient if and only if W_f(u)=0\qquad\text{for every }u\in V_n\text{ with }w_H(u)\le m. It is correlation immune of order m if and only if the same vanishing holds for every u with 0<w_H(u)\le m.

Lean code for Theorem3.4.2●3 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.walshTransform_eq_zero_iff_vectorFourierCoeff_eq_zero
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f u = 0 ↔
    FABL.vectorFourierCoeff (CryptBoolean.realSignView f) u = 0
    theorem CryptBoolean.walshTransform_eq_zero_iff_vectorFourierCoeff_eq_zero
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) :
  CryptBoolean.walshTransform f u = 0 ↔
    FABL.vectorFourierCoeff
        (CryptBoolean.realSignView f) u =
      0
    A raw Walsh coefficient vanishes exactly when the corresponding normalized FABL
vector-Fourier coefficient vanishes.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.theorem_3_correlationImmune_iff_walshTransform_eq_zero
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n) (_hn : 0 < n)
  (_hm : m < n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    ∀ (u : FABL.F₂Cube n),
      u ≠ 0 →
        (FABL.f₂Support u).card ≤ m →
          CryptBoolean.walshTransform f u = 0
    theorem CryptBoolean.theorem_3_correlationImmune_iff_walshTransform_eq_zero
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (_hn : 0 < n) (_hm : m < n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    ∀ (u : FABL.F₂Cube n),
      u ≠ 0 →
        (FABL.f₂Support u).card ≤ m →
          CryptBoolean.walshTransform f
              u =
            0
    Carlet Theorem 3, correlation-immunity form: for `n > 0` and `m < n`,
correlation immunity of order `m` is equivalent to vanishing of every nonzero
raw Walsh coefficient whose frequency has Hamming weight at most `m`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.theorem_3_resilient_iff_walshTransform_eq_zero {n : ℕ}
  (m : ℕ) (f : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    ∀ (u : FABL.F₂Cube n),
      (FABL.f₂Support u).card ≤ m → CryptBoolean.walshTransform f u = 0
    theorem CryptBoolean.theorem_3_resilient_iff_walshTransform_eq_zero
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    ∀ (u : FABL.F₂Cube n),
      (FABL.f₂Support u).card ≤ m →
        CryptBoolean.walshTransform f u =
          0
    Carlet Theorem 3, resilient form: for `n > 0` and `m < n`, resiliency of
order `m` is equivalent to vanishing of every raw Walsh coefficient whose
frequency has Hamming weight at most `m`, including the zero frequency.
Corollary3.4.3
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Proposition 5.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-4resiliencydual-distancepage-57fidelity-exact

Support dual-distance characterization (Carlet, p. 57). The function f is m-resilient if and only if |\operatorname{supp}(f)|=2^{n-1} and \operatorname{supp}(f) has dual distance at least m+1. It is correlation immune of order m if and only if the dual-distance condition alone holds.

Lean code for Corollary3.4.3●7 declarations
  • defdefined in CryptBoolean/Carlet/Chapter04/SupportDualDistance.lean
    complete
    def CryptBoolean.codeCharacterSum {n : ℕ} (C : Finset (FABL.F₂Cube n))
  (u : FABL.F₂Cube n) : ℝ
    def CryptBoolean.codeCharacterSum {n : ℕ}
  (C : Finset (FABL.F₂Cube n))
  (u : FABL.F₂Cube n) : ℝ
    The character sum of a binary code at a frequency.
  • defdefined in CryptBoolean/Carlet/Chapter04/SupportDualDistance.lean
    complete
    def CryptBoolean.HasDualDistanceAtLeast {n : ℕ} (C : Finset (FABL.F₂Cube n))
  (d : ℕ) : Prop
    def CryptBoolean.HasDualDistanceAtLeast
  {n : ℕ} (C : Finset (FABL.F₂Cube n))
  (d : ℕ) : Prop
    An arbitrary binary code has dual distance at least `d` when every nonzero
character of weight below `d` has zero sum over the code.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/SupportDualDistance.lean
    complete
    theorem CryptBoolean.sum_vectorWalshCharacter_eq_zero {n : ℕ}
  (u : FABL.F₂Cube n) (hu : u ≠ 0) :
  ∑ x, (FABL.vectorWalshCharacter u) x = 0
    theorem CryptBoolean.sum_vectorWalshCharacter_eq_zero
  {n : ℕ} (u : FABL.F₂Cube n)
  (hu : u ≠ 0) :
  ∑ x, (FABL.vectorWalshCharacter u) x = 0
    A nontrivial Walsh character sums to zero over the full binary cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/SupportDualDistance.lean
    complete
    theorem CryptBoolean.walshTransform_cast_eq_neg_two_mul_codeCharacterSum_support
  {n : ℕ} (f : CryptBoolean.BooleanFunction n) (u : FABL.F₂Cube n)
  (hu : u ≠ 0) :
  ↑(CryptBoolean.walshTransform f u) =
    -2 * CryptBoolean.codeCharacterSum (CryptBoolean.support f) u
    theorem CryptBoolean.walshTransform_cast_eq_neg_two_mul_codeCharacterSum_support
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (u : FABL.F₂Cube n) (hu : u ≠ 0) :
  ↑(CryptBoolean.walshTransform f u) =
    -2 *
      CryptBoolean.codeCharacterSum
        (CryptBoolean.support f) u
    At a nonzero frequency, the raw Walsh transform is minus twice the
character sum over the support.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/SupportDualDistance.lean
    complete
    theorem CryptBoolean.isCorrelationImmune_iff_support_hasDualDistanceAtLeast
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hm : m < n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    CryptBoolean.HasDualDistanceAtLeast (CryptBoolean.support f) (m + 1)
    theorem CryptBoolean.isCorrelationImmune_iff_support_hasDualDistanceAtLeast
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsCorrelationImmune m f ↔
    CryptBoolean.HasDualDistanceAtLeast
      (CryptBoolean.support f) (m + 1)
    Carlet's support-dual-distance corollary, correlation-immunity form.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/SupportDualDistance.lean
    complete
    theorem CryptBoolean.isBalanced_iff_support_card_eq_two_pow_pred {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (hn : 0 < n) :
  CryptBoolean.IsBalanced f ↔
    (CryptBoolean.support f).card = 2 ^ (n - 1)
    theorem CryptBoolean.isBalanced_iff_support_card_eq_two_pow_pred
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) :
  CryptBoolean.IsBalanced f ↔
    (CryptBoolean.support f).card =
      2 ^ (n - 1)
    For a nonempty binary cube, balancedness says exactly that the support has
cardinality `2^(n-1)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/SupportDualDistance.lean
    complete
    theorem CryptBoolean.isResilient_iff_support_card_and_hasDualDistanceAtLeast
  {n : ℕ} (m : ℕ) (f : CryptBoolean.BooleanFunction n) (hn : 0 < n)
  (hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    (CryptBoolean.support f).card = 2 ^ (n - 1) ∧
      CryptBoolean.HasDualDistanceAtLeast (CryptBoolean.support f)
        (m + 1)
    theorem CryptBoolean.isResilient_iff_support_card_and_hasDualDistanceAtLeast
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (hn : 0 < n) (hm : m < n) :
  CryptBoolean.IsResilient m f ↔
    (CryptBoolean.support f).card =
        2 ^ (n - 1) ∧
      CryptBoolean.HasDualDistanceAtLeast
        (CryptBoolean.support f) (m + 1)
    Carlet's support-dual-distance corollary, resilient form: the support has
size `2^(n-1)` and dual distance at least `m+1`.

Here dual distance is understood through Carlet's character-sum definition for an arbitrary finite binary code.

Theorem3.4.4
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
Tagscarletchapter-4resilient-constructionpages-57-58fidelity-exact-generator-matrix

Code-generator construction (Carlet, pp. 57--58). Let G generate a binary [n,k,d] linear code, and let g:V_k\to\mathbb F_2 be balanced. Then f(x)=g(xG^{\mathsf T}) is (d-1)-resilient.

Lean code for Theorem3.4.4●5 declarations
  • defdefined in CryptBoolean/Carlet/Chapter04/CodeGeneratorResiliency.lean
    complete
    def CryptBoolean.binaryGeneratorCodeword {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂) (u : FABL.F₂Cube k) :
  FABL.F₂Cube n
    def CryptBoolean.binaryGeneratorCodeword
  {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂)
  (u : FABL.F₂Cube k) : FABL.F₂Cube n
    The codeword obtained from the coefficient row vector `u` and the
generator matrix `G`.
  • defdefined in CryptBoolean/Carlet/Chapter04/CodeGeneratorResiliency.lean
    complete
    def CryptBoolean.IsBinaryCodeGenerator {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂) (d : ℕ) : Prop
    def CryptBoolean.IsBinaryCodeGenerator
  {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂)
  (d : ℕ) : Prop
    A binary `[n,k,d]` generator matrix: its rows are independent and
the least weight of a nonzero generated codeword is exactly `d`.
  • defdefined in CryptBoolean/Carlet/Chapter04/CodeGeneratorResiliency.lean
    complete
    def CryptBoolean.binaryGeneratorPullback {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂)
  (g : CryptBoolean.BooleanFunction k) : CryptBoolean.BooleanFunction n
    def CryptBoolean.binaryGeneratorPullback
  {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂)
  (g : CryptBoolean.BooleanFunction k) :
  CryptBoolean.BooleanFunction n
    Carlet's function `f(x)=g(xGᵀ)`, using Mathlib's column action for
the displayed multiplication by `Gᵀ`.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/CodeGeneratorResiliency.lean
    complete
    theorem CryptBoolean.isBalanced_binaryGeneratorPullback {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂)
  (g : CryptBoolean.BooleanFunction k)
  (hrows : LinearIndependent FABL.𝔽₂ G.row)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.IsBalanced (CryptBoolean.binaryGeneratorPullback G g)
    theorem CryptBoolean.isBalanced_binaryGeneratorPullback
  {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂)
  (g : CryptBoolean.BooleanFunction k)
  (hrows :
    LinearIndependent FABL.𝔽₂ G.row)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.IsBalanced
    (CryptBoolean.binaryGeneratorPullback
      G g)
    Pulling a balanced Boolean function back through a full-row-rank binary
generator matrix preserves balancedness.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/CodeGeneratorResiliency.lean
    complete
    theorem CryptBoolean.binaryGeneratorPullback_isResilient {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂) (d : ℕ)
  (hG : CryptBoolean.IsBinaryCodeGenerator G d)
  (g : CryptBoolean.BooleanFunction k)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.IsResilient (d - 1)
    (CryptBoolean.binaryGeneratorPullback G g)
    theorem CryptBoolean.binaryGeneratorPullback_isResilient
  {n k : ℕ}
  (G : Matrix (Fin k) (Fin n) FABL.𝔽₂)
  (d : ℕ)
  (hG :
    CryptBoolean.IsBinaryCodeGenerator G
      d)
  (g : CryptBoolean.BooleanFunction k)
  (hg : CryptBoolean.IsBalanced g) :
  CryptBoolean.IsResilient (d - 1)
    (CryptBoolean.binaryGeneratorPullback
      G g)
    Carlet's code-generator construction: if `G` generates a binary
`[n,k,d]` linear code and `g` is balanced, then
`x ↦ g(xGᵀ)` is `(d-1)`-resilient.
Theorem3.4.5
Group: Chapter 3: Boolean functions and cryptography (72)
Group member previews
Preview
Theorem 3.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Proposition 1.8.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-4resiliencytranslationpage-58fidelity-exact

Translation invariance of resiliency (Carlet, p. 58). If f is m-resilient, then for every b\in V_n the function x\longmapsto f(x+b) is m-resilient.

Lean code for Theorem3.4.5●2 theorems
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.walshTransform_domainTranslate_cast {n : ℕ}
  (f : CryptBoolean.BooleanFunction n) (b u : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform (FABL.domainTranslate f b) u) =
    (FABL.vectorWalshCharacter u) b * ↑(CryptBoolean.walshTransform f u)
    theorem CryptBoolean.walshTransform_domainTranslate_cast
  {n : ℕ}
  (f : CryptBoolean.BooleanFunction n)
  (b u : FABL.F₂Cube n) :
  ↑(CryptBoolean.walshTransform
        (FABL.domainTranslate f b) u) =
    (FABL.vectorWalshCharacter u) b *
      ↑(CryptBoolean.walshTransform f u)
    Translating the input multiplies a raw Walsh coefficient by the corresponding
Walsh character value.
  • theoremdefined in CryptBoolean/Carlet/Chapter04/Resiliency.lean
    complete
    theorem CryptBoolean.isResilient_domainTranslate {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n) (b : FABL.F₂Cube n) (hn : 0 < n)
  (hm : m < n) (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.IsResilient m (FABL.domainTranslate f b)
    theorem CryptBoolean.isResilient_domainTranslate
  {n : ℕ} (m : ℕ)
  (f : CryptBoolean.BooleanFunction n)
  (b : FABL.F₂Cube n) (hn : 0 < n)
  (hm : m < n)
  (hf : CryptBoolean.IsResilient m f) :
  CryptBoolean.IsResilient m
    (FABL.domainTranslate f b)
    Carlet's translation invariance of resiliency: an additive input translation
preserves every resilient order in the source range `n > 0`, `m < n`.