Margin minimizer in the fitted interior-block cost

Proved

QAlgorithms.Papers.Independent.Intakethird100.P39.fitted_interior_minimizer

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $S\ge4$ be an integer. For integers $k\ge4$ , $m\ge1$ with $km=S$ , define the fitted interior-block cost

C(k,m)=(13k-8)\left((m+2)\frac{215}{100}-\frac{448}{100}\right)+\mathbf1_{m\ne1}(13k+3)\left(m\frac{69}{100}+\frac6{100}\right).

Then the feasible choice $(k,m)=(S,1)$ attains the minimum:

C(S,1)\le C(k,m)\qquad(km=S,\ k\ge4,\ m\ge1).

Here $S=(n-m_1-m_2-1)/2$ in the paper's application. The decimals define an exact rational surrogate for regression-based durations; this is not a theorem about optimal hardware time.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P39

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P39

open scoped BigOperators

/-- PDF p.13, Eq. (35): for fixed S=km>=4, the feasible margin (S,1)
attains the minimum of the fitted cost. This is not optimal hardware time. -/
theorem fitted_interior_minimizer (S : ℕ) (hS : 4 ≤ S) :
    ∀ k m : ℕ, 4 ≤ k → 1 ≤ m → k * m = S →
      fittedInteriorCost S 1 ≤ fittedInteriorCost k m := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P39

Source

Quantum CISC Compilation by Optimal Control and Scalable Assembly of Complex Instruction Sets beyond Two-Qubit Gates, arXiv:0712.3227v2, PDF p. 13, Interior-block minimizer in the fitted timing surrogate, Eq. (35)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $S$ satisfying $S\ge4$ , and every pair of natural numbers $k,m$ satisfying $k\ge4$ , $m\ge1$ , and $km=S$ , the theorem asserts

(13S-8)\frac{197}{100} \le (13k-8)\left((m+2)\frac{215}{100}-\frac{448}{100}\right) +\begin{cases}0&m=1,\\1&m\ne1\end{cases} (13k+3)\left(m\frac{69}{100}+\frac{6}{100}\right).

All arithmetic in this displayed inequality is real arithmetic after converting the natural parameters to real numbers. The left side is the value of the same cost formula at $(S,1)$ . The conclusion is a non-strict inequality over precisely the factorizations satisfying the stated bounds; the allowed case $m=1$ forces $k=S$ and gives equality.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph