Cryptographic Boolean Functions in Lean

5.15. Kerdock codes🔗

Theorem5.15.1
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.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 6
Reverse dependency previews
Preview
Theorem 5.15.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagscarletchapter-6relation-56pages-109-110fidelity-exact

Relation (56) (Carlet, pp. 109--110). Define the complete quadratic function on V_n by q_n(x)=\sum_{1\le i<j\le n}x_ix_j. For every x\in V_n, its value is the parity of \binom{w_H(x)}2. If n is even, the polar form of q_n has trivial radical and q_n is bent.

Lean code for Theorem5.15.1●13 declarations
  • defdefined in FABL/Chapter05/ThresholdCircuits.lean
    complete
    def FABL.completeQuadraticBit {n : ℕ} (x : FABL.F₂Cube n) : FABL.𝔽₂
    def FABL.completeQuadraticBit {n : ℕ}
  (x : FABL.F₂Cube n) : FABL.𝔽₂
    The quadratic form underlying the complete quadratic function.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_completeQuadraticBit_le_two
  {n : ℕ} : FABL.functionAlgebraicDegree FABL.completeQuadraticBit ≤ 2
    theorem CryptBoolean.functionAlgebraicDegree_completeQuadraticBit_le_two
  {n : ℕ} :
  FABL.functionAlgebraicDegree
      FABL.completeQuadraticBit ≤
    2
    The complete quadratic function has algebraic degree at most two.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.completeQuadraticBit_eq_choose_support_card {n : ℕ}
  (x : FABL.F₂Cube n) :
  FABL.completeQuadraticBit x = ↑((FABL.f₂Support x).card.choose 2)
    theorem CryptBoolean.completeQuadraticBit_eq_choose_support_card
  {n : ℕ} (x : FABL.F₂Cube n) :
  FABL.completeQuadraticBit x =
    ↑((FABL.f₂Support x).card.choose 2)
    Relation (56): the complete quadratic value is the parity of the number
of unordered pairs in the support, namely `choose(weight, 2)` modulo two.
  • defdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    def CryptBoolean.completeQuadraticPolarFrequency {n : ℕ}
  (a : FABL.F₂Cube n) : FABL.F₂Cube n
    def CryptBoolean.completeQuadraticPolarFrequency
  {n : ℕ} (a : FABL.F₂Cube n) :
  FABL.F₂Cube n
    The coefficient vector representing the polar form of the complete
