Plain polynomial-time signed integer division and modular reduction

Plain Turing.MultiTapeTM.ComputableInPolyTime certificates, exact-division identities, and sign-magnitude code-length bounds for signed binary integer division and remainder over Turing.MultiTapeTM.encIntBin:

• truncated-toward-zero division and remainder (Int.tdiv, Int.tmod);
• Euclidean division and nonnegative remainder (Int.ediv, Int.emod, and the / and % operators on ℤ);
• power-of-two modular reduction Int.modPowTwo x ℓ = x % 2 ^ ℓ with ℓ in unary Turing.MultiTapeTM.encUnary, used to recover integer counts modulo 2 ^ ℓ in Appendix B.3 of [OAI26c].

All certificates are total (at divisor 0, a / 0 = 0, a.tdiv 0 = 0, a % 0 = a, and a.tmod 0 = a) and build on the binary natural division and modular reduction primitives of PolyTime/Nat/BinaryDiv and PolyTime/Int/BinaryDiv without constructing new Turing machines.

Main definitions

• Int.modPowTwo: least nonnegative residue x % (2 : ℤ) ^ ℓ modulo 2 ^ ℓ.

Main results

• Int.ediv_mul_left_exact, Int.ediv_mul_right_exact: exact Euclidean division of integer multiples (d * q).ediv d = q and (q * d).ediv d = q for d ≠ 0.
• Int.modPowTwo_eq_of_dvd_sub: unique recovery of z ∈ [0, 2 ^ ℓ) from any x with 2 ^ ℓ ∣ x - z.
• Int.size_natAbs_tdiv_le, Int.size_natAbs_ediv_le, Int.size_natAbs_emod_le_of_ne_zero, Int.size_natAbs_modPowTwo_le, Turing.MultiTapeTM.length_encIntBin_tdiv_le, Turing.MultiTapeTM.length_encIntBin_ediv_le, Turing.MultiTapeTM.length_encIntBin_emod_le_of_ne_zero, Turing.MultiTapeTM.length_encIntBin_emod_le_max, Turing.MultiTapeTM.length_encIntBin_modPowTwo_le: binary magnitude and encIntBin code-length bounds.
• Turing.MultiTapeTM.ComputableInPolyTime.intBin_tdiv, .intBin_tmod, .intBin_ediv, .intBin_emod, .intBin_div, .intBin_mod, .intBin_modPowTwo: plain polynomial-time certificates and @[fun_prop] composition rules (.intBin_tdiv', .intBin_tmod', .intBin_ediv', .intBin_emod', .intBin_div', .intBin_mod', .intBin_modPowTwo').

References

• OpenAI, The Exponential Time Hypothesis is False
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

Exact division and power-of-two modular reduction

def Int.modPowTwo (x : ℤ) (ℓ : ℕ) : ℤ

Least nonnegative residue of x modulo 2 ^ ℓ, i.e., x - 2 ^ ℓ * ⌊x / 2 ^ ℓ⌋.

theorem Int.modPowTwo_eq_emod (x : ℤ) (ℓ : ℕ) : x.modPowTwo ℓ = x.emod (2 ^ ℓ)

theorem Int.modPowTwo_eq_sub_mul_ediv (x : ℤ) (ℓ : ℕ) : x.modPowTwo ℓ = x - 2 ^ ℓ * x.ediv (2 ^ ℓ)

theorem Int.modPowTwo_nonneg (x : ℤ) (ℓ : ℕ) : 0 ≤ x.modPowTwo ℓ

theorem Int.modPowTwo_lt (x : ℤ) (ℓ : ℕ) : x.modPowTwo ℓ < 2 ^ ℓ

theorem Int.natAbs_modPowTwo_lt (x : ℤ) (ℓ : ℕ) : (x.modPowTwo ℓ).natAbs < 2 ^ ℓ

theorem Int.modPowTwo_eq_of_dvd_sub {x z : ℤ} {ℓ : ℕ} (hz₀ : 0 ≤ z) (hz₁ : z < 2 ^ ℓ) (hdvd : 2 ^ ℓ ∣ x - z) : x.modPowTwo ℓ = z

If z ∈ [0, 2 ^ ℓ) and 2 ^ ℓ divides x - z, then x.modPowTwo ℓ = z.

theorem Int.ediv_mul_left_exact {d : ℤ} (q : ℤ) (hd : d ≠ 0) : (d * q).ediv d = q

Exact Euclidean division of a left multiple (d * q).ediv d = q for d ≠ 0, stated directly on Int.ediv for rewriting without folding to /.

theorem Int.ediv_mul_right_exact (q : ℤ) {d : ℤ} (hd : d ≠ 0) : (q * d).ediv d = q

Exact Euclidean division of a right multiple (q * d).ediv d = q for d ≠ 0, stated directly on Int.ediv for rewriting without folding to /.

Sign-magnitude reductions and magnitude bounds

theorem Int.natAbs_emod_lt_of_ne_zero (a : ℤ) {b : ℤ} (hb : b ≠ 0) : (a.emod b).natAbs < b.natAbs

theorem Int.size_natAbs_tdiv_le (a b : ℤ) : (a.tdiv b).natAbs.size ≤ a.natAbs.size

theorem Int.size_natAbs_ediv_le (a b : ℤ) : (a.ediv b).natAbs.size ≤ a.natAbs.size

theorem Int.size_natAbs_emod_le_of_ne_zero (a : ℤ) {b : ℤ} (hb : b ≠ 0) : (a.emod b).natAbs.size ≤ b.natAbs.size

theorem Int.size_natAbs_modPowTwo_le (x : ℤ) (ℓ : ℕ) : (x.modPowTwo ℓ).natAbs.size ≤ ℓ

Sign-magnitude encIntBin code-length bounds

theorem Turing.MultiTapeTM.length_encIntBin_tdiv_le (a b : ℤ) : (encIntBin (a.tdiv b)).length ≤ (encIntBin a).length

Truncated integer division never increases the encIntBin code length of the dividend.

theorem Turing.MultiTapeTM.length_encIntBin_ediv_le (a b : ℤ) : (encIntBin (a.ediv b)).length ≤ (encIntBin a).length

Euclidean integer division never increases the encIntBin code length of the dividend.

theorem Turing.MultiTapeTM.length_encIntBin_emod_le_of_ne_zero (a : ℤ) {b : ℤ} (hb : b ≠ 0) : (encIntBin (a.emod b)).length ≤ (encIntBin b).length

For b ≠ 0, the Euclidean remainder a.emod b has encIntBin code length at most (encIntBin b).length.

theorem Turing.MultiTapeTM.length_encIntBin_emod_le_max (a b : ℤ) : (encIntBin (a.emod b)).length ≤ max (encIntBin a).length (encIntBin b).length

Unconditionally on b (including b = 0), (encIntBin (a.emod b)).length ≤ max (encIntBin a).length (encIntBin b).length.

theorem Turing.MultiTapeTM.length_encIntBin_modPowTwo_le (x : ℤ) (ℓ : ℕ) : (encIntBin (x.modPowTwo ℓ)).length ≤ ℓ + 1

Reducing modulo 2 ^ ℓ produces an encIntBin code of length at most ℓ + 1.

Plain polynomial-time certificates

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_tdiv : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1.tdiv p.2) (encPair encIntBin encIntBin) encIntBin

