Pattern Rule 1: adding a first-row box to a one-row tableau

Proved

QAlgorithms.Papers.Independent.Intake100.P91.rule_1

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $n\ge1$ , and let $a,b$ be nonnegative integers satisfying $a\le n-1$ , $b\le n$ , and $b=a$ or $b=a+1$ . Consider the qubit GT patterns with lower top row $(n-1,0)$ and zero count $a$ , and upper top row $(n,0)$ and zero count $b$ . Let $\alpha(r,s,a;R,S,b)$ denote their real transition coefficient calculated from Louck's product (17)–(18), with the first three arguments specifying the lower pattern. Then

\alpha(n-1,0,a;n,0,b)= \begin{cases} \sqrt{(n-b)/n},&a=b,\\ \sqrt{b/n},&b=a+1. \end{cases}

This computes the coefficient by counting ones or zeroes in the upper tableau. For $n=1$ it gives both vacuum-to-one-qubit amplitudes as $1$ .

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P91

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intake100.P91

open scoped BigOperators

attribute [local instance] Classical.propDecidable

/-- Rule 1, PDF p.12, (19)-(22), proved p.18, (33)-(34).
Includes n=1 and the empty lower tableau. Both branches are positive. -/
theorem rule_1 (n a b : ℕ) (hn : 1 ≤ n) (ha : a ≤ n-1)
    (hb : b ≤ n) (hedge : b = a ∨ b = a+1) :
    qubitLouck (n-1) 0 a n 0 b =
      if a = b then Real.sqrt (((n : ℝ) - b) / (n : ℝ))
      else Real.sqrt ((b : ℝ) / (n : ℝ)) := by sorry

end QAlgorithms.Papers.Independent.Intake100.P91

end

Source

A Multigraph Approach for Performing the Quantum Schur Transform, arXiv:2204.10694v1, PDF p. 12, §4.1, Rule 1, (19)–(22); Appendix A, (33)–(34)

Read-back

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

For all natural numbers $n,a,b$ satisfying $n\ge1$ , $a\le n-1$ , $b\le n$ , and $b=a$ or $b=a+1$ , the product-defined coefficient with lower parameters $(n-1,0,a)$ and upper parameters $(n,0,b)$ , whose explicit value is the left-hand side below, satisfies

\begin{cases} \displaystyle\sqrt{\left|\frac{n-a}{n}\right|},&a=b,\\[2mm] \displaystyle\sqrt{\left|\frac{a+1}{n}\right|},&a\ne b \end{cases} = \begin{cases} \displaystyle\sqrt{\frac{n-b}{n}},&a=b,\\[2mm] \displaystyle\sqrt{\frac{b}{n}},&a\ne b. \end{cases}

The fractions use real arithmetic. The denominator is positive by $n\ge1$ ; the endpoint cases $a=0$ , $a=n-1$ , $b=0$ , and $b=n$ are included whenever the hypotheses hold.

Human review

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

View graph