quadratic function in its second argument.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.quadraticPolarKernel_completeQuadraticBit_eq_crossSum
  {n : ℕ} (a b : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel FABL.completeQuadraticBit a b =
    ∑ i, ∑ j ∈ Finset.Ioi i, (a i * b j + b i * a j)
    theorem CryptBoolean.quadraticPolarKernel_completeQuadraticBit_eq_crossSum
  {n : ℕ} (a b : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel
      FABL.completeQuadraticBit a b =
    ∑ i,
      ∑ j ∈ Finset.Ioi i,
        (a i * b j + b i * a j)
    The polar kernel of the complete quadratic function is the sum of its
mixed quadratic terms.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.quadraticPolarKernel_completeQuadraticBit_eq_dotProduct
  {n : ℕ} (a b : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel FABL.completeQuadraticBit a b =
    FABL.f₂DotProduct (CryptBoolean.completeQuadraticPolarFrequency a) b
    theorem CryptBoolean.quadraticPolarKernel_completeQuadraticBit_eq_dotProduct
  {n : ℕ} (a b : FABL.F₂Cube n) :
  CryptBoolean.quadraticPolarKernel
      FABL.completeQuadraticBit a b =
    FABL.f₂DotProduct
      (CryptBoolean.completeQuadraticPolarFrequency
        a)
      b
    The polar form of the complete quadratic function is represented by the
sum of all coordinates other than the indexed coordinate.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.completeQuadraticPolarFrequency_eq_zero_of_even {n : ℕ}
  (hn : Even n) {a : FABL.F₂Cube n}
  (ha : CryptBoolean.completeQuadraticPolarFrequency a = 0) : a = 0
    theorem CryptBoolean.completeQuadraticPolarFrequency_eq_zero_of_even
  {n : ℕ} (hn : Even n)
  {a : FABL.F₂Cube n}
  (ha :
    CryptBoolean.completeQuadraticPolarFrequency
        a =
      0) :
  a = 0
    In even dimension the polar-frequency map of the complete quadratic
function has trivial kernel.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.quadraticRadical_completeQuadraticBit_eq_bot {n : ℕ}
  (hn : Even n) :
  CryptBoolean.quadraticRadical FABL.completeQuadraticBit ⋯ = ⊥
    theorem CryptBoolean.quadraticRadical_completeQuadraticBit_eq_bot
  {n : ℕ} (hn : Even n) :
  CryptBoolean.quadraticRadical
      FABL.completeQuadraticBit ⋯ =
    ⊥
    In even dimension the polar radical of the complete quadratic function is
trivial.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.isBent_completeQuadraticBit {n : ℕ} (hn : Even n) :
  CryptBoolean.IsBent FABL.completeQuadraticBit
    theorem CryptBoolean.isBent_completeQuadraticBit
  {n : ℕ} (hn : Even n) :
  CryptBoolean.IsBent
    FABL.completeQuadraticBit
    FABL's complete quadratic Boolean function is bent in every even
dimension, including the zero-dimensional boundary.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.completeQuadraticBit_zero_dimension (x : FABL.F₂Cube 0) :
  FABL.completeQuadraticBit x = 0
    theorem CryptBoolean.completeQuadraticBit_zero_dimension
  (x : FABL.F₂Cube 0) :
  FABL.completeQuadraticBit x = 0
    In dimension zero Relation (56) is the empty sum.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.isBent_completeQuadraticBit_zero_dimension :
  CryptBoolean.IsBent FABL.completeQuadraticBit
    theorem CryptBoolean.isBent_completeQuadraticBit_zero_dimension :
  CryptBoolean.IsBent
    FABL.completeQuadraticBit
    The zero-dimensional complete quadratic function is bent under the
zero-dimensional convention for bent functions.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.completeQuadraticBit_two_dimension (x : FABL.F₂Cube 2) :
  FABL.completeQuadraticBit x = x 0 * x 1
    theorem CryptBoolean.completeQuadraticBit_two_dimension
  (x : FABL.F₂Cube 2) :
  FABL.completeQuadraticBit x = x 0 * x 1
    In dimension two Relation (56) consists of its single quadratic
monomial.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/CompleteQuadratic.lean
    complete
    theorem CryptBoolean.isBent_completeQuadraticBit_two_dimension :
  CryptBoolean.IsBent FABL.completeQuadraticBit
    theorem CryptBoolean.isBent_completeQuadraticBit_two_dimension :
  CryptBoolean.IsBent
    FABL.completeQuadraticBit
    The first positive-dimensional instance of Relation (56) is bent.
Theorem5.15.2
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6kerdockpages-109-110fidelity-exact-conditional-reduction

Kerdock parameters (Carlet, pp. 109--110). Let n\ge2 be even and let F be a family of 2^{n-1} Boolean functions on V_n containing zero. Suppose that every nonzero member of F has algebraic degree two and that f+g is bent whenever f,g\in F are distinct. Then K(F)=\bigcup_{f\in F}\bigl(f+R(1,n)\bigr) contains R(1,n), is contained in R(2,n), has 2^{2n} words, and has minimum distance 2^{n-1}-2^{n/2-1}. The first-order Reed--Muller cosets in this union are pairwise distinct.

Lean code for Theorem5.15.2●12 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    def CryptBoolean.IsKerdockRepresentativeFamily {n : ℕ}
  (F : Finset (CryptBoolean.BooleanFunction n)) : Prop
    def CryptBoolean.IsKerdockRepresentativeFamily
  {n : ℕ}
  (F :
    Finset
      (CryptBoolean.BooleanFunction n)) :
  Prop
    The source conditions on a finite family of Kerdock coset representatives:
zero is represented, every nonzero representative is quadratic, distinct
representatives have bent sum, and the family has `2^(n-1)` members.
  • defdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    def CryptBoolean.kerdockCodeOfRepresentatives {n : ℕ}
  (F : Finset (CryptBoolean.BooleanFunction n)) :
  Finset (CryptBoolean.BooleanFunction n)
    def CryptBoolean.kerdockCodeOfRepresentatives
  {n : ℕ}
  (F :
    Finset
      (CryptBoolean.BooleanFunction n)) :
  Finset (CryptBoolean.BooleanFunction n)
    The union of first-order Reed--Muller cosets determined by a finite
Kerdock representative family.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_le_two_of_mem_kerdockRepresentatives
  {n : ℕ} {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F)
  {f : CryptBoolean.BooleanFunction n} (hf : f ∈ F) :
  FABL.functionAlgebraicDegree f ≤ 2
    theorem CryptBoolean.functionAlgebraicDegree_le_two_of_mem_kerdockRepresentatives
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  {f : CryptBoolean.BooleanFunction n}
  (hf : f ∈ F) :
  FABL.functionAlgebraicDegree f ≤ 2
    Every representative in a Kerdock family has algebraic degree at most
two, including the zero representative.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.reedMuller_one_subset_kerdockCodeOfRepresentatives {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F)
  ⦃c : CryptBoolean.BooleanFunction n⦄ :
  c ∈ CryptBoolean.reedMuller 1 n →
    c ∈ CryptBoolean.kerdockCodeOfRepresentatives F
    theorem CryptBoolean.reedMuller_one_subset_kerdockCodeOfRepresentatives
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  ⦃c : CryptBoolean.BooleanFunction n⦄ :
  c ∈ CryptBoolean.reedMuller 1 n →
    c ∈
      CryptBoolean.kerdockCodeOfRepresentatives
        F
    The Kerdock coset union contains the first-order Reed--Muller code.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.kerdockCodeOfRepresentatives_subset_reedMuller_two {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F)
  ⦃c : CryptBoolean.BooleanFunction n⦄ :
  c ∈ CryptBoolean.kerdockCodeOfRepresentatives F →
    c ∈ CryptBoolean.reedMuller 2 n
    theorem CryptBoolean.kerdockCodeOfRepresentatives_subset_reedMuller_two
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  ⦃c : CryptBoolean.BooleanFunction n⦄ :
  c ∈
      CryptBoolean.kerdockCodeOfRepresentatives
        F →
    c ∈ CryptBoolean.reedMuller 2 n
    The Kerdock coset union is contained in the second-order Reed--Muller
code.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.nonlinearity_add_eq_kerdockDistance_of_mem {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F) (hn : 2 ≤ n)
  {f g : CryptBoolean.BooleanFunction n} (hf : f ∈ F) (hg : g ∈ F)
  (hfg : f ≠ g) :
  CryptBoolean.nonlinearity (f + g) = 2 ^ (n - 1) - 2 ^ (n / 2 - 1)
    theorem CryptBoolean.nonlinearity_add_eq_kerdockDistance_of_mem
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  (hn : 2 ≤ n)
  {f g : CryptBoolean.BooleanFunction n}
  (hf : f ∈ F) (hg : g ∈ F)
  (hfg : f ≠ g) :
  CryptBoolean.nonlinearity (f + g) =
    2 ^ (n - 1) - 2 ^ (n / 2 - 1)
    Distinct representatives in a Kerdock family have the exact bent
nonlinearity value.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.hasDistinctFirstOrderCosets_of_isKerdockRepresentativeFamily
  {n : ℕ} {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F) (hnEven : Even n)
  (hn : 2 ≤ n) : CryptBoolean.HasDistinctFirstOrderCosets F
    theorem CryptBoolean.hasDistinctFirstOrderCosets_of_isKerdockRepresentativeFamily
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  (hnEven : Even n) (hn : 2 ≤ n) :
  CryptBoolean.HasDistinctFirstOrderCosets
    F
    In dimension at least two, bent pairwise sums force distinct Kerdock
representatives to determine distinct first-order Reed--Muller cosets.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.kerdockRepresentativeFamily_offDiag_nonempty {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F) (hn : 2 ≤ n) :
  F.offDiag.Nonempty
    theorem CryptBoolean.kerdockRepresentativeFamily_offDiag_nonempty
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  (hn : 2 ≤ n) : F.offDiag.Nonempty
    A Kerdock representative family in dimension at least two contains two
distinct representatives.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.card_kerdockCodeOfRepresentatives {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F) (hnEven : Even n)
  (hn : 2 ≤ n) :
  (CryptBoolean.kerdockCodeOfRepresentatives F).card = 2 ^ (2 * n)
    theorem CryptBoolean.card_kerdockCodeOfRepresentatives
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  (hnEven : Even n) (hn : 2 ≤ n) :
  (CryptBoolean.kerdockCodeOfRepresentatives
        F).card =
    2 ^ (2 * n)
    A Kerdock coset union has `2^(2n)` codewords in dimension at least two.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.minimumPairNonlinearity_eq_kerdockDistance {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F) (hn : 2 ≤ n) :
  CryptBoolean.minimumPairNonlinearity F = 2 ^ (n - 1) - 2 ^ (n / 2 - 1)
    theorem CryptBoolean.minimumPairNonlinearity_eq_kerdockDistance
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  (hn : 2 ≤ n) :
  CryptBoolean.minimumPairNonlinearity F =
    2 ^ (n - 1) - 2 ^ (n / 2 - 1)
    The minimum pair nonlinearity of a Kerdock representative family is the
bent nonlinearity value.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.minimumHammingDistance_kerdockCodeOfRepresentatives {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F) (hnEven : Even n)
  (hn : 2 ≤ n) :
  CryptBoolean.minimumHammingDistance
      (CryptBoolean.kerdockCodeOfRepresentatives F) =
    2 ^ (n - 1) - 2 ^ (n / 2 - 1)
    theorem CryptBoolean.minimumHammingDistance_kerdockCodeOfRepresentatives
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  (hnEven : Even n) (hn : 2 ≤ n) :
  CryptBoolean.minimumHammingDistance
      (CryptBoolean.kerdockCodeOfRepresentatives
        F) =
    2 ^ (n - 1) - 2 ^ (n / 2 - 1)
    The minimum distance of a Kerdock coset union is
`2^(n-1) - 2^(n/2-1)`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/Kerdock.lean
    complete
    theorem CryptBoolean.kerdockCodeOfRepresentatives_parameters {n : ℕ}
  {F : Finset (CryptBoolean.BooleanFunction n)}
  (hF : CryptBoolean.IsKerdockRepresentativeFamily F) (hnEven : Even n)
  (hn : 2 ≤ n) :
  F.offDiag.Nonempty ∧
    CryptBoolean.HasDistinctFirstOrderCosets F ∧
      (∀ ⦃c : CryptBoolean.BooleanFunction n⦄,
          c ∈ CryptBoolean.reedMuller 1 n →
            c ∈ CryptBoolean.kerdockCodeOfRepresentatives F) ∧
        (∀ ⦃c : CryptBoolean.BooleanFunction n⦄,
            c ∈ CryptBoolean.kerdockCodeOfRepresentatives F →
              c ∈ CryptBoolean.reedMuller 2 n) ∧
          (CryptBoolean.kerdockCodeOfRepresentatives F).card =
              2 ^ (2 * n) ∧
            CryptBoolean.minimumHammingDistance
                (CryptBoolean.kerdockCodeOfRepresentatives F) =
              2 ^ (n - 1) - 2 ^ (n / 2 - 1)
    theorem CryptBoolean.kerdockCodeOfRepresentatives_parameters
  {n : ℕ}
  {F :
    Finset
      (CryptBoolean.BooleanFunction n)}
  (hF :
    CryptBoolean.IsKerdockRepresentativeFamily
      F)
  (hnEven : Even n) (hn : 2 ≤ n) :
  F.offDiag.Nonempty ∧
    CryptBoolean.HasDistinctFirstOrderCosets
        F ∧
      (∀
          ⦃c :
            CryptBoolean.BooleanFunction
              n⦄,
          c ∈
              CryptBoolean.reedMuller 1
                n →
            c ∈
              CryptBoolean.kerdockCodeOfRepresentatives
                F) ∧
        (∀
            ⦃c :
              CryptBoolean.BooleanFunction
                n⦄,
            c ∈
                CryptBoolean.kerdockCodeOfRepresentatives
                  F →
              c ∈
                CryptBoolean.reedMuller 2
                  n) ∧
          (CryptBoolean.kerdockCodeOfRepresentatives
                  F).card =
              2 ^ (2 * n) ∧
            CryptBoolean.minimumHammingDistance
                (CryptBoolean.kerdockCodeOfRepresentatives
                  F) =
              2 ^ (n - 1) -
                2 ^ (n / 2 - 1)
    The Kerdock parameters determined by a finite quadratic representative
family in positive even dimension.
Theorem5.15.3
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 1.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagscarletchapter-6kerdockrelation-56pages-109-110fidelity-exact-explicit-coordinate-hypotheses

Self-dual normal-basis trace identity (Carlet, pp. 109--110). Let m=2t+1 and identify V_m with \mathbb F_{2^m} through a self-dual normal basis. Explicitly, assume that the coordinate equivalence intertwines Frobenius squaring with cyclic rotation, identifies the absolute trace with the coordinate sum, and identifies the trace pairing with the standard binary dot product. Under the induced identification V_{m+1}\simeq\mathbb F_{2^m}\times\mathbb F_2, the complete quadratic function of Relation (56) is q(x,z)=\operatorname{Tr}_m\!\left(\sum_{j=1}^{t}x^{2^j+1}\right) +z\operatorname{Tr}_m(x).

Lean code for Theorem5.15.3●1 theorem
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockCoordinateIdentity.lean
    complete
    theorem CryptBoolean.completeQuadraticBit_eq_kerdockFieldRepresentative_one_of_selfDualNormalCoordinates
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (hnormal :
    ∀ (x : FABL.F₂Cube (2 * t + 1)),
      (theta fun i => x ((finRotate (2 * t + 1)) i)) = theta x ^ 2)
  (htrace :
    ∀ (x : FABL.F₂Cube (2 * t + 1)),
      (CryptBoolean.absoluteTrace (2 * t + 1)) (theta x) = ∑ i, x i)
  (hselfDual :
    ∀ (x y : FABL.F₂Cube (2 * t + 1)),
      (CryptBoolean.absoluteTrace (2 * t + 1)) (theta x * theta y) =
        ∑ i, x i * y i) :
  FABL.completeQuadraticBit =
    CryptBoolean.kerdockFieldRepresentative t theta 1
    theorem CryptBoolean.completeQuadraticBit_eq_kerdockFieldRepresentative_one_of_selfDualNormalCoordinates
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (hnormal :
    ∀ (x : FABL.F₂Cube (2 * t + 1)),
      (theta fun i =>
          x ((finRotate (2 * t + 1)) i)) =
        theta x ^ 2)
  (htrace :
    ∀ (x : FABL.F₂Cube (2 * t + 1)),
      (CryptBoolean.absoluteTrace
            (2 * t + 1))
          (theta x) =
        ∑ i, x i)
  (hselfDual :
    ∀ (x y : FABL.F₂Cube (2 * t + 1)),
      (CryptBoolean.absoluteTrace
            (2 * t + 1))
          (theta x * theta y) =
        ∑ i, x i * y i) :
  FABL.completeQuadraticBit =
    CryptBoolean.kerdockFieldRepresentative
      t theta 1
    Under self-dual normal-basis coordinates, Relation (56) is the
finite-field Kerdock trace formula. The hypotheses state the Frobenius
rotation, absolute-trace coordinate sum, and self-dual trace pairing.
Theorem5.15.4
Group: Chapter 5: Bent functions (69)
Group member previews
Preview
Definition 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Definition 1.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagscarletchapter-6kerdockpages-109-110fidelity-source-footnote-44-coordinate-invariant

Finite-field construction of the Kerdock code (Carlet, pp. 109--110). Let m=2t+1, set n=m+1, and define q(x,z)=\operatorname{Tr}_m\!\left(\sum_{j=1}^{t}x^{2^j+1}\right) +z\operatorname{Tr}_m(x) on \mathbb F_{2^m}\times\mathbb F_2. For u\in\mathbb F_{2^m}, set q_u(x,z)=q(ux,z) and transport these functions to V_n along an \mathbb F_2-linear coordinate identification. The representative q_0 is zero, every q_u with u\ne0 has algebraic degree two, and q_u+q_v is bent whenever u\ne v. Thus the 2^m representatives form a Kerdock representative family. Consequently the union of the cosets q_u+R(1,n) is a Kerdock code with 2^{2n} words and minimum distance 2^{n-1}-2^{n/2-1}.

Lean code for Theorem5.15.4●22 declarations
  • defdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    def CryptBoolean.kerdockTraceQuadratic (t : ℕ) :
  CryptBoolean.FieldBooleanFunction (2 * t + 1)
    def CryptBoolean.kerdockTraceQuadratic
  (t : ℕ) :
  CryptBoolean.FieldBooleanFunction
    (2 * t + 1)
    The homogeneous trace quadratic used in the Kerdock construction.
  • defdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    def CryptBoolean.kerdockFieldQuadratic (t : ℕ)
  (u x : CryptBoolean.BinaryGaloisField (2 * t + 1)) (z : FABL.𝔽₂) :
  FABL.𝔽₂
    def CryptBoolean.kerdockFieldQuadratic (t : ℕ)
  (u x :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1))
  (z : FABL.𝔽₂) : FABL.𝔽₂
    The field-coordinate Kerdock representative indexed by `u`.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.absoluteTrace_algebraMap_odd (t : ℕ) (c : FABL.𝔽₂) :
  (CryptBoolean.absoluteTrace (2 * t + 1))
      ((algebraMap FABL.𝔽₂ (CryptBoolean.BinaryGaloisField (2 * t + 1)))
        c) =
    c
    theorem CryptBoolean.absoluteTrace_algebraMap_odd
  (t : ℕ) (c : FABL.𝔽₂) :
  (CryptBoolean.absoluteTrace (2 * t + 1))
      ((algebraMap FABL.𝔽₂
          (CryptBoolean.BinaryGaloisField
            (2 * t + 1)))
        c) =
    c
    On an odd binary extension, the absolute trace restricts to the identity
on the prime field.
  • defdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    def CryptBoolean.kerdockTraceCube (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  CryptBoolean.BooleanFunction (2 * t + 1)
    def CryptBoolean.kerdockTraceCube (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1)) :
  CryptBoolean.BooleanFunction (2 * t + 1)
    The odd-dimensional trace quadratic pulled back to binary coordinates.
  • defdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    def CryptBoolean.kerdockTraceLinearCube (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  CryptBoolean.BooleanFunction (2 * t + 1)
    def CryptBoolean.kerdockTraceLinearCube
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1)) :
  CryptBoolean.BooleanFunction (2 * t + 1)
    The linear trace character paired with the Kerdock field parameter.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_kerdockTraceCube_le_two (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockTraceCube t theta u) ≤
    2
    theorem CryptBoolean.functionAlgebraicDegree_kerdockTraceCube_le_two
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockTraceCube t
        theta u) ≤
    2
    The binary-coordinate trace quadratic has algebraic degree at most two.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_kerdockTraceLinearCube_le_one
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockTraceLinearCube t theta u) ≤
    1
    theorem CryptBoolean.functionAlgebraicDegree_kerdockTraceLinearCube_le_one
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockTraceLinearCube
        t theta u) ≤
    1
    The trace character paired with `u` is affine-linear.
  • defdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    def CryptBoolean.kerdockFieldCoordinateEquiv (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  FABL.F₂Cube (2 * t + 1 + 1) ≃ₗ[FABL.𝔽₂]
    CryptBoolean.BinaryGaloisField (2 * t + 1) × FABL.𝔽₂
    def CryptBoolean.kerdockFieldCoordinateEquiv
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1)) :
  FABL.F₂Cube (2 * t + 1 + 1) ≃ₗ[FABL.𝔽₂]
    CryptBoolean.BinaryGaloisField
        (2 * t + 1) ×
      FABL.𝔽₂
    Coordinates on the Kerdock ambient cube, split into the odd-dimensional
