Rational hitting lists: binomial bounds

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/BinomialBounds.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.Binomial.allFactors : Program (Fin 18)

Compute the three factorials in the binomial formula.

Equations

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

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

The register store containing the three computed factorials.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_allFactors (n k : ℕ) : ∃ t ≤ factorCost n 0 + factorCost k 0 + factorCost (n - k) 0 + 2, Eval allFactors (prepared n k) (factored n k) t

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

Binary multiplication embedded in the binomial register bank.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_cleanMul (s : Store (Fin 18)) (hs : ∀ (j : Fin 18), 2 ≤ ↑j → ↑j < 8 → s j = []) (B : ℕ) (h0 : (s 0).length ≤ B) (h1 : (s 1).length ≤ B) : ∃ t ≤ 200 * (B + 1) ^ 4, Eval cleanMul s (Function.update (Function.update s 0 (wordValue (s 0) * wordValue (s 1)).bits) 1 []) t

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_cleanQuotient (s : Store (Fin 18)) (hs : GcdScratch fun (j : Fin 10) => s (arith j)) (hd : 0 < wordValue (s 5)) (B : ℕ) (h0 : (s 0).length ≤ B) (h5 : (s 5).length ≤ B) : ∃ t ≤ 400 * (B + 1) ^ 2, Eval (Program.rename (⇑arith) quotient) s (Function.update s 0 (wordValue (s 0) / wordValue (s 5)).bits) t

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_copy_clean {a b : Fin 18} (hab : a ≠ b) (ha : a ≠ 17) (hb : b ≠ 17) (s : Store (Fin 18)) (h17 : s 17 = []) : Eval (copy a b 17) s (Function.update s b (s a)) (7 * (s a).length + 2 * (s b).length + 7)

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

Form the factorial quotient giving the binomial coefficient.

Equations

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

def Complexity.RationalHitting.StackLanguage.Binomial.width (n k : ℕ) : ℕ

A bound on the combined binary widths of the three factorials.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.width n k = 1 + n * (n + 1) + (1 + k * (k + 1)) + (1 + (n - k) * (n - k + 1))

def Complexity.RationalHitting.StackLanguage.Binomial.ratioCost (n k : ℕ) : ℕ

Polynomial stack-step bound for the factorial quotient.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_ratio (n k : ℕ) (hk : k ≤ n) : ∃ t ≤ ratioCost n k, Eval ratio (factored n k) (Function.update (input n k) 0 (n.choose k).bits) t

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

Compute the factorials and their quotient.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.compute = Complexity.RationalHitting.StackLanguage.Binomial.allFactors.seq Complexity.RationalHitting.StackLanguage.Binomial.ratio

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

Clear the difference and underflow registers in the zero-result case.

Equations

• Complexity.RationalHitting.StackLanguage.Binomial.discard = (Complexity.RationalHitting.StackLanguage.clear 12).seq (Complexity.RationalHitting.StackLanguage.clear 13)

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

Compute a binomial coefficient, including the out-of-range zero case.

Equations

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

def Complexity.RationalHitting.StackLanguage.Binomial.cost (n k : ℕ) : ℕ

Polynomial stack-step bound for the complete binomial program.

Equations

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

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_choose (n k : ℕ) : ∃ t ≤ cost n k, Eval choose (input n k) (Function.update (input n k) 0 (n.choose k).bits) t

A single finite program for every binomial coefficient; the inputs are unary counters, not a factorial oracle. The out-of-range case is tested by the actual stack guard.

theorem Complexity.RationalHitting.StackLanguage.Binomial.factorCost_bound (j R : ℕ) (hR : 1 ≤ R) (hj : j ≤ R) : factorCost j 0 ≤ 77000 * R ^ 10

theorem Complexity.RationalHitting.StackLanguage.Binomial.width_bound (n k R : ℕ) (hR : 1 ≤ R) (hn : n ≤ R) (hk : k ≤ R) : width n k ≤ 9 * R ^ 2

theorem Complexity.RationalHitting.StackLanguage.Binomial.cost_bound (n k : ℕ) : cost n k ≤ 3000000 * (n + k + 1) ^ 10

theorem Complexity.RationalHitting.StackLanguage.Binomial.eval_choose_polynomial (n k : ℕ) : ∃ t ≤ 3000000 * (n + k + 1) ^ 10, Eval choose (input n k) (Function.update (input n k) 0 (n.choose k).bits) t

The exact binary binomial coefficient with a fixed polynomial bound in the unary input length.