[proofplan] Starting from any positive definite BQF $(a, b, c)$, we describe a reduction algorithm using only the two elementary generators $S = \bigl(\begin{smallmatrix} 0 & -1 \\ 1 & 0 \end{smallmatrix}\bigr)$ and $T_\pm = \bigl(\begin{smallmatrix} 1 & 0 \\ \pm 1 & 1 \end{smallmatrix}\bigr)$ of $\mathrm{SL}_2(\mathbb{Z})$. The substitution $S$ swaps $a$ and $c$ (with a sign flip on $b$); the substitution $T_\pm$ shifts $b \mapsto b \pm 2a$ without changing $a$. The argument has three parts: (1) if $a > c$, apply $S$ to strictly decrease $a$; (2) if $a \leq c$ and $|b| > a$, apply one of $T_\pm$ to strictly decrease $|b|$; (3) after finitely many steps the strict monovariant $a + |b|$ forces $|b| \leq a \leq c$. A final tidy-up handles the two boundary cases where the form lands on the boundary of the reduced region but is not strictly reduced: $b = -a$ with $a < c$, and $b < 0$ with $a = c$. The positive definiteness hypothesis is used implicitly to ensure $a, c > 0$ throughout, so that "decrease $a$" is meaningful. [/proofplan]

[step:Record how $S$ and $T_\pm$ act on a BQF, and fix the positive definite hypothesis]Let $f = (a, b, c)$ be a positive definite BQF. By the [Discriminant Determines Definiteness](/theorems/1728) theorem (positive-definite case), we have $d := b^2 - 4ac < 0$ and $a > 0$; moreover $c = f(0, 1) > 0$. So throughout the algorithm, both $a$ and $c$ are strictly positive integers. The two generators act on BQFs as follows (with $f \sim Af$ for $A \in \mathrm{SL}_2(\mathbb{Z})$): \begin{align*} S: (a, b, c) &\longmapsto (c, -b, a), \\ T_+: (a, b, c) &\longmapsto (a, b + 2a, a + b + c), \\ T_-: (a, b, c) &\longmapsto (a, b - 2a, a - b + c). \end{align*} Both $S$ and $T_\pm$ lie in $\mathrm{SL}_2(\mathbb{Z})$, so the forms produced are equivalent to $f$, and positive definiteness is preserved (equivalent forms have the same discriminant by [Discriminant is an Invariant](/theorems/1726), and the same set of represented values, in particular the same sign behaviour).[/step]

[guided]We assemble the building blocks of the reduction procedure. The form $f = (a, b, c) = ax^2 + bxy + cy^2$ is positive definite, so by the [Discriminant Determines Definiteness](/theorems/1728) theorem we have $d = b^2 - 4ac < 0$ and the leading coefficient satisfies $a > 0$. The final coefficient satisfies $c = f(0, 1) > 0$ because $(0, 1) \neq (0, 0)$ and $f$ is strictly positive on nonzero vectors. Hence at every moment during the algorithm, $a$ and $c$ are positive integers and the comparison $a > c$ or $a \leq c$ is well-defined. The two generators have explicit actions on the coefficients: \begin{align*} S: (a, b, c) &\longmapsto (c, -b, a), \\ T_\lambda: (a, b, c) &\longmapsto (a, b + 2\lambda a, \lambda^2 a + \lambda b + c) \quad \text{for } \lambda \in \mathbb{Z}. \end{align*} The case $\lambda = \pm 1$ gives $T_\pm$. Geometrically $S$ corresponds to the substitution $(x, y) \mapsto (y, -x)$ (swapping the roles of the variables), and $T_\lambda$ to $(x, y) \mapsto (x + \lambda y, y)$ (a shear). Both lie in $\mathrm{SL}_2(\mathbb{Z})$, so the images are equivalent to $f$. Positive definiteness is preserved: by [Discriminant is an Invariant](/theorems/1726) the discriminant is unchanged (still negative), and the leading coefficient remains positive (it becomes $c > 0$ after $S$; it is unchanged by $T_\lambda$).[/guided]

[step:If $a > c$, apply $S$ to strictly decrease the leading coefficient] Suppose $a > c$. The substitution $S$ sends $(a, b, c) \mapsto (c, -b, a)$. The new leading coefficient is $c$, and $c < a$ by hypothesis. So $S$ replaces the leading coefficient $a$ by the strictly smaller positive integer $c$. In particular $a + |b|$ is bounded below by $1$ (since both $a \geq 1$ and $|b| \geq 0$), so repeating $S$ cannot loop forever without violating this bound — which is made precise in the termination step. [/step]