field coordinate and the final bit.
  • defdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    def CryptBoolean.kerdockFieldRepresentative (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  CryptBoolean.BooleanFunction (2 * t + 1 + 1)
    def CryptBoolean.kerdockFieldRepresentative
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1)) :
  CryptBoolean.BooleanFunction
    (2 * t + 1 + 1)
    The Boolean representative obtained by transporting the field-coordinate
quadratic to the canonical binary cube.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.kerdockFieldRepresentative_coordinate (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u x : CryptBoolean.BinaryGaloisField (2 * t + 1)) (z : FABL.𝔽₂) :
  CryptBoolean.kerdockFieldRepresentative t theta u
      ((CryptBoolean.kerdockFieldCoordinateEquiv t theta).symm (x, z)) =
    CryptBoolean.kerdockFieldQuadratic t u x z
    theorem CryptBoolean.kerdockFieldRepresentative_coordinate
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u x :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1))
  (z : FABL.𝔽₂) :
  CryptBoolean.kerdockFieldRepresentative
      t theta u
      ((CryptBoolean.kerdockFieldCoordinateEquiv
            t theta).symm
        (x, z)) =
    CryptBoolean.kerdockFieldQuadratic t u
      x z
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.kerdockFieldRepresentative_zero (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  CryptBoolean.kerdockFieldRepresentative t theta 0 = 0
    theorem CryptBoolean.kerdockFieldRepresentative_zero
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1)) :
  CryptBoolean.kerdockFieldRepresentative
      t theta 0 =
    0
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_kerdockFieldRepresentative_le_two
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockFieldRepresentative t theta u) ≤
    2
    theorem CryptBoolean.functionAlgebraicDegree_kerdockFieldRepresentative_le_two
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1)) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockFieldRepresentative
        t theta u) ≤
    2
    Every finite-field Kerdock representative has algebraic degree at most
