Rational hitting lists: rational binary

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/RationalBinary.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.RationalHitting.StackLanguage.eval_copy9 (s : Store (Fin 12)) (a b : Fin 12) (hab : a ≠ b) (ha : a ≠ 9) (hb : b ≠ 9) (h9 : s 9 = []) : Eval (copy a b 9) s (Function.update s b (s a)) (7 * (s a).length + 2 * (s b).length + 7)

def Complexity.RationalHitting.StackLanguage.fractionReduce : Program (Fin 12)

Euclid followed by two binary divisions, destructively producing the coprime numerator and positive denominator magnitudes.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_fractionReduce (s : Store (Fin 12)) (hs : FractionScratch s) (h10 : s 10 = []) (h11 : s 11 = []) (hcan0 : (wordValue (s 0)).bits = s 0) (hcan5 : (wordValue (s 5)).bits = s 5) (hb : 0 < wordValue (s 5)) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) : ∃ t ≤ 3000 * (B + 1) ^ 3, Eval fractionReduce s (Function.update (Function.update s 0 (wordValue (s 0) / (wordValue (s 0)).gcd (wordValue (s 5))).bits) 5 (wordValue (s 5) / (wordValue (s 0)).gcd (wordValue (s 5))).bits) t

def Complexity.RationalHitting.StackLanguage.unaryLength {K : Type} (a b : K) : Program K

Consume a word, emitting its unary length, independently of its bits.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_unaryLength {K : Type} [DecidableEq K] {a b : K} (hab : a ≠ b) (s : Store K) : Eval (unaryLength a b) s (Function.update (Function.update s a []) b (List.replicate (s a).length true ++ s b)) (4 * (s a).length + 1)

def Complexity.RationalHitting.StackLanguage.encodedWord (w : List Bool) : List Bool

Canonical output's self-delimiting natural-number encoding, applied to an already canonical little-endian binary word.

Equations

• Complexity.RationalHitting.StackLanguage.encodedWord w = List.replicate w.length true ++ [false] ++ w

def Complexity.RationalHitting.StackLanguage.encodeWord : Program (Fin 4)

Write a self-delimiting binary word with its unary length prefix.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_encodeWord (s : Store (Fin 4)) (h2 : s 2 = []) (h3 : s 3 = []) : Eval encodeWord s (Function.update (Function.update s 0 []) 1 (encodedWord (s 0) ++ s 1)) (11 * (s 0).length + 7)

theorem Complexity.RationalHitting.StackLanguage.digits_bool_bits (a : ℕ) : List.map (fun (b : ℕ) => b != 0) (Nat.digits 2 a) = a.bits

theorem Complexity.RationalHitting.RationalCanonical.divInt_num_abs (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).num.natAbs = a.natAbs / a.natAbs.gcd b.natAbs

theorem Complexity.RationalHitting.RationalCanonical.divInt_den (a b : ℤ) (hb : b ≠ 0) : (Rat.divInt a b).den = b.natAbs / a.natAbs.gcd b.natAbs

theorem Complexity.RationalHitting.RationalCanonical.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)

The sign used by the canonical binary rational encoder.

theorem Complexity.RationalHitting.StackLanguage.encodedWord_bits (a : ℕ) : encodedWord a.bits = encodeNat a

theorem Complexity.RationalHitting.StackLanguage.eval_encodeWord_rename {K : Type} [DecidableEq K] (f : Fin 4 → K) (hf : Function.Injective f) (s : Store K) (h2 : s (f 2) = []) (h3 : s (f 3) = []) : Eval (Program.rename f encodeWord) s (Function.update (Function.update s (f 0) []) (f 1) (encodedWord (s (f 0)) ++ s (f 1))) (11 * (s (f 0)).length + 7)

theorem Complexity.RationalHitting.StackLanguage.eval_fractionReduce_rename {K : Type} [DecidableEq K] (f : Fin 12 → K) (hf : Function.Injective f) (s : Store K) (hs : FractionScratch fun (k : Fin 12) => s (f k)) (h10 : s (f 10) = []) (h11 : s (f 11) = []) (A D B : ℕ) (h0 : s (f 0) = A.bits) (h5 : s (f 5) = D.bits) (hD : 0 < D) (ha : A.bits.length ≤ B) (hd : D.bits.length ≤ B) : ∃ t ≤ 3000 * (B + 1) ^ 3, Eval (Program.rename f fractionReduce) s (Function.update (Function.update s (f 0) (A / A.gcd D).bits) (f 5) (D / A.gcd D).bits) t

def Complexity.RationalHitting.StackLanguage.fractionSign : Program (Fin 16)

Registers 12 and 13 hold signed-magnitude signs; 15 stores the canonical result's sign and remains disjoint from the twelve arithmetic registers.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_fractionSign (s : Store (Fin 16)) (a b : Bool) (h12 : s 12 = [a]) (h13 : s 13 = [b]) : ∃ t ≤ 4, Eval fractionSign s (Function.update s 15 ((if s 0 = [] then false else a ^^ b) :: s 15)) t

def Complexity.RationalHitting.StackLanguage.reduceReg (i : Fin 12) : Fin 16

Embed fraction-reduction registers into the rational-encoding program.

Equations

• Complexity.RationalHitting.StackLanguage.reduceReg i = ⟨↑i, ⋯⟩

theorem Complexity.RationalHitting.StackLanguage.reduceReg_inj : Function.Injective reduceReg

def Complexity.RationalHitting.StackLanguage.denominatorReg : Fin 4 → Fin 16

Registers used when emitting the canonical denominator.

Equations

• Complexity.RationalHitting.StackLanguage.denominatorReg = ![5, 14, 1, 2]

def Complexity.RationalHitting.StackLanguage.numeratorReg : Fin 4 → Fin 16

Registers used when emitting the canonical numerator magnitude.

Equations

• Complexity.RationalHitting.StackLanguage.numeratorReg = ![0, 14, 1, 2]

theorem Complexity.RationalHitting.StackLanguage.denominatorReg_inj : Function.Injective denominatorReg

theorem Complexity.RationalHitting.StackLanguage.numeratorReg_inj : Function.Injective numeratorReg

def Complexity.RationalHitting.StackLanguage.rationalEncode : Program (Fin 16)

Full signed canonical rational output. No gcd, comparison or sign oracle occurs in this fixed finite binary-stack program.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.RationalHitting.StackLanguage.eval_rationalEncode (s : Store (Fin 16)) (a b : ℤ) (hb : b ≠ 0) (h0 : s 0 = a.natAbs.bits) (h5 : s 5 = b.natAbs.bits) (h12 : s 12 = [decide (a < 0)]) (h13 : s 13 = [decide (b < 0)]) (h15 : s 15 = []) (hs : ∀ (i : Fin 16), ↑i < 12 → i ≠ 0 → i ≠ 5 → s i = []) (B : ℕ) (ha : a.natAbs.bits.length ≤ B) (hd : b.natAbs.bits.length ≤ B) : ∃ t ≤ 3100 * (B + 1) ^ 3, Eval rationalEncode s (Function.update (Function.update (Function.update s 0 []) 5 []) 14 (encodeRat (Rat.divInt a b) ++ s 14)) t

Exact final canonical binary fraction, with a cubic bit-time stack implementation. This supplies the output-format obligation of the uniform list generator.