Rational hitting lists: binary binomial

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

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

def Complexity.RationalHitting.StackLanguage.multiplyClean : Program (Fin 8)

Clean multiplication interface used by the finite rising-product loop.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_multiplyClean (s : Store (Fin 8)) (hf : ∀ (k : Fin 8), 2 ≤ ↑k → s k = []) (B : ℕ) (ha : (s 0).length ≤ B) (hb : (s 1).length ≤ B) : ∃ t ≤ 200 * (B + 1) ^ 4, Eval multiplyClean s (Function.update (Function.update s 0 (wordValue (s 0) * wordValue (s 1)).bits) 1 []) t

def Complexity.RationalHitting.StackLanguage.factorMul : Fin 8 ↪ Fin 10

Embed the multiplication registers in the factorial register bank.

Equations

• Complexity.RationalHitting.StackLanguage.factorMul = Fin.castAddEmb 2

def Complexity.RationalHitting.StackLanguage.FactorialScratch (s : Store (Fin 10)) : Prop

The clean scratch registers used by factorial iteration.

Equations

• Complexity.RationalHitting.StackLanguage.FactorialScratch s = ∀ (k : Fin 10), 1 ≤ ↑k → ↑k < 8 → s k = []

theorem Complexity.RationalHitting.StackLanguage.eval_factorMul (s : Store (Fin 10)) (hf : ∀ (k : Fin 10), 2 ≤ ↑k → ↑k < 8 → s k = []) (B : ℕ) (ha : (s 0).length ≤ B) (hb : (s 1).length ≤ B) : ∃ t ≤ 200 * (B + 1) ^ 4, Eval (Program.rename (⇑factorMul) multiplyClean) s (Function.update (Function.update s 0 (wordValue (s 0) * wordValue (s 1)).bits) 1 []) t

def Complexity.RationalHitting.StackLanguage.factorialBody : Program (Fin 10)

One rising-product step: multiply accumulator by the copied current index, advance the binary index, and drop one symbol of the unary loop counter.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_factorialBody (s : Store (Fin 10)) (hf : FactorialScratch s) (B : ℕ) (h0 : (s 0).length ≤ B) (h8 : (s 8).length ≤ B) : ∃ t ≤ 300 * (B + 1) ^ 4, Eval factorialBody s (Function.update (Function.update (Function.update s 0 (wordValue (s 0) * wordValue (s 8)).bits) 8 (incrementWord (s 8))) 9 (s 9).tail) t

theorem Complexity.RationalHitting.StackLanguage.factorial_wordValue_bits (n : ℕ) : wordValue n.bits = n

def Complexity.RationalHitting.StackLanguage.factorialLoop : Program (Fin 10)

Repeat factorial multiplication over the unary counter.

Equations

• Complexity.RationalHitting.StackLanguage.factorialLoop = Complexity.RationalHitting.StackLanguage.Program.loop 9 Complexity.RationalHitting.StackLanguage.factorialBody

theorem Complexity.RationalHitting.StackLanguage.eval_factorialLoop (n L : ℕ) (s : Store (Fin 10)) (hf : FactorialScratch s) (hcan : (wordValue (s 0)).bits = s 0) (hn : (s 9).length = n) (hp : (s 0).length + n * ((s 8).length + n) ≤ L) (hi : (s 8).length + n ≤ L) : ∃ t ≤ n * (300 * (L + 1) ^ 4 + 1) + 1, ∃ (v : Store (Fin 10)), Eval factorialLoop s v t ∧ v 0 = (wordValue (s 0) * (wordValue (s 8)).ascFactorial n).bits ∧ wordValue (v 8) = wordValue (s 8) + n ∧ v 9 = [] ∧ FactorialScratch v ∧ (v 8).length ≤ (s 8).length + n

Rising products, with a unary iteration budget obtained from the input. No scalar factorial operation occurs in this fixed finite program.

theorem Complexity.RationalHitting.StackLanguage.eval_factorial (n : ℕ) (s : Store (Fin 10)) (hf : FactorialScratch s) (h0 : s 0 = [true]) (h8 : s 8 = [true]) (h9 : (s 9).length = n) : ∃ t ≤ n * (300 * (1 + n * (1 + n) + 1) ^ 4 + 1) + 1, ∃ (v : Store (Fin 10)), Eval factorialLoop s v t ∧ v 0 = n.factorial.bits ∧ wordValue (v 8) = n + 1 ∧ v 9 = [] ∧ FactorialScratch v

Ordinary factorial on unary n, including zero, with polynomial bit cost. The two binary registers initially contain 1; no computed value is an input.

theorem Complexity.RationalHitting.StackLanguage.factorial_bits_length (n : ℕ) : n.factorial.bits.length ≤ 1 + n * (n + 1)