two.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.quadraticPolarKernel_kerdockFieldRepresentative (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1))
  (a b : FABL.F₂Cube (2 * t + 1 + 1)) :
  have xz := (CryptBoolean.kerdockFieldCoordinateEquiv t theta) a;
  have yr := (CryptBoolean.kerdockFieldCoordinateEquiv t theta) b;
  CryptBoolean.quadraticPolarKernel
      (CryptBoolean.kerdockFieldRepresentative t theta u) a b =
    (CryptBoolean.absoluteTrace (2 * t + 1)) (u * xz.1) *
            (CryptBoolean.absoluteTrace (2 * t + 1)) (u * yr.1) +
          (CryptBoolean.absoluteTrace (2 * t + 1))
            (u ^ 2 * (xz.1 * yr.1)) +
        xz.2 * (CryptBoolean.absoluteTrace (2 * t + 1)) (u * yr.1) +
      yr.2 * (CryptBoolean.absoluteTrace (2 * t + 1)) (u * xz.1)
    theorem CryptBoolean.quadraticPolarKernel_kerdockFieldRepresentative
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1))
  (a b : FABL.F₂Cube (2 * t + 1 + 1)) :
  have xz :=
    (CryptBoolean.kerdockFieldCoordinateEquiv
        t theta)
      a;
  have yr :=
    (CryptBoolean.kerdockFieldCoordinateEquiv
        t theta)
      b;
  CryptBoolean.quadraticPolarKernel
      (CryptBoolean.kerdockFieldRepresentative
        t theta u)
      a b =
    (CryptBoolean.absoluteTrace
                (2 * t + 1))
              (u * xz.1) *
            (CryptBoolean.absoluteTrace
                (2 * t + 1))
              (u * yr.1) +
          (CryptBoolean.absoluteTrace
              (2 * t + 1))
            (u ^ 2 * (xz.1 * yr.1)) +
        xz.2 *
          (CryptBoolean.absoluteTrace
              (2 * t + 1))
            (u * yr.1) +
      yr.2 *
        (CryptBoolean.absoluteTrace
            (2 * t + 1))
          (u * xz.1)
    The polar form of one field-coordinate Kerdock representative.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.quadraticPolarKernel_kerdockFieldRepresentative_add (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u v : CryptBoolean.BinaryGaloisField (2 * t + 1))
  (a b : FABL.F₂Cube (2 * t + 1 + 1)) :
  have xz := (CryptBoolean.kerdockFieldCoordinateEquiv t theta) a;
  have yr := (CryptBoolean.kerdockFieldCoordinateEquiv t theta) b;
  have w := u + v;
  CryptBoolean.quadraticPolarKernel
      (CryptBoolean.kerdockFieldRepresentative t theta u +
        CryptBoolean.kerdockFieldRepresentative t theta v)
      a b =
    (CryptBoolean.absoluteTrace (2 * t + 1)) (u * xz.1) *
              (CryptBoolean.absoluteTrace (2 * t + 1)) (u * yr.1) +
            (CryptBoolean.absoluteTrace (2 * t + 1)) (v * xz.1) *
              (CryptBoolean.absoluteTrace (2 * t + 1)) (v * yr.1) +
          (CryptBoolean.absoluteTrace (2 * t + 1))
            (w ^ 2 * (xz.1 * yr.1)) +
        xz.2 * (CryptBoolean.absoluteTrace (2 * t + 1)) (w * yr.1) +
      yr.2 * (CryptBoolean.absoluteTrace (2 * t + 1)) (w * xz.1)
    theorem CryptBoolean.quadraticPolarKernel_kerdockFieldRepresentative_add
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u v :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1))
  (a b : FABL.F₂Cube (2 * t + 1 + 1)) :
  have xz :=
    (CryptBoolean.kerdockFieldCoordinateEquiv
        t theta)
      a;
  have yr :=
    (CryptBoolean.kerdockFieldCoordinateEquiv
        t theta)
      b;
  have w := u + v;
  CryptBoolean.quadraticPolarKernel
      (CryptBoolean.kerdockFieldRepresentative
          t theta u +
        CryptBoolean.kerdockFieldRepresentative
          t theta v)
      a b =
    (CryptBoolean.absoluteTrace
                  (2 * t + 1))
                (u * xz.1) *
              (CryptBoolean.absoluteTrace
                  (2 * t + 1))
                (u * yr.1) +
            (CryptBoolean.absoluteTrace
                  (2 * t + 1))
                (v * xz.1) *
              (CryptBoolean.absoluteTrace
                  (2 * t + 1))
                (v * yr.1) +
          (CryptBoolean.absoluteTrace
              (2 * t + 1))
            (w ^ 2 * (xz.1 * yr.1)) +
        xz.2 *
          (CryptBoolean.absoluteTrace
              (2 * t + 1))
            (w * yr.1) +
      yr.2 *
        (CryptBoolean.absoluteTrace
            (2 * t + 1))
          (w * xz.1)
    The polar form of the sum of two representatives, expressed through
