Documentation

LeanPool.ACMax.Reduction.GapReduction

Numerical specialization of the linear large-order bound #

boundLin_sharp2_value evaluates the bound from Counting.LargeN.acmax_conjecture_large_n_sharp2 to 17692. The complete all-order theorem is assembled separately in Band.Final.

theorem ACMax.boundLin_sharp2_value :
boundLin ((128 * 306 + 34508) / 23) = 17692

The doubly-sharpened large-n threshold (acmax_conjecture_large_n_sharp2, Counting.WallSharp, mid-leaf bound 108 ⟹ usable cap C_m ≤ 306) evaluates to 17 692 — the current finite frontier.