Dependencies

\(R_q^{\sigma _{-1}} := \{ x \in R_q : \sigma _{-1}(x) = x\} = \texttt{eqLocus}\ \sigma _{-1}\ \mathrm{id}\).

\(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.

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.

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.

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))).

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.

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.

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

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.

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\), \(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.)

A finite nontrivial commutative integral domain is a field. (Mathlib; Finite.isField_of_domain / Fintype.fieldOfDomain.)

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.)

\(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}}\).

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\)).

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\), the multiplicative order of \(q\) in \((\mathbb {Z}/2^{\alpha +1})^\times \) is \(2^{\alpha -1}\).

If \(S \le T\) is a subring of an integral domain \(T\), then \(S\) is an integral domain (it inherits NoZeroDivisors; Mathlib).

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\).

Over \(R = \mathbb {Z}_q\) with \(q\) prime and \(2k \mid d\), \(\; |R_q^H| = q^{k}\).

For \(q\) prime with \(q \equiv 5 \pmod8\) and \(\alpha \ge 1\), \(R_q^{\sigma _{-1}}\) is a field.

In \(S = \mathbb {F}_q[X]/(X^{2^\alpha }+1)\) every nonzero \(\sigma _{-1}\)-fixed element is a unit.

Let \(q\) be prime with \(q \equiv 5 \pmod8\) and \(2 \cdot 2^\kappa \mid 2^\alpha \). Then there is a ring isomorphism

For \(q\) prime, \(q \equiv 5 \pmod8\), \(2k \mid d\), the ring \(R_q^H\) is a field.

The map \(\psi : (R_q^H)^{d/k} \to R_q\) is a bijection.