Rational hitting lists: unary arithmetic

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/UnaryArithmetic.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.unaryMulStep_iterate (a : Unary × Unary) (n : ℕ) : (fun (a : Unary × Unary) => (a.1, { val := a.2.val + a.1.val }))^[n] a = (a.1, { val := a.2.val + n * a.1.val })

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryMul : Poly fun (a : Unary × Unary) => { val := a.1.val * a.2.val }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryPow (k : ℕ) : Poly fun (a : Unary) => { val := a.val ^ k }

@[reducible, inline]

abbrev Complexity.RationalHitting.StackLanguage.DivState : Type

Unary division state containing divisor, quotient, and remainder.

Equations

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

def Complexity.RationalHitting.StackLanguage.divStep (a : DivState) : DivState

One unary division step, carrying into the quotient when possible.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.divStep_size (a : DivState) : (code (divStep a)).length ≤ (code a).length + 3

theorem Complexity.RationalHitting.StackLanguage.divStep_iterate_size (a : DivState) (n : ℕ) : (code (divStep^[n] a)).length ≤ (code a).length + 3 * n

theorem Complexity.RationalHitting.StackLanguage.divStep_expected (d n : ℕ) : divStep ({ val := d }, { val := n / d }, { val := n % d }) = ({ val := d }, { val := (n + 1) / d }, { val := (n + 1) % d })

theorem Complexity.RationalHitting.StackLanguage.divStep_iterate (d : Unary) (n : ℕ) : divStep^[n] (d, { val := 0 }, { val := 0 }) = (d, { val := n / d.val }, { val := n % d.val })

theorem Complexity.RationalHitting.StackLanguage.Poly.divStep_poly : Poly divStep

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryDivMod : Poly fun (a : Unary × Unary) => ({ val := a.1.val / a.2.val }, { val := a.1.val % a.2.val })

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryDiv : Poly fun (a : Unary × Unary) => { val := a.1.val / a.2.val }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryMod : Poly fun (a : Unary × Unary) => { val := a.1.val % a.2.val }

def Complexity.RationalHitting.StackLanguage.Procedure.wordLength : Procedure (fun (x : List Bool) => x) unaryCode List.length

Compute raw word length as a unary output.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Poly.bitLength : Poly fun (a : BitWord) => { val := a.val.length }

theorem Complexity.RationalHitting.StackLanguage.Poly.natBitLength : Poly fun (a : ℕ) => { val := a.bits.length }

theorem Complexity.RationalHitting.StackLanguage.Poly.natSize : Poly fun (a : ℕ) => { val := a.size }

def Complexity.RationalHitting.StackLanguage.doubleBelow (t v : ℕ) : ℕ

Double a value while it is at most the given threshold.

Equations

• Complexity.RationalHitting.StackLanguage.doubleBelow t v = if v ≤ t then v + v else v

def Complexity.RationalHitting.StackLanguage.doubleState (a : Unary × Unary) : Unary × Unary

Advance threshold-bounded doubling while preserving the threshold.

Equations

• Complexity.RationalHitting.StackLanguage.doubleState a = (a.1, { val := Complexity.RationalHitting.StackLanguage.doubleBelow a.1.val a.2.val })

theorem Complexity.RationalHitting.StackLanguage.doubleBelow_iterate_bound (t v k : ℕ) : (doubleBelow t)^[k] v ≤ max v (2 * t)

theorem Complexity.RationalHitting.StackLanguage.doubleState_iterate (a : Unary × Unary) (k : ℕ) : doubleState^[k] a = (a.1, { val := (doubleBelow a.1.val)^[k] a.2.val })

theorem Complexity.RationalHitting.StackLanguage.doubleBelow_iterate_pow (t k : ℕ) (hk : k ≤ t.size) : (doubleBelow t)^[k] 1 = 2 ^ k

theorem Complexity.RationalHitting.StackLanguage.nat_size_log {t : ℕ} (ht : 0 < t) : t.size = Nat.log 2 t + 1

theorem Complexity.RationalHitting.StackLanguage.Poly.doubleState_poly : Poly doubleState

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryNextPower : Poly fun (a : Unary) => { val := 2 ^ a.val.size }

theorem Complexity.RationalHitting.StackLanguage.Poly.unaryLogTwo : Poly fun (a : Unary) => { val := Nat.log 2 a.val }