A polynomial identity and the square root of 2 Inspired by Bill Dubuque and Aaron Meyerowitz' arguments in this question
https://mathoverflow.net/questions/32011/direct-proof-of-irrationality
I calculated the following polynomial identity:
$$m^2[pa^2n+2abm+b^2n]^2=p(am+bn)^4+(m^2-pn^2)(-pa^4m^2+4a^2b^2m^2+4ab^3mn+b^4n^2).$$
(Sage proof)
It follows from this identity that if $gcd(m,n)=1$ and $(m/n)^2=p$ then $p$ is a square.  Indeed, applying Bézout's identity we find $a,b$ with $am+bn=1$, and if moreover $m^2-pn^2 = 0$ then the identity becomes
$$m^2[pa^2n+2abm+b^2n]^2=p.$$
This may or may not be a "direct"/"constructive" proof of the irrationality of $\sqrt{2}$ (which is the subject of discussion in the question I linked).  But I am primarily interested in improving this proof:
Question 1: Is there any simpler such identity?  I guess by "such an identity" I mean an identity of the form
$$
P(a,b,m,n,p)^2=p(am+bn)^{k}+(m^2-pn^2)Q(a,b,m,n,p).
$$ 
and by "simpler" I mean of lower degree or with fewer terms.
Alternatively,
Question 2: Why does the identity work?  How would one come up with it?  
(Obviously I did come up with it myself, via a tortuous path that I won't bother describing here, but I am wondering if there is an elegant way.)
 A: Oops, that was easy.  Brahmagupta's identity:
$$
(pan+bm)^2=p(am+bn)^2+(m^2-pn^2)(b^2-pa^2).
$$
A: The proof in my MO post (better here) essentially uses composition of linear (vs. quadratic) forms when viewed as in your question, i.e. using your notation they are as below:
$\ \ \ \begin{align}\text{Quadratic form}\ \ \ \ \  (pan + bm)^2\! &-\,p(am+bn)^2\!= (m^2-pn^2)(b^2-pa^2)\\[.2em]
\text{Linear form}\ \ \ \ \  \color{#90f}{p^2} an + bm \ \ \,  &-\, p(\color{#c00}{am+bn})\, =\, (\color{#0a0}{m\,-\,pn}\,)\ (b\,-\,pa)\end{align}$
So if reduced $\,\color{#0a0}{p = m/n}\in\Bbb Q,\ \color{#90f}{p^2 = d}\in \Bbb Z\,$ then by Bezout $\,\exists\, a,b\!:\ \color{#c00}{am\!+\!bn = 1}\ $ so above is 
$\qquad\qquad\qquad\qquad\ \ \ \ \ \color{#90f}d\,an + bm\ -\ \,   p(\color{#C00}1)\, =\, (\color{#0a0}0)(\cdots)\ \Rightarrow\ p\in\Bbb Z$
which proves that $\, p = \sqrt d\in \Bbb Q\,\Rightarrow\,\sqrt{d}\in\Bbb Z.\, $  Said more "radically", i.e. using quadratic integers
$\qquad\qquad \color{#0a0}{0 = (m-n\sqrt d)}(b-a\sqrt d) = c - \sqrt d\:\Rightarrow\, \sqrt d = c = dan\!+\!bm\in\Bbb Z$
If memory serves correct, I was inspired to employ that linear form after reading a quadratic form that Dedekind employed (essentially composition of squares). In older times (before ideals, modules and algebraic number theory flourished) it was more common to see results like this expressed in the language of (binary) quadratic forms. Nowadays these arguments are linearized by using ideals and modules, e.g. see this answer for  the correspondence between quadratic forms, ideals and numbers.
In terms of quadratic number rings, the proof shows that if an ideal $I$ contains a number $\,m - n\sqrt d\,$ that is primitive $(\gcd(m,n) = 1),\,$ and $\,n> 1,\,$ then $I$ also contains its $ $ simpler multiple $\ c- \sqrt d,\,$  simpler due to the smaller coef $\,1<n\,$ on $\sqrt d.\,$ Generally this idea reduces the coef to $\,\color{#c00}{\gcd(m,n)},\,$ which is $< n\,$ if $\,n\nmid m\,$ [when $\,n\mid m\,$ it is $\,n(m/n -\sqrt d)\,$]. Such reductions prove useful for various purposes, e.g. in   normal forms for ideals and modules.
As I show in this answer the above linear proof generalizes to higher degree polynomials: it yields a Bezout-based proof of the (monic) Rational Root Test by induction on degree. We can also view those proofs in the form that you seek.