their parameter sum.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.eq_zero_of_forall_quadraticPolarKernel_kerdockFieldRepresentative_add
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u v : CryptBoolean.BinaryGaloisField (2 * t + 1)) (huv : u ≠ v)
  (a : FABL.F₂Cube (2 * t + 1 + 1))
  (ha :
    ∀ (b : FABL.F₂Cube (2 * t + 1 + 1)),
      CryptBoolean.quadraticPolarKernel
          (CryptBoolean.kerdockFieldRepresentative t theta u +
            CryptBoolean.kerdockFieldRepresentative t theta v)
          a b =
        0) :
  a = 0
    theorem CryptBoolean.eq_zero_of_forall_quadraticPolarKernel_kerdockFieldRepresentative_add
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u v :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1))
  (huv : u ≠ v)
  (a : FABL.F₂Cube (2 * t + 1 + 1))
  (ha :
    ∀ (b : FABL.F₂Cube (2 * t + 1 + 1)),
      CryptBoolean.quadraticPolarKernel
          (CryptBoolean.kerdockFieldRepresentative
              t theta u +
            CryptBoolean.kerdockFieldRepresentative
              t theta v)
          a b =
        0) :
  a = 0
    Distinct field parameters give a sum whose quadratic polar form has
trivial radical.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.isBent_kerdockFieldRepresentative_add (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u v : CryptBoolean.BinaryGaloisField (2 * t + 1)) (huv : u ≠ v) :
  CryptBoolean.IsBent
    (CryptBoolean.kerdockFieldRepresentative t theta u +
      CryptBoolean.kerdockFieldRepresentative t theta v)
    theorem CryptBoolean.isBent_kerdockFieldRepresentative_add
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u v :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1))
  (huv : u ≠ v) :
  CryptBoolean.IsBent
    (CryptBoolean.kerdockFieldRepresentative
        t theta u +
      CryptBoolean.kerdockFieldRepresentative
        t theta v)
    Distinct field parameters index representatives with bent pairwise sum.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.functionAlgebraicDegree_kerdockFieldRepresentative_eq_two
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1))
  (u : CryptBoolean.BinaryGaloisField (2 * t + 1)) (hu : u ≠ 0) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockFieldRepresentative t theta u) =
    2
    theorem CryptBoolean.functionAlgebraicDegree_kerdockFieldRepresentative_eq_two
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1))
  (u :
    CryptBoolean.BinaryGaloisField
      (2 * t + 1))
  (hu : u ≠ 0) :
  FABL.functionAlgebraicDegree
      (CryptBoolean.kerdockFieldRepresentative
        t theta u) =
    2
    A representative with nonzero field parameter is genuinely quadratic.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.kerdockFieldRepresentative_injective (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  Function.Injective (CryptBoolean.kerdockFieldRepresentative t theta)
    theorem CryptBoolean.kerdockFieldRepresentative_injective
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1)) :
  Function.Injective
    (CryptBoolean.kerdockFieldRepresentative
      t theta)
    Distinct field parameters determine distinct Boolean representatives.
  • defdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    def CryptBoolean.kerdockFieldRepresentativeFamily (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  Finset (CryptBoolean.BooleanFunction (2 * t + 1 + 1))
    def CryptBoolean.kerdockFieldRepresentativeFamily
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1)) :
  Finset
    (CryptBoolean.BooleanFunction
      (2 * t + 1 + 1))
    The finite set of all Kerdock representatives indexed by the odd binary