[step:If $a \leq c$ and $|b| > a$, apply $T_+$ or $T_-$ to strictly decrease $|b|$]Suppose $a \leq c$ and $|b| > a$. The substitution $T_\lambda: (a, b, c) \mapsto (a, b + 2\lambda a, \lambda^2 a + \lambda b + c)$ leaves $a$ unchanged and shifts $b$ by $2\lambda a$. We claim we can choose $\lambda \in \{+1, -1\}$ so that $|b + 2\lambda a| < |b|$. Write $b = 2aq + r$ by division with remainder, with $q \in \mathbb{Z}$ and $-a < r \leq a$; equivalently, choose the integer $q$ nearest to $b/(2a)$, preferring the upper value on a tie. Then $|r| \leq a < |b|$, so $r$ is a strictly smaller replacement for $b$ than $b$ itself. However, the generators $T_\pm$ only shift by $\pm 2a$ in one step; to produce the residue $r$ we iterate. It suffices to show that a single application of $T_{\operatorname{sgn}(-b)}$ decreases $|b|$ whenever $|b| > a$, which implies termination by induction. If $b > a$, then $b - 2a < b$ and $|b - 2a| = |b| - 2a$ if $b \geq 2a$, or $2a - b < b$ if $a < b < 2a$; in either case $|b - 2a| < b = |b|$. So applying $T_-$ yields $|b'| = |b - 2a| < |b|$. If $b < -a$, then $b + 2a > b$, and a symmetric analysis gives $|b + 2a| < |b|$, so $T_+$ strictly decreases $|b|$. In both cases, applying the correct one of $T_\pm$ decreases $|b|$ by at least $1$ (since both quantities are integers), while leaving $a$ unchanged.[/step]

[guided]The issue is that $T_+$ and $T_-$ shift $b$ by exactly $\pm 2a$, so a single application might not bring $|b|$ below $a$ if $|b|$ is much larger than $a$. But it does bring $|b|$ strictly closer to $0$, and that is enough for termination. Concretely, assume $|b| > a$, so $b$ is outside the interval $[-a, a]$. Consider two cases by sign: - **Case $b > a$**: apply $T_-$, sending $b \mapsto b - 2a$. Two sub-cases: - If $b \geq 2a$, then $b - 2a \geq 0$, so $|b - 2a| = b - 2a < b = |b|$ (strict inequality because $2a \geq 2 > 0$). - If $a < b < 2a$, then $b - 2a \in (-a, 0)$, so $|b - 2a| = 2a - b < a < b = |b|$. In either sub-case $|b - 2a| < |b|$. - **Case $b < -a$**: apply $T_+$, sending $b \mapsto b + 2a$. Analogously, either $b + 2a \leq 0$ and $|b + 2a| = -b - 2a < -b = |b|$, or $b + 2a \in (0, a)$ and $|b + 2a| = b + 2a < -b = |b|$. So the correct one of $T_\pm$ — chosen as $T_{-\operatorname{sgn}(b)}$ — strictly decreases $|b|$ by at least $1$ (the quantities are integers). Crucially $T_\pm$ does **not** touch $a$, so the bound $a \leq c$ from the hypothesis is preserved throughout any sequence of $T_\pm$ moves. Iterating $T_{-\operatorname{sgn}(b)}$ drives $b$ into the interval $[-a, a]$, at which point the condition $|b| \leq a$ holds and we exit this phase.[/guided]