def Complexity.RationalHitting.StackLanguage.factorialCore : Program (Fin 10)

Factorial with clean local registers: only the unary counter and output register are changed. This is the binary subroutine for the Taylor binomials.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.eval_factorialCore (s : Store (Fin 10)) (hs : ∀ (k : Fin 10), ↑k < 9 → s k = []) : ∃ t ≤ (s 9).length * (300 * (1 + (s 9).length * (1 + (s 9).length) + 1) ^ 4 + 1) + 2 * (s 9).length + 10, Eval factorialCore s (Function.update (Function.update s 0 (s 9).length.factorial.bits) 9 []) t

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

Cancel one unary digit, recording when the minuend is exhausted.

Equations

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

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

Subtract unary counters while retaining an underflow flag.

Equations

• Complexity.RationalHitting.StackLanguage.unaryDiff a b flag = Complexity.RationalHitting.StackLanguage.Program.loop b (Complexity.RationalHitting.StackLanguage.unaryDiffBody a b flag)

theorem Complexity.RationalHitting.StackLanguage.eval_unaryDiff {K : Type} [DecidableEq K] {a b flag : K} (hab : a ≠ b) (haf : a ≠ flag) (hbf : b ≠ flag) (s : Store K) : Eval (unaryDiff a b flag) s (Function.update (Function.update (Function.update s a (List.drop (s b).length (s a))) b []) flag (List.replicate ((s b).length - (s a).length) true ++ s flag)) (5 * (s b).length + 1)

Variable-length subtraction of unary loop counters. The leftover flag is nonempty exactly when the second counter exceeded the first.

def Complexity.RationalHitting.StackLanguage.Binomial.arith : Fin 10 ↪ Fin 18

Embed the arithmetic register bank in the binomial-coefficient program.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.arith = Fin.castAddEmb 8

def Complexity.RationalHitting.StackLanguage.Binomial.LowEmpty (s : Store (Fin 18)) : Prop

The lower arithmetic registers are all empty.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.LowEmpty s = ∀ (k : Fin 18), ↑k < 10 → s k = []

def Complexity.RationalHitting.StackLanguage.Binomial.factorialCost (n : ℕ) : ℕ

Polynomial bound on the stack steps of factorial computation.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.factorialCost n = n * (300 * (1 + n * (1 + n) + 1) ^ 4 + 1) + 2 * n + 10

def Complexity.RationalHitting.StackLanguage.Binomial.factorBlock (a b : Fin 18) : Program (Fin 18)

Compute one factorial and copy its binary result to the chosen register.

Equations

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

def Complexity.RationalHitting.StackLanguage.Binomial.factorCost (n b : ℕ) : ℕ

Stack-step bound for a factorial block, including copies and cleanup.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.factorCost n b = Complexity.RationalHitting.StackLanguage.Binomial.factorialCost n + 7 * n + 9 * (1 + n * (n + 1)) + 2 * b + 20

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_factorBlock (a b : Fin 18) (ha : 10 ≤ ↑a) (hb : 10 ≤ ↑b) (ha17 : a ≠ 17) (hb17 : b ≠ 17) (s : Store (Fin 18)) (hs : LowEmpty s) (h17 : s 17 = []) : ∃ t ≤ factorCost (s a).length (s b).length, Eval (factorBlock a b) s (Function.update s b (s a).length.factorial.bits) t

def Complexity.RationalHitting.StackLanguage.Binomial.input (n k : ℕ) : Store (Fin 18)

Initial register store containing the two unary binomial arguments.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.input n k = Function.update (Function.update (fun (x : Fin 18) => []) 14 (List.replicate n true)) 15 (List.replicate k true)

def Complexity.RationalHitting.StackLanguage.Binomial.prepared (n k : ℕ) : Store (Fin 18)

The input store extended with both truncated differences of its arguments.

Equations

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

def Complexity.RationalHitting.StackLanguage.Binomial.prepare : Program (Fin 18)

Compute the unary difference and underflow flag for binomial evaluation.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_prepare (n k : ℕ) : Eval prepare (input n k) (prepared n k) (7 * n + 12 * k + 17)

theorem Complexity.RationalHitting.StackLanguage.Binomial.lowEmpty_input (n k : ℕ) : LowEmpty (input n k)

theorem Complexity.RationalHitting.StackLanguage.Binomial.lowEmpty_update (s : Store (Fin 18)) (hs : LowEmpty s) (j : Fin 18) (hj : 10 ≤ ↑j) (w : List Bool) : LowEmpty (Function.update s j w)

theorem Complexity.RationalHitting.StackLanguage.Binomial.lowEmpty_prepared (n k : ℕ) : LowEmpty (prepared n k)