Holzer's theorem (Theorem 2.5): if the ternary diagonal form $ax^2 + by^2 + cz^2 = 0$ has a nontrivial rational solution (with $a, b, c$ pairwise coprime and squarefree), then it has an integer solution bounded by $x_0^2 \leq |bc|$, $y_0^2 \leq |ac|$, $z_0^2 \leq |ab|$.
A diagonal ternary quadratic form $w_0 x^2 + w_1 y^2 + w_2 z^2$ is isotropic over $\mathbb{Q}$ iff there is a nontrivial rational solution $(x, y, z)$ with $w_0 x^2 + w_1 y^2 + w_2 z^2 = 0$.
Real isotropy for Legendre: the diagonal form $ax^2 + by^2 + cz^2$ has a nontrivial real solution iff $a, b, c$ do not all have the same sign.
Hensel-lifting square root: if $-uv$ is a square mod $w$, and an odd prime $p$ divides $w$ but not $u, v$, then $-uv$ is a square in $\mathbb{Q}_p$.
Unfolding the ternary diagonal quadratic form over $\mathbb{Q}_p$ at the vector $(v_0, v_1, v_2)$ in terms of the underlying multiplication expression.
$p$-adic isotropy at an odd prime $p$ dividing one of $a, b, c$: Legendre's congruence conditions imply isotropy over $\mathbb{Q}_p$.
Axiomatized $2$-adic isotropy when all three coefficients are odd and have mixed signs: under the congruence and coprimality hypotheses, the form is isotropic over $\mathbb{Q}_2$.
Axiomatized $2$-adic isotropy in the Legendre setting: under all of Legendre's hypotheses, the form is isotropic over $\mathbb{Q}_2$.
$2$-adic isotropy in the Legendre setting (wrapper around the axiomatized version).
Full $p$-adic isotropy in the Legendre setting: assuming all of Legendre's congruence and sign hypotheses, the form is isotropic over every $\mathbb{Q}_p$.
Auxiliary necessity lemma: from a nontrivial integer solution to $aP^2 + bQ^2 + cR^2 = 0$ (with $a$ squarefree, $\gcd(a, c) = 1$) one extracts an integer $X$ with $X^2 \equiv -bc \pmod{a}$. Proved by strong induction on $|P| + |Q| + |R|$, descending via prime factors.
Necessity direction of Legendre's theorem: a nontrivial rational solution to $ax^2 + by^2 + cz^2 = 0$ implies the three congruence conditions (clearing denominators reduces to the auxiliary lemma).
Legendre's theorem (Theorem 2.6): for squarefree pairwise coprime integers $a, b, c$ with mixed signs, the equation $ax^2 + by^2 + cz^2 = 0$ has a nontrivial rational solution iff $-bc$ is a square mod $a$, $-ca$ is a square mod $b$, and $-ab$ is a square mod $c$.
In a field $K$ with $\operatorname{char}(K) \neq 2$, the element $2$ is invertible.
Instances For
A quadratic form $Q$ is geometrically irreducible if its associated bilinear form is left-nondegenerate (separating). This makes the associated conic absolutely irreducible.
Instances For
The quadratic form $ax^2 + by^2 + cz^2 + dxy + exz + fyz$ on $K^3$, encoded as the matrix $\begin{pmatrix} a & d/2 & e/2 \\ d/2 & b & f/2 \\ e/2 & f/2 & c \end{pmatrix}$.
Instances For
Theorem 2.1 (diagonalization): any nondegenerate general conic over a field with $\operatorname{char} \neq 2$ is equivalent to a diagonal weighted sum of squares with nonzero (unit) coefficients.
Alias for generalConicQuadForm: the general ternary quadratic form $ax^2 + by^2 + cz^2 + dxy + exz + fyz$.
Instances For
Stereographic projection (forward map): given a base point $(x_0, y_0, z_0)$ on the diagonal conic $aX^2 + bY^2 + cZ^2 = 0$, this maps $(U, V) \in \mathbb{P}^1$ to a point on the conic via a quadratic formula.
Instances For
The stereographic forward map indeed lands on the conic: $a \cdot \varphi_0^2 + b \cdot \varphi_1^2 + c \cdot \varphi_2^2 = 0$.
Composition identity (0-th coordinate): the back-then-forward of $(U, V)$ scales $U$ by the linear factor $2 z_0 (a x_0 U + b y_0 V)$.
Composition identity (1st coordinate): the back-then-forward of $(U, V)$ scales $V$ by the same linear factor $2 z_0 (a x_0 U + b y_0 V)$.
Composition identity (forward-then-backward, 0-th coordinate): the forward image of the backward projection of a point $(x, y, z)$ on the conic returns $x$ scaled by the bilinear pairing factor.
Composition identity (forward-then-backward, 1st coordinate): analogous to the 0-th coordinate version, scaling $y$ by the same factor.
Quadratic homogeneity: scaling the input $(U, V)$ by $t$ scales the stereographic forward map by $t^2$ (so it descends to projective space).
The bilinear pairing $\langle (x_0, y_0, z_0), (x, y, z) \rangle = a x_0 x + b y_0 y + c z_0 z$ associated to the diagonal conic; encodes the polarization of the quadratic form.
Instances For
Auxiliary: if both $au^2 + bv^2 = 0$ and a related polynomial vanish (with the standard nondegeneracy hypotheses), then $u = 0$. Used in bilinScalar_zero_iff_proportional.
Tangent line criterion: a nonzero point $(x, y, z)$ on the diagonal conic with $\langle p_0, p \rangle = 0$ (i.e., on the tangent line at $p_0$) must be proportional to $p_0 = (x_0, y_0, z_0)$.
Packaged isomorphism data for Theorem 2.3: the stereographic forward map lands on the conic, the back-then-forward and forward-then-backward maps are scalar multiples of the identity, and the tangent line through the base point intersects the conic only at the base point. Together these say the stereographic projection induces a bijection $\mathbb{P}^1 \cong $ conic.
The stereographic forward map sends any nonzero $(U, V)$ to a nonzero point of $K^3$. This is needed to descend the map to projective space.
The diagonal conic as a subset of $\mathbb{P}^2(K)$: the projective points $[x : y : z]$ satisfying $ax^2 + by^2 + cz^2 = 0$.
Instances For
The projectivized stereographic forward map $\mathbb{P}^1(K) \to \mathbb{P}^2(K)$ induced by stereoForward, using the quadratic homogeneity to descend to projective space.
Instances For
The diagonal quadratic form $a X^2 + b Y^2 + c Z^2$ vanishes at the chosen representative of $[v] \in \mathbb{P}^2$ iff it vanishes at $v$ itself; this lets us pass between affine and projective conditions.
The projectivized stereographic forward map lands on the diagonal conic: for every $Q \in \mathbb{P}^1$, the image $\varphi(Q)$ lies in DiagConicSet.
Theorem 2.3 (bijective form): a smooth diagonal conic with a rational base point $(x_0, y_0, z_0)$ admits a bijection $\mathbb{P}^1(K) \to \mathrm{Conic}$ given by stereographic projection.
Theorem 2.3 (equivalence form): the diagonal conic variety with a rational base point is in bijection with $\mathbb{P}^1$ — packaged as an Equiv (the bijection from conic_isomorphic_to_P1 upgraded to an isomorphism of sets).