Documentation

Complexity.Computability.TreeEval.Reader.Cert.Residue

Residues within linear work space #

The residue operations of Cslib.TreeEval.Reader are computable within work space linear in the lengths of their encoded arguments.

Main results #

Cslib.TreeEval.Reader.addMod_inSpace, .mulMod_inSpace, .negMod_inSpace, .chi_inSpace, .unitInv_inSpace: the residue operations; unitInv p j computes (j + 1) ^ (p - 2) modulo p by repeated multiplication.

theorem Cslib.TreeEval.Reader.addMod_inSpace :

Turing.MultiTapeTM.ComputableInSpace (fun (q : ℕ × ℕ × ℕ) => addMod q.1 q.2.1 q.2.2) Turing.MultiTapeTM.encNat3 Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ × ℕ) => (Turing.MultiTapeTM.encNat3 q).length

The sum modulo p, from (p, a, b).

theorem Cslib.TreeEval.Reader.mulMod_inSpace :

Turing.MultiTapeTM.ComputableInSpace (fun (q : ℕ × ℕ × ℕ) => mulMod q.1 q.2.1 q.2.2) Turing.MultiTapeTM.encNat3 Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ × ℕ) => (Turing.MultiTapeTM.encNat3 q).length

The product modulo p, from (p, a, b).

theorem Cslib.TreeEval.Reader.negMod_inSpace :

Turing.MultiTapeTM.ComputableInSpace (fun (q : ℕ × ℕ) => negMod q.1 q.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) q).length

The negation modulo p, from (p, a).

The residue of x or of 1 - x modulo p, from ((p, x), b).

theorem Cslib.TreeEval.Reader.powMod_le {p a k : ℕ} (hk : k ≤ p - 2) :

powMod p a k ≤ p + 1

theorem Cslib.TreeEval.Reader.unitInv_inSpace :

Turing.MultiTapeTM.ComputableInSpace (fun (q : ℕ × ℕ) => unitInv q.1 q.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encNat fun (q : ℕ × ℕ) => ((Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) q).length

The inverse of the unit of round j, unitInv p j from (p, j).