Downsizing conditionally linear functions, and reindexing #
Paper linear.tex, def:cl-downsize, lem:cl-downsize and lem:downsize-cl-dist; blueprint
lem:cl-downsize. The CL functions of the pipeline are native to 𝔽_{2^t} (the low-degree
tests, the introspection sampler), while samplers of normal form verifiers are over 𝔽₂
(def:sampler). Downsizing bridges the two: a basis b of a field F over a subfield K
gives the K-linear bijection ↓ : F^ι ≃ K^{ι × κ} reading off coordinates entry by entry
(downsizeEquiv), and L ↦ ↓ ∘ L ∘ ↓⁻¹ carries ℓ-level CL functions on F^ι to ℓ-level CL
functions on K^{ι × κ} — on presentations, CLFun.downsize, whose decomposition data are
the downsized data of the original: register subspaces S become S × κ, stage maps are
conjugated by ↓, and the marginals, factor spaces and stage maps of lem:cl-kth correspond
(eval_truncate_downsize, factorOfPrefix_downsize, mapOfPrefix_downsize). Exactness is
preserved, and the CL distribution is pushed forward along ↓ (clDist_downsize).
The paper states this for admissible field sizes q = 2^t, t odd, with the self-dual
normal basis of blueprint lem:self-dual-basis. Nothing here depends on the choice of basis:
the self-duality matters for the arithmetic of 𝔽_{2^t} to be computable from 𝔽₂-data
by the programs that use it, which is a matter for the efficient-computability toolkit. The
paper's downsized sampler (def:downsize_sampler), a machine wrapping a sampler over
𝔽_{2^t}, has no counterpart: samplers are over 𝔽₂ by definition, and a construction native
to 𝔽_{2^t} is to present the downsized CL functions directly.
The second half of the file is the transport of presentations along a bijection of
coordinates e : ι ≃ ι' (reindexEquiv, CLFun.reindex), with the same list of lemmas; it is
the identification K^{ι × κ} = K^{|ι| · |κ|} the paper leaves implicit, and it is what puts a
downsized presentation on the coordinates Fin (s · t) of a sampler.
The downsize map, and the transport along a bijection of coordinates #
The downsize map of a basis b of F over K, on vectors: F^ι ≃ K^{ι × κ}, sending
v to the coordinates of its entries, ↓v (i, j) = (b.repr (v i)) j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The downsized linear map ↓ ∘ L ∘ ↓⁻¹ of a map on V_S: a map on V_{S × κ} over K.
Equations
- MIPRE.CL.RegLinear.downsize b L = { toLinearMap := ↑(MIPRE.CL.downsizeEquiv b) ∘ₗ ↑K L.toLinearMap ∘ₗ ↑(MIPRE.CL.downsizeEquiv b).symm, proj_comp_proj' := ⋯ }
Instances For
The downsized presentation L^↓ (paper def:cl-downsize): register subspaces S become
S × κ, the linear maps are conjugated by the downsize map, and the continuations are selected
through it.
Equations
- One or more equations did not get rendered due to their size.
- MIPRE.CL.CLFun.downsize b MIPRE.CL.CLFun.zero = MIPRE.CL.CLFun.zero
Instances For
Reindexing coordinates #
A map on V_S, transported along e.
Equations
- MIPRE.CL.RegLinear.reindex e L = { toLinearMap := ↑(MIPRE.CL.reindexEquiv e) ∘ₗ L.toLinearMap ∘ₗ ↑(MIPRE.CL.reindexEquiv e).symm, proj_comp_proj' := ⋯ }
Instances For
A presentation, transported along a bijection of coordinates.
Equations
- One or more equations did not get rendered due to their size.
- MIPRE.CL.CLFun.reindex e MIPRE.CL.CLFun.zero = MIPRE.CL.CLFun.zero
Instances For
Evaluation, and the data of lem:cl-kth #
L^↓ = ↓ ∘ L ∘ ↓⁻¹.
Item 1 of lem:cl-downsize: the marginals of L^↓ are the downsized marginals of L.
Item 2 of lem:cl-downsize, factor spaces: V^↓_{k, ↓u} = V_{k,u} × κ.
Item 2 of lem:cl-downsize, linear maps: L^↓_{k, ↓u} = ↓ ∘ L_{k,u} ∘ ↓⁻¹.
lem:cl-downsize for functions: ↓ ∘ f ∘ ↓⁻¹ is an ℓ-level CL function on V_{T × κ}
over K whenever f is one on V_T over F.
Reindexing, for functions.
lem:downsize-cl-dist: the CL distribution of the downsized functions is the image of the
CL distribution under ↓.