Admissible fields exist

MIPRE.SAT.BinField k is what thm:pcp-decider takes as a parameter: a field of size 2^k with a fixed k-bit representation of its elements. This file inhabits it, for every k ≥ 1.

The field is Mathlib's GaloisField 2 k and the representation is the coordinate vector in an arbitrary basis. That is enough for BinField as stated -- the structure asks for the cardinality and a representation with a left inverse, and nothing more -- so it is enough to remove thm:pcp-decider's field parameter from the list of things this project assumes.

What this does not do. It is not lem:self-dual-basis. The basis here is whatever Module.finBasisOfFinrankEq returns; it is not normal, not self-dual, and carries no multiplication tables, so the \downsize maps of lem:downsize-field are not computed by the trace form and there is no poly(k) bound on anything. Consumers that need those --- the downsized samplers of lem:cl-downsize past field size 2 --- need the self-dual normal basis, and MIPRE.SAT.BinField will have to grow fields for it before they can be served. The point of this file is the narrower one: nothing in the pipeline should be blocked on an existence question that Mathlib already answers.

def MIPRE.SAT.bitOf (z : ZMod 2) : Bool

The coordinate representation of a ZMod 2-vector as bits.

Equations

• MIPRE.SAT.bitOf z = decide (z = 1)

theorem MIPRE.SAT.ite_bitOf (z : ZMod 2) : (if bitOf z = true then 1 else 0) = z

noncomputable def MIPRE.SAT.binFieldGalois (k : ℕ) (hk : k ≠ 0) : BinField k

An admissible field of size 2^k with a bit representation, for every k ≥ 1: Mathlib's GaloisField 2 k with coordinates in a basis. See the module docstring for what this is not.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.SAT.nonempty_binField (k : ℕ) (hk : k ≠ 0) : Nonempty (BinField k)