Truncated-toward-zero division of signed binary integers is computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_tdiv' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => (left a).tdiv (right a)) input encIntBin

Truncated-toward-zero division of computed binary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_tmod : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1.tmod p.2) (encPair encIntBin encIntBin) encIntBin

Truncated-toward-zero remainder of signed binary integers is computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_tmod' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => (left a).tmod (right a)) input encIntBin

Truncated-toward-zero remainder of computed binary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_ediv : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1.ediv p.2) (encPair encIntBin encIntBin) encIntBin

Euclidean division (Int.ediv) of signed binary integers is computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_ediv' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => (left a).ediv (right a)) input encIntBin

Euclidean division (Int.ediv) of computed binary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_div : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1 / p.2) (encPair encIntBin encIntBin) encIntBin

Euclidean division (/) of signed binary integers is computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_div' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => left a / right a) input encIntBin

Euclidean division (/) of computed binary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_emod : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1.emod p.2) (encPair encIntBin encIntBin) encIntBin

Euclidean remainder (Int.emod) of signed binary integers is computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_emod' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => (left a).emod (right a)) input encIntBin

Euclidean remainder (Int.emod) of computed binary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_mod : ComputableInPolyTime (fun (p : ℤ × ℤ) => p.1 % p.2) (encPair encIntBin encIntBin) encIntBin

Euclidean remainder (%) of signed binary integers is computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_mod' {α : Type} {input : α ↪ List Bool} {left right : α → ℤ} (hleft : ComputableInPolyTime left input encIntBin) (hright : ComputableInPolyTime right input encIntBin) : ComputableInPolyTime (fun (a : α) => left a % right a) input encIntBin

Euclidean remainder (%) of computed binary integers.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_modPowTwo : ComputableInPolyTime (fun (p : ℤ × ℕ) => p.1.modPowTwo p.2) (encPair encIntBin encUnary) encIntBin

Reduction Int.modPowTwo p.1 p.2 = p.1 % 2 ^ p.2 of a binary integer modulo 2 ^ ℓ (with ℓ in unary) is computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.intBin_modPowTwo' {α : Type} {input : α ↪ List Bool} {value : α → ℤ} {exponent : α → ℕ} (hvalue : ComputableInPolyTime value input encIntBin) (hexponent : ComputableInPolyTime exponent input encUnary) : ComputableInPolyTime (fun (a : α) => (value a).modPowTwo (exponent a)) input encIntBin

Reduction Int.modPowTwo (value a) (exponent a) of a computed binary integer modulo a computed unary power of two.