[step:Combine the two moves using the strict monovariant $a + |b|$ to prove termination] We define the monovariant \begin{align*} \Phi: \{\text{positive definite BQFs}\} &\to \mathbb{Z}_{\geq 0} \\ (a, b, c) &\mapsto a + |b|. \end{align*} Note $\Phi \geq 0$ (since $a \geq 1$ and $|b| \geq 0$). We claim each non-trivial move strictly decreases $\Phi$. - If $a > c$, applying $S$ replaces $(a, b, c)$ by $(c, -b, a)$. The new monovariant is $c + |-b| = c + |b|$. Since $c < a$, we have $c + |b| < a + |b|$, i.e. $\Phi$ drops by at least $1$. - If $a \leq c$ and $|b| > a$, applying the correct $T_\pm$ produces $(a, b', a \pm b + c)$ with $|b'| < |b|$ (by the previous step). The new monovariant is $a + |b'| < a + |b|$, i.e. $\Phi$ drops by at least $1$. So whenever the form fails to satisfy both $a \leq c$ and $|b| \leq a$, one of the two moves applies and decreases $\Phi$ by at least $1$. Since $\Phi$ takes values in $\mathbb{Z}_{\geq 0}$, the algorithm terminates after at most $\Phi(a, b, c)$ steps. At termination both $a \leq c$ and $|b| \leq a$ hold simultaneously. [/step]

[step:Promote $|b| \leq a \leq c$ to the strict reduced conditions on the boundary]The algorithm produces $(a, b, c)$ with $|b| \leq a \leq c$. Recall that a BQF is **reduced** if \begin{align*} -a < b \leq a < c \qquad \text{or} \qquad 0 \leq b \leq a = c. \end{align*} Two boundary cases may still fail to be reduced: **Case $a < c$ and $b = -a$.** The form $(a, -a, c)$ satisfies $|b| = a$ but the first reduced condition requires $-a < b$, i.e. $b > -a$. Apply $T_+$: \begin{align*} T_+: (a, -a, c) \longmapsto (a, -a + 2a, a + (-a) + c) = (a, a, c). \end{align*} The image $(a, a, c)$ satisfies $-a < b = a \leq a < c$, so it is reduced. **Case $a = c$ and $-a \leq b < 0$.** The second reduced condition requires $b \geq 0$. Apply $S$: \begin{align*} S: (a, b, a) \longmapsto (a, -b, a). \end{align*} The image has $b' = -b > 0$, and $|b'| = |b| \leq a$, so $0 < b' \leq a = a$, and the second reduced condition $0 \leq b' \leq a = c$ holds. The form is reduced. In all other cases — i.e. $|b| \leq a < c$ with $b \neq -a$, or $a = c$ with $b \geq 0$ — the output already satisfies the reduced conditions. This exhausts the boundary scenarios.[/step]

[guided]After the main algorithm terminates we have $|b| \leq a \leq c$, but the definition of "reduced" is slightly stricter on the boundary. Specifically: - The first reduced condition $-a < b \leq a < c$ excludes $b = -a$ (it uses the strict inequality $-a < b$), and it requires $a < c$ rather than $a \leq c$. - The second condition $0 \leq b \leq a = c$ applies only when $a = c$, and it requires $b \geq 0$. So the output $(a, b, c)$ with $|b| \leq a \leq c$ might fall into one of two "bad" zones: - **$a < c$ and $b = -a$**: we are on the wrong edge of the first condition. Apply $T_+$: $(a, -a, c) \mapsto (a, -a + 2a, a + (-a) + c) = (a, a, c)$. The new form has $b = a$, which satisfies $-a < b \leq a$ (since $a > 0$), and $a < c$ is unchanged. So $(a, a, c)$ is reduced. - **$a = c$ and $b < 0$**: we need $b \geq 0$ for the second condition. Apply $S$: $(a, b, a) \mapsto (a, -b, a)$. The new $b' = -b > 0$ still satisfies $|b'| = |b| \leq a$, so $0 < b' \leq a = c$ and the form is reduced. The remaining output scenarios — $|b| \leq a < c$ with $b \neq -a$, or $a = c$ with $b \geq 0$ — are already reduced, so no further move is needed. Importantly, neither of the two tidy-up moves re-triggers the main algorithm: $T_+$ on $(a, -a, c)$ produces $(a, a, c)$ which has $a < c$ and $|b| = a$ (not strictly greater), so the main algorithm would immediately terminate; $S$ on $(a, b, a)$ produces $(a, -b, a)$ which has $a = c$ (not $a > c$) and $|b'| = |b| \leq a$. So applying these moves once yields a genuinely reduced output.[/guided]

[step:Conclude that every positive definite BQF is equivalent to a reduced BQF] Given any positive definite BQF $(a, b, c)$, the algorithm produces, in finitely many steps, an equivalent form satisfying $|b| \leq a \leq c$ (by the monovariant argument), and the subsequent tidy-up produces an equivalent form satisfying the full reduced conditions. Each move in the algorithm and in the tidy-up is a generator of $\mathrm{SL}_2(\mathbb{Z})$, so the final output is in the $\mathrm{SL}_2(\mathbb{Z})$-orbit of $(a, b, c)$, i.e. equivalent to it. This completes the proof that every positive definite BQF is equivalent to a reduced BQF. [/step]