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. Combining binary integer operations with binary_div, binary_gcd, and canonical component expansions of Rat.divInt (Complexity.Foundations.Data.Rat.Basic) then expands encodeRat (Rat.divInt a b) (encodeRat_divInt) and 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.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.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.