1.8. Finite-field representations🔗

Definition1.8.1

uses 0used by 1✓L∃∀N

Tagscarletchapter-2absolute-tracepage-15fidelity-exact-direct-mathlib

Absolute trace (Carlet, p. 15). Let n>0, let K_n=\operatorname{GF}(2^n), and let \iota:\mathbb F_2\hookrightarrow K_n be the canonical embedding. The absolute trace is the \mathbb F_2-linear map \operatorname{Tr}_n:K_n\longrightarrow\mathbb F_2, \qquad \iota(\operatorname{Tr}_n(x)) =\sum_{i=0}^{n-1}x^{2^i}. The pairing (x,y)\mapsto\operatorname{Tr}_n(xy) is nondegenerate; hence \operatorname{Tr}_n is surjective. In particular, choose \tau\in K_n with \operatorname{Tr}_n(\tau)=1. For every f:K_n\to\mathbb F_2, define F_\tau(x)= \begin{cases} 0,&f(x)=0,\\ \tau,&f(x)=1. \end{cases} Then \operatorname{Tr}_n(F_\tau(x))=f(x) \qquad(x\in K_n).

Lean code for Definition1.8.1●10 declarations

abbrevdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

abbrev CryptBoolean.BinaryGaloisField (n : ℕ) : Type

abbrev CryptBoolean.BinaryGaloisField (n : ℕ) :
  Type

Mathlib's canonical field with `2^n` elements.

abbrevdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

abbrev CryptBoolean.FieldBooleanFunction (n : ℕ) : Type

abbrev CryptBoolean.FieldBooleanFunction
  (n : ℕ) : Type

A scalar Boolean function represented on the binary Galois field.

defdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

def CryptBoolean.absoluteTrace (n : ℕ) :
  CryptBoolean.BinaryGaloisField n →ₗ[FABL.𝔽₂] FABL.𝔽₂

def CryptBoolean.absoluteTrace (n : ℕ) :
  CryptBoolean.BinaryGaloisField
      n →ₗ[FABL.𝔽₂]
    FABL.𝔽₂

The absolute trace from `GF(2^n)` to `GF(2)`.

theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

theorem CryptBoolean.algebraMap_absoluteTrace_eq_sum_frobenius {n : ℕ}
  (hn : n ≠ 0) (x : CryptBoolean.BinaryGaloisField n) :
  (algebraMap FABL.𝔽₂ (CryptBoolean.BinaryGaloisField n))
      ((CryptBoolean.absoluteTrace n) x) =
    ∑ i ∈ Finset.range n, x ^ 2 ^ i

theorem CryptBoolean.algebraMap_absoluteTrace_eq_sum_frobenius
  {n : ℕ} (hn : n ≠ 0)
  (x : CryptBoolean.BinaryGaloisField n) :
  (algebraMap FABL.𝔽₂
        (CryptBoolean.BinaryGaloisField
          n))
      ((CryptBoolean.absoluteTrace n) x) =
    ∑ i ∈ Finset.range n, x ^ 2 ^ i

Mathlib's finite-field trace formula specializes to the absolute binary trace.

theoremdefined in Mathlib/RingTheory/Trace/Basic.lean

complete

