Polynomial-time canonical binary encodings of naturals and rationals

This module bridges the self-delimiting binary encodings Cslib.Circuits.Rational.encodeNat and Cslib.Circuits.Rational.encodeRat from Complexity/Computability/Circuit/Rational/Defs.lean to the fun_prop polynomial-time calculus over Turing.MultiTapeTM.encNat and Turing.MultiTapeTM.encIntBin.

First, encodeNat a is shown to equal List.replicate a.bits.length true ++ false :: a.bits (encodeNat_eq), yielding a polynomial-time certificate encodeNat_polytime. Next, the reduced numerator magnitude, denominator, and sign bit of Rat.divInt a b are expressed in terms of a.natAbs, b.natAbs, and Nat.gcd a.natAbs b.natAbs (divInt_num_abs, divInt_den, divInt_sign, and encodeRat_divInt). Combining binary integer operations with binary_div and binary_gcd then certifies (p, q) ↦ encodeRat (Rat.divInt p q) on binary integer pairs (encodeDivInt_polytime).

Main results

• Cslib.Circuits.Rational.digits_two_map_bne_zero: (Nat.digits 2 a).map (· != 0) = a.bits.
• Cslib.Circuits.Rational.encodeNat_eq: encodeNat a in terms of a.bits.
• Cslib.Circuits.Rational.encodeNat_polytime, .encodeNat_polytime': polynomial-time certificates for encodeNat.
• Cslib.Circuits.Rational.divInt_num_abs, .divInt_den, .divInt_sign: reduced components of Rat.divInt a b via Nat.gcd a.natAbs b.natAbs.
• Cslib.Circuits.Rational.encodeRat_divInt: unconditional expansion of encodeRat (Rat.divInt a b).
• Cslib.Circuits.Rational.encodeDivInt_polytime, .encodeDivInt_polytime': polynomial-time certificates for (p, q) ↦ encodeRat (Rat.divInt p q).

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/RationalBinary.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.Circuits.Rational.digits_two_map_bne_zero (a : ℕ) : List.map (fun (b : ℕ) => b != 0) (Nat.digits 2 a) = a.bits

Mapping · != 0 over the base-2 digits of a recovers a.bits.

theorem Cslib.Circuits.Rational.encodeNat_eq (a : ℕ) : encodeNat a = List.replicate a.bits.length true ++ false :: a.bits

encodeNat a is the unary length of a.bits, a false delimiter, and a.bits.

theorem Cslib.Circuits.Rational.encodeNat_polytime : Turing.MultiTapeTM.ComputableInPolyTime encodeNat Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBits

Self-delimiting binary encoding of a binary natural is computable in polynomial time.

theorem Cslib.Circuits.Rational.encodeNat_polytime' {α : Type} {input : α ↪ List Bool} {f : α → ℕ} (hf : Turing.MultiTapeTM.ComputableInPolyTime f input Turing.MultiTapeTM.encNat) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => encodeNat (f a)) input Turing.MultiTapeTM.encBits

Self-delimiting binary encoding of a computed binary natural.

theorem Cslib.Circuits.Rational.divInt_num_abs (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs = a.natAbs / a.natAbs.gcd b.natAbs

Reduced numerator magnitude of Rat.divInt a b for b ≠ 0.

theorem Cslib.Circuits.Rational.divInt_den (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den = b.natAbs / a.natAbs.gcd b.natAbs

Reduced denominator of Rat.divInt a b for b ≠ 0.

theorem Cslib.Circuits.Rational.divInt_sign (a b : ℤ) (hb : b ≠ 0) : decide ((Rat.divInt a b).num < 0) = if a = 0 then false else decide (a < 0) ^^ decide (b < 0)

Sign bit of Rat.divInt a b for b ≠ 0.

theorem Cslib.Circuits.Rational.divInt_num_abs_eq (a b : ℤ) : (Rat.divInt a b).num.natAbs = if b = 0 then 0 else a.natAbs / a.natAbs.gcd b.natAbs

Reduced numerator magnitude of Rat.divInt a b for arbitrary integers a, b.

theorem Cslib.Circuits.Rational.divInt_den_eq (a b : ℤ) : (Rat.divInt a b).den = if b = 0 then 1 else b.natAbs / a.natAbs.gcd b.natAbs

Reduced denominator of Rat.divInt a b for arbitrary integers a, b.

theorem Cslib.Circuits.Rational.divInt_sign_eq (a b : ℤ) : decide ((Rat.divInt a b).num < 0) = if a = 0 then false else if b = 0 then false else decide (a < 0) ^^ decide (b < 0)

Sign bit of Rat.divInt a b for arbitrary integers a, b.

theorem Cslib.Circuits.Rational.encodeRat_divInt (a b : ℤ) : encodeRat (Rat.divInt a b) = (if a = 0 then false else if b = 0 then false else decide (a < 0) ^^ decide (b < 0)) :: (encodeNat (if b = 0 then 0 else a.natAbs / a.natAbs.gcd b.natAbs) ++ encodeNat (if b = 0 then 1 else b.natAbs / a.natAbs.gcd b.natAbs))

Explicit expansion of encodeRat (Rat.divInt a b) in terms of integer magnitudes and Nat.gcd.

theorem Cslib.Circuits.Rational.encodeDivInt_polytime : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℤ × ℤ) => encodeRat (Rat.divInt p.1 p.2)) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encIntBin Turing.MultiTapeTM.encIntBin) Turing.MultiTapeTM.encBits

Encoding the reduced rational quotient Rat.divInt p.1 p.2 of two binary integers is computable in polynomial time.

theorem Cslib.Circuits.Rational.encodeDivInt_polytime' {α : Type} {input : α ↪ List Bool} {num den : α → ℤ} (hnum : Turing.MultiTapeTM.ComputableInPolyTime num input Turing.MultiTapeTM.encIntBin) (hden : Turing.MultiTapeTM.ComputableInPolyTime den input Turing.MultiTapeTM.encIntBin) : Turing.MultiTapeTM.ComputableInPolyTime (fun (a : α) => encodeRat (Rat.divInt (num a) (den a))) input Turing.MultiTapeTM.encBits

Encode the reduced rational quotient of two computed binary integers.