[proofplan]
The proof uses the formal interpretation stated in the theorem: a complete classification is a bijection between parameter classes and solution classes together with explicit accounting for the reduction and sign conventions used to define those classes. Verification makes the proposed formula land in the solution set, derivation gives surjectivity, and duplicate control gives injectivity. The common-factor and sign-symmetry clauses are not consequences of bare bijectivity alone; they are the extra well-definedness data that ensure the displayed formula and the chosen equivalence relations represent the intended integer classification.
[/proofplan]
[step:Construct the quotient map from the proposed formula]
Assume first that the five stated conditions hold. Define
\begin{align*}
\overline{\Phi}: P/\!\approx &\to S/\!\sim \\
[p]_{\approx} &\mapsto [\Phi(p)]_{\sim}.
\end{align*}
The verification condition gives $\Phi(p) \in S$ for every $p \in P$, so the expression $[\Phi(p)]_{\sim}$ is an element of $S/\!\sim$.
We check that $\overline{\Phi}$ is well-defined. Let $p,q \in P$ satisfy $[p]_{\approx} = [q]_{\approx}$, equivalently $p \approx q$. By the duplicate-parameter condition,
\begin{align*}
p \approx q \implies \Phi(p) \sim \Phi(q).
\end{align*}
Hence $[\Phi(p)]_{\sim} = [\Phi(q)]_{\sim}$, so the value of $\overline{\Phi}$ does not depend on the representative of the parameter class.
By the formal meaning of common-factor treatment in the statement, every divisibility, primitivity, or reduction operation used in defining $\Phi$ is defined for each $p \in P$, produces an integer tuple, and preserves the intended class in $S/\!\sim$. Hence the symbol $\Phi:P\to S$ used above is not merely a formal expression: it is a well-defined map into the intended set of integer solution representatives.
By the formal meaning of sign-symmetry treatment in the statement, every allowed sign change on a displayed solution is recorded either by the solution [equivalence relation](/page/Equivalence%20Relation) $\sim$ or by the parameter equivalence relation $\approx$, and no unrecorded sign identification is imposed. Hence the quotient sets $P/\!\approx$ and $S/\!\sim$ are exactly the quotient sets determined by the problem convention. Therefore the quotient map above is the mathematical object represented by the proposed classification.
[/step]
[step:Use derivation to prove every solution class appears]
Let $[x]_{\sim} \in S/\!\sim$ be an arbitrary solution class, with representative $x \in S$. By the derivation condition, there exists $p \in P$ such that
\begin{align*}
x \sim \Phi(p).
\end{align*}
Therefore
\begin{align*}
[x]_{\sim} = [\Phi(p)]_{\sim} = \overline{\Phi}([p]_{\approx}).
\end{align*}
Since every element of $S/\!\sim$ lies in the image of $\overline{\Phi}$, the map $\overline{\Phi}$ is surjective.
[/step]
[step:Use duplicate control to prove no unrecorded repetitions occur]
Let $[p]_{\approx},[q]_{\approx} \in P/\!\approx$ satisfy
\begin{align*}
\overline{\Phi}([p]_{\approx}) = \overline{\Phi}([q]_{\approx}).
\end{align*}
By the definition of $\overline{\Phi}$, this means
\begin{align*}
[\Phi(p)]_{\sim} = [\Phi(q)]_{\sim},
\end{align*}
equivalently $\Phi(p) \sim \Phi(q)$. The duplicate-parameter condition gives
\begin{align*}
\Phi(p) \sim \Phi(q) \implies p \approx q.
\end{align*}
Thus $[p]_{\approx} = [q]_{\approx}$. Hence $\overline{\Phi}$ is injective.
Together with surjectivity, this proves that $\overline{\Phi}:P/\!\approx \to S/\!\sim$ is a bijection. Therefore the proposed parametric classification is complete, with duplicates recorded exactly by $\approx$.
[/step]
[step:Recover the checklist from a complete classification]
Conversely, suppose the proposed classification is complete with duplicates recorded exactly by $\approx$ in the formal sense stated in the theorem. Thus completeness supplies a well-defined bijection
\begin{align*}
\overline{\Phi}: P/\!\approx &\to S/\!\sim \\
[p]_{\approx} &\mapsto [\Phi(p)]_{\sim},
\end{align*}
and exact duplicate recording means that two parameter choices represent the same solution class exactly when they are $\approx$-equivalent.
First, because $\overline{\Phi}([p]_{\approx})$ is an element of $S/\!\sim$ for every $p \in P$, the representative $\Phi(p)$ must lie in $S$. Hence every displayed tuple is a solution. This is the verification condition.
Second, because $\overline{\Phi}$ is surjective, for every class $[x]_{\sim} \in S/\!\sim$ there exists $p \in P$ such that
\begin{align*}
[x]_{\sim} = \overline{\Phi}([p]_{\approx}) = [\Phi(p)]_{\sim}.
\end{align*}
Equivalently, every solution class is derived from the formula. This is the derivation condition.
Third, the formal definition of completeness used here requires $\Phi$ to be a map from the stated parameter set into the intended integer solution representatives. Therefore every divisibility, primitivity, or reduction step used to define $\Phi$ must be specified, must be defined on the stated parameter domain, must produce an integer tuple, and must preserve the intended class in $S/\!\sim$. This is exactly the common-factor treatment condition.
Fourth, the quotient $S/\!\sim$ is the quotient by the problem's allowed solution symmetries, and $P/\!\approx$ is the quotient by the recorded parameter symmetries. Since the displayed bijection is asserted to classify the intended solution classes with duplicates recorded exactly by $\approx$, every allowed sign change must be represented either by $\sim$ on the solution side or by $\approx$ on the parameter side, and no further sign identification may be used silently. This is the sign-symmetry treatment condition.
Finally, exact duplicate recording gives, for all $p,q \in P$,
\begin{align*}
\Phi(p) \sim \Phi(q) \quad \Longleftrightarrow \quad p \approx q.
\end{align*}
This is the duplicate-parameter condition.
[/step]
[step:Conclude the equivalence between completeness and the checklist]
The first direction shows that the five checklist items produce a well-defined bijection
\begin{align*}
\overline{\Phi}: P/\!\approx \to S/\!\sim.
\end{align*}
Here verification supplies the map into $S$, derivation supplies surjectivity, duplicate control supplies injectivity, and the common-factor and sign-symmetry treatments supply the formal well-definedness data ensuring that $\Phi$, $\sim$, and $\approx$ encode the intended integer representatives and sign conventions. The reverse direction shows that any complete classification in this formal sense necessarily satisfies those same five items. Hence a parametric classification of integer solutions is complete exactly when verification, derivation, common-factor treatment, sign-symmetry treatment, and duplicate-parameter treatment have all been supplied.
[/step]