field.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.card_kerdockFieldRepresentativeFamily (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  (CryptBoolean.kerdockFieldRepresentativeFamily t theta).card =
    2 ^ (2 * t + 1)
    theorem CryptBoolean.card_kerdockFieldRepresentativeFamily
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1)) :
  (CryptBoolean.kerdockFieldRepresentativeFamily
        t theta).card =
    2 ^ (2 * t + 1)
    The finite-field representative set has one member for every field
parameter.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.isKerdockRepresentativeFamily_kerdockField (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  CryptBoolean.IsKerdockRepresentativeFamily
    (CryptBoolean.kerdockFieldRepresentativeFamily t theta)
    theorem CryptBoolean.isKerdockRepresentativeFamily_kerdockField
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1)) :
  CryptBoolean.IsKerdockRepresentativeFamily
    (CryptBoolean.kerdockFieldRepresentativeFamily
      t theta)
    The explicit finite-field family satisfies the Kerdock representative
conditions.
  • theoremdefined in CryptBoolean/Carlet/Chapter06/KerdockFieldConstruction.lean
    complete
    theorem CryptBoolean.kerdockFieldConstruction_parameters (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField (2 * t + 1)) :
  have F := CryptBoolean.kerdockFieldRepresentativeFamily t theta;
  CryptBoolean.IsKerdockRepresentativeFamily F ∧
    F.offDiag.Nonempty ∧
      CryptBoolean.HasDistinctFirstOrderCosets F ∧
        (∀ c ∈ CryptBoolean.reedMuller 1 (2 * t + 1 + 1),
            c ∈ CryptBoolean.kerdockCodeOfRepresentatives F) ∧
          (∀ c ∈ CryptBoolean.kerdockCodeOfRepresentatives F,
              c ∈ CryptBoolean.reedMuller 2 (2 * t + 1 + 1)) ∧
            (CryptBoolean.kerdockCodeOfRepresentatives F).card =
                2 ^ (2 * (2 * t + 1 + 1)) ∧
              CryptBoolean.minimumHammingDistance
                  (CryptBoolean.kerdockCodeOfRepresentatives F) =
                2 ^ (2 * t + 1 + 1 - 1) - 2 ^ ((2 * t + 1 + 1) / 2 - 1)
    theorem CryptBoolean.kerdockFieldConstruction_parameters
  (t : ℕ)
  (theta :
    FABL.F₂Cube (2 * t + 1) ≃ₗ[FABL.𝔽₂]
      CryptBoolean.BinaryGaloisField
        (2 * t + 1)) :
  have F :=
    CryptBoolean.kerdockFieldRepresentativeFamily
      t theta;
  CryptBoolean.IsKerdockRepresentativeFamily
      F ∧
    F.offDiag.Nonempty ∧
      CryptBoolean.HasDistinctFirstOrderCosets
          F ∧
        (∀
            c ∈
              CryptBoolean.reedMuller 1
                (2 * t + 1 + 1),
            c ∈
              CryptBoolean.kerdockCodeOfRepresentatives
                F) ∧
          (∀
              c ∈
                CryptBoolean.kerdockCodeOfRepresentatives
                  F,
              c ∈
                CryptBoolean.reedMuller 2
                  (2 * t + 1 + 1)) ∧
            (CryptBoolean.kerdockCodeOfRepresentatives
                    F).card =
                2 ^
                  (2 * (2 * t + 1 + 1)) ∧
              CryptBoolean.minimumHammingDistance
                  (CryptBoolean.kerdockCodeOfRepresentatives
                    F) =
                2 ^ (2 * t + 1 + 1 - 1) -
                  2 ^
                    ((2 * t + 1 + 1) / 2 -
                      1)
    The explicit field representatives and their first-order coset union
have the Kerdock parameters.