5 Supporting Theories
5.1 Polynomials
This section contains facts about polynomials that are used in the rest of the library, and also definitions for computable representations of polynomials.
We note that the Schwartz-Zippel Lemma is already in Mathlib.
We also define the type of computable univariate & multilinear polynomials using arrays to represent their coefficients (or dually, their evaluations at given points).
5.2 Coding Theory
This section contains definitions and theorems about coding theory as they are used in the rest of the library.
5.3 The VCVio Library
This library provides a formal framework for reasoning about computations that make oracle queries. Many cryptographic primitives and interactive protocols use oracles to model (or simulate) external functionality such as random responses, coin flips, or more structured queries. The VCVio library "lifts" these ideas into a setting where both the abstract specification and concrete simulation of oracles may be studied, and their probabilistic behavior analyzed.
The main ingredients of the library are as follows:
An oracle specification describes a collection of available oracles, each with its own input and output types. Formally, it’s given by an indexed family where each oracle is specified by:
A domain type (what inputs it accepts)
A range type (what outputs it can produce)
The indexing allows for potentially infinite collections of oracles, and the specification itself is agnostic to how the oracles actually behave - it just describes their interfaces.
Some examples of oracle specifications (and their intended behavior) are as follows:
emptySpec: Represents an empty set of oraclessingletonSpec: Represents a single oracle available on a singleton indexcoinSpec: A coin flipping oracle that produces a random Boolean valueunifSpec: A family of oracles that for every natural number \(n \in \mathbb {N}\) chooses uniformly from the set \(\{ 0, \ldots , n\} \).
We often require extra properties on the domains and ranges of oracles. For example, we may require that the domains and ranges come equipped with decidable equality or finiteness properties .
An oracle computation represents a program that can make oracle queries. It can:
Return a pure value without making any queries (via pure)
Make an oracle query and continue with the response (via queryBind)
Signal failure (via failure)
The formal implementation uses a free monad on the inductive type of oracle queries wrapped in an option monad transformer (i.e. OptionT(FreeMonad(OracleQuery spec))).
To actually run oracle computations, we need a way to handle (or implement) the oracle queries. An oracle implementation consists a mapping from oracle queries to values in another monad. Depending on the monad, this may allow for various interpretations of the oracle queries.
We can view oracle computations as probabilistic programs by considering what happens when oracles respond uniformly at random. This gives rise to a probability distribution over possible outputs (including the possibility of failure). The semantics maps each oracle query to a uniform distribution over its possible responses.
Once we have mapped an oracle computation to a probability distribution, we can define various associated probabilities, such as the probability of failure, or the probability of the output satisfying a given predicate (assuming it does not fail).
We can simulate complex oracles using simpler ones by providing a translation mechanism. A simulation oracle specifies how to implement queries in one specification using computations in another specification, possibly maintaining additional state information during the simulation.
Using the simulation framework, we can add logging and caching behaviors to oracle queries:
Logging records all queries made during a computation
Caching remembers query responses and reuses them for repeated queries
These are implemented as special cases of simulation oracles.
A random oracle is implemented as a caching oracle that uses lazy sampling:
On first query: generates a uniform random response and caches it
On repeated queries: returns the cached response
5.4 The Subfield \(R_q^H \cong \mathbb {F}_{q^k}\) (Hachi Lemma 5)
This section is a blueprint for the one missing piece of Hachi [ 13 ] §3, Lemma 5: that the fixed subring \(R_q^H\) is a field and is isomorphic to \(\mathbb {F}_{q^k}\). The packing map \(\psi \) and the trace formula of Theorem 2 (the rest of §3) are already formalized; what remains is to upgrade \(R_q^H\) from “a Subring of cardinality \(q^k\)” to “a field \(\cong \mathbb {F}_{q^k}\)”.
Throughout, \(d = 2^\alpha \), \(R_q = \mathbb {Z}_q[X]/(X^{d}+1)\) with \(q\) an odd prime, \(k = 2^\kappa \) a divisor of \(d/2\) (i.e. \(2k \mid d\)), and \(H = \langle \sigma _{-1}, \sigma _{4k+1}\rangle \). For the field statement we additionally assume \(q \equiv 5 \pmod8\).
5.4.1 What already exists
\(R_q^H := \{ x \in R_q : \sigma _{-1}(x) = x \wedge \sigma _{4k+1}(x) = x\} \), defined as the meet of two eqLocus’s, hence a Subring.
Over \(R = \mathbb {Z}_q\) with \(q\) prime and \(2k \mid d\), \(\; |R_q^H| = q^{k}\).
The map \(\psi : (R_q^H)^{d/k} \to R_q\) is a bijection.
These two are proven with no sorry. The blueprint below adds the field structure on top.
5.4.2 Target
Let \(q\) be prime with \(q \equiv 5 \pmod8\) and \(2 \cdot 2^\kappa \mid 2^\alpha \). Then there is a ring isomorphism
The point of this decomposition is that the cardinality is already known (Theorem 215), so once field-ness is established we get the isomorphism without any finite-field Galois-descent analysis of the \(\sigma _{4k+1}\)-action.
5.4.3 Reduction to “\(R_q^H\) is a field”
The whole difficulty concentrates in field-ness; everything else is generic algebra reused from Mathlib.
Two finite fields of equal cardinality are isomorphic; in particular a finite field of cardinality \(q^{n}\) is isomorphic to \(\texttt{GaloisField } q\ n\). (Mathlib; GaloisField/FiniteField API.)
If \(S \le T\) is a subring of an integral domain \(T\), then \(S\) is an integral domain (it inherits NoZeroDivisors; Mathlib).
A finite nontrivial commutative integral domain is a field. (Mathlib; Finite.isField_of_domain / Fintype.fieldOfDomain.)
For \(q\) prime, \(q \equiv 5 \pmod8\), \(2k \mid d\), the ring \(R_q^H\) is a field.
\(R_q^{\sigma _{-1}} := \{ x \in R_q : \sigma _{-1}(x) = x\} = \texttt{eqLocus}\ \sigma _{-1}\ \mathrm{id}\).
\(R_q^H \subseteq R_q^{\sigma _{-1}}\), immediate from the definition of \(R_q^H\) as a meet whose first factor is \(R_q^{\sigma _{-1}}\).
5.4.4 The crux: \(R_q^{\sigma _{-1}}\) is a field
This is the only genuinely new mathematics. The route is the two-factor decomposition of \(R_q\) that is special to \(q \equiv 5 \pmod8\).
For \(q \equiv 5 \pmod8\) and \(\alpha \ge 1\), the multiplicative order of \(q\) in \((\mathbb {Z}/2^{\alpha +1})^\times \) is \(2^{\alpha -1}\).
\((\mathbb {Z}/2^{\alpha +1})^\times \cong \langle -1\rangle \times \langle 5\rangle \) with \(|\langle 5\rangle | = 2^{\alpha -1}\). Writing \(q \equiv (-1)^a 5^b\), the congruence \(q \equiv 5 \pmod8\) forces \(a = 0\) and \(b\) odd; since \(b\) is odd it is a unit mod \(2^{\alpha -1}\), so \(q\) generates \(\langle 5\rangle \) and \(\operatorname {ord}(q) = 2^{\alpha -1}\). The \(2\)-adic computation is the same lifting-the-exponent toolkit already used in Galois/Order.lean (two_pow_dvd_four_pow_sub_one_iff).
Over \(\mathbb {F}_q\) with \(q \equiv 5 \pmod8\), the polynomial \(X^{2^\alpha }+1 = \Phi _{2^{\alpha +1}}(X)\) factors as a product of exactly two distinct monic irreducible polynomials, each of degree \(2^{\alpha -1} = d/2\).
\(X^{2^\alpha }+1\) is the \(2^{\alpha +1}\)-th cyclotomic polynomial. Since \(q \nmid 2^{\alpha +1}\) it is separable over \(\mathbb {F}_q\), and over a finite field every irreducible factor of \(\Phi _n\) has degree \(\operatorname {ord}_n(q)\); the number of factors is \(\varphi (n)/\operatorname {ord}_n(q)\). With \(n = 2^{\alpha +1}\), \(\varphi (n) = 2^\alpha \) and \(\operatorname {ord}_n(q) = 2^{\alpha -1}\) (Lemma 224), giving exactly \(2\) factors of degree \(2^{\alpha -1}\). Formalized directly from Mathlib’s Polynomial.normalizedFactors_cyclotomic_card (factor count \(= \varphi (n)/\operatorname {ord}\)) together with Nat.totient_prime_pow_succ.
For \(q \equiv 5 \pmod8\), \(X^{2^\alpha }+1 = p_1 \cdot p_2\) over \(\mathbb {F}_q\) with \(p_1, p_2\) coprime and irreducible. (Extracted from the two normalized factors; coprimality of the distinct monic irreducibles via Irreducible.coprime_iff_not_dvd.)
5.4.5 The swap (Phase 4): \(\sigma _{-1}\) and polynomial reversal
The proof is gated by one fact: \(\sigma _{-1}\) interchanges the two factors. Rather than build the explicit CRT product \(K \times K\), we work directly in \(S := \mathbb {F}_q[X]/(X^{2^\alpha }+1)\) via a reverse identity and a divisibility argument.
In \(S\), with \(\mathrm{mk}\) the quotient map and \(\sigma _{-1} = \texttt{galoisAutₛ}\) of exponent \(2^{\alpha +1}-1\),
Since \(\mathrm{mk}\, X\) is a unit, \(\sigma _{-1}\) carries the ideal \((\mathrm{mk}\, p)\) onto \((\mathrm{mk}\, p^{\mathrm{rev}})\). Proved from Mathlib’s Polynomial.eval₂_reverse_mul_pow at the point \((\mathrm{mk}\, X)^{-1} = (\mathrm{mk}\, X)^{c}\).
For \(q \equiv 5 \pmod8\), reversal swaps the two factors: if \(X^{2^\alpha }+1 = p_1 p_2\) then \(p_1^{\mathrm{rev}}\) is associated to \(p_2\). (Left as sorry; carries the entire \(-1 \notin \langle q\rangle \) content.) The root set of \(p_1\) is a single Frobenius orbit \(=\) a coset of \(\langle q\rangle \); were \(p_1^{\mathrm{rev}} \sim p_1\) it would be closed under \(\zeta \mapsto \zeta ^{-1}\), i.e. \(-1 \in \langle q\rangle \), contradicting Lemma 229; as reversal permutes the two factors of the self-reciprocal \(X^{2^\alpha }+1\), it sends \(p_1\) to \(p_2\).
For \(q \equiv 5 \pmod8\) and \(\alpha \ge 1\), no power of \(q\) equals \(-1\) in \(\mathbb {Z}/2^{\alpha +1}\) (every power is \(\equiv 1 \pmod4\), while \(-1 \equiv 3\)).
5.4.6 Phase 5: assembling the field and the isomorphism
In \(S = \mathbb {F}_q[X]/(X^{2^\alpha }+1)\) every nonzero \(\sigma _{-1}\)-fixed element is a unit.
Write the element as \(\mathrm{mk}\, g\). If it is not a unit then \(g\) is not coprime to \(X^{2^\alpha }+1 = p_1 p_2\), so (WLOG) \(p_1 \mid g\). The reverse identity (Lemma 227) together with \(p_1^{\mathrm{rev}} \sim p_2\) (Lemma 228) gives \(\mathrm{mk}\, p_2 \mid \sigma _{-1}(\mathrm{mk}\, p_1) \mid \sigma _{-1}(\mathrm{mk}\, g) = \mathrm{mk}\, g\), hence \(p_2 \mid g\). With \(p_1 \mid g\) and \(p_1, p_2\) coprime, \(X^{2^\alpha }+1 \mid g\), so \(\mathrm{mk}\, g = 0\) — contradiction.
For \(q\) prime with \(q \equiv 5 \pmod8\) and \(\alpha \ge 1\), \(R_q^{\sigma _{-1}}\) is a field.
Transport along \(R_q \cong S\) (Rq.equivQuotient), under which \(\sigma _{-1}\) becomes \(\texttt{galoisAutₛ}\) (galoisAut_toQuotient). A nonzero \(\sigma _{-1}\)-fixed element of \(R_q^{\sigma _{-1}}\) maps to a nonzero fixed element of \(S\), a unit by Theorem 230; its inverse is again \(\sigma _{-1}\)-fixed (apply \(\sigma _{-1}\) to \(a a^{-1} = 1\) and cancel the unit), so it lies in \(R_q^{\sigma _{-1}}\).
5.4.7 Status and dependency summary
Everything below is formalized and compiles, with the single exception of 228, which is left as sorry and carries the entire \(-1 \notin \langle q\rangle \) content of the swap.
Reused, done: 214, 215, 216, the fintype instance, the LTE order toolkit in Galois/Order.lean, and IsCyclotomic (which already gives \(X^{2^\alpha }+1 = \Phi _{2^{\alpha +1}}\) and, via Rq.equivQuotient, lands in the Mathlib quotient \(S\)).
Phase 0 — glue: 222, 223; the assembly 221 (subring-of-field domain \(\Rightarrow \) finite domain \(\Rightarrow \) field) and 217 (FiniteField.ringEquivOfCardEq).
Phase 1 — number theory: 224 (via ZMod.orderOf_one_add_four_mul), 229.
Phase 2 — factorization: 225 (count via normalizedFactors_cyclotomic_card), 226.
Phase 4 — the swap: 227 (the reverse identity, via eval₂_reverse_mul_pow) and \(\boxed {\ref{lem:no_selfReciprocal}\ (\texttt{sorry})}\).
Files. Subfield/Factorization.lean (Phases 1–2, importing Galois/Order.lean) and Subfield/Field.lean (Phases 4–5 and the Phase 0/glue assembly); the \(\sigma _{-1}\)-fixed subring helper 222 sits in Galois/FixedSubring.lean. The implementation works directly in \(S\) via the reverse identity and a divisibility argument, rather than constructing the explicit CRT product \(R_q \cong K\times K\) (which is therefore not needed). The sole remaining sorry is 228.