Claims

../

2026_09_05_chen: A partial proof claim of 5 September 2026: explicit linear upper bounds in the at-most convention, g(n) at most 12n for every n with a Lean development the author reports kernel-checked, and 2n when max(A) is at least 8n^3.

---