theorem traceForm_nondegenerate.{u_4, u_5} (K : Type u_4) (L : Type u_5)
  [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
  [Algebra.IsSeparable K L] : (Algebra.traceForm K L).Nondegenerate

theorem traceForm_nondegenerate.{u_4, u_5}
  (K : Type u_4) (L : Type u_5) [Field K]
  [Field L] [Algebra K L]
  [FiniteDimensional K L]
  [Algebra.IsSeparable K L] :
  (Algebra.traceForm K L).Nondegenerate

Let $L/K$ be a finite extension of fields. If $L/K$ is separable,
then `traceForm` is nondegenerate.

theoremdefined in Mathlib/RingTheory/Trace/Basic.lean

complete

theorem Algebra.trace_surjective.{u_4, u_5} (K : Type u_4) (L : Type u_5)
  [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
  [Algebra.IsSeparable K L] : Function.Surjective ⇑(Algebra.trace K L)

theorem Algebra.trace_surjective.{u_4, u_5}
  (K : Type u_4) (L : Type u_5) [Field K]
  [Field L] [Algebra K L]
  [FiniteDimensional K L]
  [Algebra.IsSeparable K L] :
  Function.Surjective ⇑(Algebra.trace K L)

theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

theorem CryptBoolean.exists_absoluteTrace_eq_one (n : ℕ) :
  ∃ traceOne, (CryptBoolean.absoluteTrace n) traceOne = 1

theorem CryptBoolean.exists_absoluteTrace_eq_one
  (n : ℕ) :
  ∃ traceOne,
    (CryptBoolean.absoluteTrace n)
        traceOne =
      1

Nondegeneracy of the finite-field trace supplies an element of absolute trace one.

theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

theorem CryptBoolean.absoluteTrace_surjective (n : ℕ) :
  Function.Surjective ⇑(CryptBoolean.absoluteTrace n)

theorem CryptBoolean.absoluteTrace_surjective
  (n : ℕ) :
  Function.Surjective
    ⇑(CryptBoolean.absoluteTrace n)

The absolute trace onto the binary prime field is surjective.

defdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

def CryptBoolean.traceLift {n : ℕ}
  (traceOne : CryptBoolean.BinaryGaloisField n)
  (f : CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.BinaryGaloisField n → CryptBoolean.BinaryGaloisField n

def CryptBoolean.traceLift {n : ℕ}
  (traceOne :
    CryptBoolean.BinaryGaloisField n)
  (f :
    CryptBoolean.FieldBooleanFunction n) :
  CryptBoolean.BinaryGaloisField n →
    CryptBoolean.BinaryGaloisField n

A field-valued lift selected by a trace-one element.

theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

theorem CryptBoolean.absoluteTrace_traceLift {n : ℕ}
  (traceOne : CryptBoolean.BinaryGaloisField n)
  (htraceOne : (CryptBoolean.absoluteTrace n) traceOne = 1)
  (f : CryptBoolean.FieldBooleanFunction n)
  (x : CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.absoluteTrace n) (CryptBoolean.traceLift traceOne f x) =
    f x

theorem CryptBoolean.absoluteTrace_traceLift
  {n : ℕ}
  (traceOne :
    CryptBoolean.BinaryGaloisField n)
  (htraceOne :
    (CryptBoolean.absoluteTrace n)
        traceOne =
      1)
  (f :
    CryptBoolean.FieldBooleanFunction n)
  (x : CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.absoluteTrace n)
      (CryptBoolean.traceLift traceOne f
        x) =
    f x

Every field-domain Boolean function is an absolute trace of a field-valued function.

Formalization note. The field, finite-field trace, trace nondegeneracy, and Frobenius-sum theorem are provided by Mathlib. The Blueprint statement records the resulting mathematics rather than those implementation choices.

Theorem1.8.2

uses 0used by 0✓L∃∀N

Tagscarletchapter-2relation-4page-15fidelity-exact

Univariate representation (Carlet, Relation (4), p. 15). Let n>0 and K_n=\operatorname{GF}(2^n). For every function F:K_n\to K_n, there exists a unique polynomial P_F\in K_n[X] such that \deg P_F<2^n \qquad\text{and}\qquad P_F(x)=F(x)\quad\text{for every }x\in K_n. Equivalently, P_F(X)=\sum_{i=0}^{2^n-1}\delta_iX^i for uniquely determined coefficients \delta_i\in K_n.

Lean code for Theorem1.8.2●4 declarations

defdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

def CryptBoolean.univariateRepresentation {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  Polynomial (CryptBoolean.BinaryGaloisField n)

def CryptBoolean.univariateRepresentation
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  Polynomial
    (CryptBoolean.BinaryGaloisField n)

The canonical Lagrange polynomial representing a function on `GF(2^n)`.

theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

theorem CryptBoolean.eval_univariateRepresentation {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n → CryptBoolean.BinaryGaloisField n)
  (x : CryptBoolean.BinaryGaloisField n) :
  Polynomial.eval x (CryptBoolean.univariateRepresentation F) = F x

theorem CryptBoolean.eval_univariateRepresentation
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n)
  (x : CryptBoolean.BinaryGaloisField n) :
  Polynomial.eval x
      (CryptBoolean.univariateRepresentation
        F) =
    F x

The univariate representation evaluates to the original function.

theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

theorem CryptBoolean.degree_univariateRepresentation_lt_card {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.univariateRepresentation F).degree <
    ↑(Nat.card (CryptBoolean.BinaryGaloisField n))

theorem CryptBoolean.degree_univariateRepresentation_lt_card
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  (CryptBoolean.univariateRepresentation
        F).degree <
    ↑(Nat.card
        (CryptBoolean.BinaryGaloisField
          n))

The canonical univariate representation has degree strictly below the field cardinality.

theoremdefined in CryptBoolean/Carlet/Chapter02/FiniteField.lean

complete

theorem CryptBoolean.existsUnique_univariateRepresentation {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  ∃! P,
    P.degree < ↑(Nat.card (CryptBoolean.BinaryGaloisField n)) ∧
      ∀ (x : CryptBoolean.BinaryGaloisField n),
        Polynomial.eval x P = F x

theorem CryptBoolean.existsUnique_univariateRepresentation
  {n : ℕ}
  (F :
    CryptBoolean.BinaryGaloisField n →
      CryptBoolean.BinaryGaloisField n) :
  ∃! P,
    P.degree <
        ↑(Nat.card
            (CryptBoolean.BinaryGaloisField
              n)) ∧
      ∀
        (x :
          CryptBoolean.BinaryGaloisField
            n),
        Polynomial.eval x P = F x

Carlet's unique univariate representation below degree `2^n`.

Formalization note. The canonical witness is finite Lagrange interpolation. This theorem has no mathematical dependency on the absolute trace, so no such edge is recorded in the Blueprint graph.

Proposition1.8.3

Statement uses 2

Statement dependency previews

Preview

Definition 1.8.1

Loading preview

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

used by 0XL∃∀N

Tagscarletchapter-2proposition-3pages-17-18source-open

Proposition 3 (Carlet, pp. 17--18). Let n>0, let a\in K_n, choose an \mathbb F_2-linear isomorphism \theta:V_n\xrightarrow{\sim}K_n, and let k be represented by an integer 0\le k<2^n-1 modulo 2^n-1. If the Boolean function f_\theta(x)=\operatorname{Tr}_n\!\left(a\,\theta(x)^k\right) is not identically zero, then \deg_{\mathrm{alg}}(f_\theta)=w_2(k), where w_2(k) is the number of nonzero digits in the binary expansion of k.

Formalization note. Carlet identifies K_n with V_n after fixing a basis. Making the coordinate isomorphism explicit is necessary to apply the cube-based definition of algebraic degree; changing the basis composes f_\theta with a linear automorphism, so affine invariance makes the displayed degree basis-independent.