Direct affine-plane models for the cage

The first variable is the primitive root coordinate and the second variable is the power parameter. Passing through finTwoToIteratedPolynomial makes the defining equations polynomials in the root coordinate with coefficients in the parameter polynomial ring.

theorem BGS.Markoff.finTwoToIteratedPolynomial_map {K : Type u_1} [Field K] {L : Type u_2} [Field L] (phi : K →+* L) (p : MvPolynomial (Fin 2) K) : finTwoToIteratedPolynomial ((MvPolynomial.map phi) p) = Polynomial.map (Polynomial.mapRingHom phi) (finTwoToIteratedPolynomial p)

The two-variable/iterated-polynomial equivalence commutes with extension of scalar fields.

noncomputable def BGS.Markoff.cageDiagonalIteratedPolynomial {K : Type u_1} [Field K] (xi : K) (d : ℕ) : Polynomial (Polynomial K)

The diagonal hyperelliptic model L² = F_ξ(t), written as a polynomial in L over K[t].

Equations

• BGS.Markoff.cageDiagonalIteratedPolynomial xi d = BGS.Markoff.adjoinSquarePolynomial (BGS.Markoff.cagePulledRadicand xi d)

noncomputable def BGS.Markoff.cageOffDiagonalIteratedPolynomial {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : Polynomial (Polynomial K)

The off-diagonal primitive-element model. Its root coordinate is S = L + M; eliminating L and M gives (S² - F_ξ - F_η)² - 4 F_ξ F_η.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.Markoff.cagePulledRadicandSecondCoordinate {K : Type u_1} [Field K] (xi : K) (d : ℕ) : MvPolynomial (Fin 2) K

The pulled radicand placed in the second bivariate coordinate.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.Markoff.finTwoToIteratedPolynomial_cagePulledRadicandSecondCoordinate {K : Type u_1} [Field K] (xi : K) (d : ℕ) : finTwoToIteratedPolynomial (cagePulledRadicandSecondCoordinate xi d) = Polynomial.C (cagePulledRadicand xi d)

noncomputable def BGS.Markoff.cageDiagonalPlanePolynomial {K : Type u_1} [Field K] (xi : K) (d : ℕ) : MvPolynomial (Fin 2) K

The diagonal model as the displayed bivariate polynomial L² - F_ξ(t).

Equations

• BGS.Markoff.cageDiagonalPlanePolynomial xi d = MvPolynomial.X 0 ^ 2 - BGS.Markoff.cagePulledRadicandSecondCoordinate xi d

noncomputable def BGS.Markoff.cageOffDiagonalPlanePolynomial {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : MvPolynomial (Fin 2) K

The off-diagonal model as an honest bivariate polynomial.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.Markoff.finTwoToIteratedPolynomial_cageDiagonalPlanePolynomial {K : Type u_1} [Field K] (xi : K) (d : ℕ) : finTwoToIteratedPolynomial (cageDiagonalPlanePolynomial xi d) = cageDiagonalIteratedPolynomial xi d

@[simp]

theorem BGS.Markoff.finTwoToIteratedPolynomial_cageOffDiagonalPlanePolynomial {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : finTwoToIteratedPolynomial (cageOffDiagonalPlanePolynomial xi eta d) = cageOffDiagonalIteratedPolynomial xi eta d

theorem BGS.Markoff.cageDiagonalIteratedPolynomial_irreducible {K : Type u_1} [Field K] {xi : K} (hxi : xi ≠ 0) (hXi : xi ^ 2 - 4 ≠ 0) {d : ℕ} (hd : 0 < d) (h2 : 2 ≠ 0) (hdegree : ↑(2 * d) ≠ 0) : Irreducible (cageDiagonalIteratedPolynomial xi d)

Gauss's lemma turns nonsquareness of the radicand in K(t) into irreducibility of the diagonal plane equation over K[t].

theorem BGS.Markoff.cageDiagonalPlanePolynomial_irreducible {K : Type u_1} [Field K] {xi : K} (hxi : xi ≠ 0) (hXi : xi ^ 2 - 4 ≠ 0) {d : ℕ} (hd : 0 < d) (h2 : 2 ≠ 0) (hdegree : ↑(2 * d) ≠ 0) : Irreducible (cageDiagonalPlanePolynomial xi d)

Ground-field irreducibility of the diagonal bivariate polynomial.

theorem BGS.Markoff.cageOffDiagonalIteratedPolynomial_irreducible {K : Type u_1} [Field K] {xi eta : K} (hxi : xi ≠ 0) (heta : eta ≠ 0) (hXi : xi ^ 2 - 4 ≠ 0) (hEta : eta ^ 2 - 4 ≠ 0) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) {d : ℕ} (hd : 0 < d) (h2 : 2 ≠ 0) (hdegree : ↑(2 * d) ≠ 0) : Irreducible (cageOffDiagonalIteratedPolynomial xi eta d)

The off-diagonal primitive quartic is irreducible over the parameter polynomial ring. The only geometric input is the proved independence of the three pulled-radicand square classes.

theorem BGS.Markoff.cageOffDiagonalPlanePolynomial_irreducible {K : Type u_1} [Field K] {xi eta : K} (hxi : xi ≠ 0) (heta : eta ≠ 0) (hXi : xi ^ 2 - 4 ≠ 0) (hEta : eta ^ 2 - 4 ≠ 0) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) {d : ℕ} (hd : 0 < d) (h2 : 2 ≠ 0) (hdegree : ↑(2 * d) ≠ 0) : Irreducible (cageOffDiagonalPlanePolynomial xi eta d)

Ground-field irreducibility of the off-diagonal bivariate polynomial.

theorem BGS.Markoff.map_cagePulledRadicand {K : Type u_1} [Field K] {L : Type u_2} [Field L] (phi : K →+* L) (xi : K) (d : ℕ) : Polynomial.map phi (cagePulledRadicand xi d) = cagePulledRadicand (phi xi) d

Scalar extension commutes with the explicit pulled radicand.

theorem BGS.Markoff.cageDiagonalPlanePolynomial_absolutelyIrreducible {K : Type u_1} [Field K] {xi : K} (hxi : xi ≠ 0) (hXi : xi ^ 2 - 4 ≠ 0) {d : ℕ} (hd : 0 < d) (h2 : 2 ≠ 0) (hdegree : ↑(2 * d) ≠ 0) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) (cageDiagonalPlanePolynomial xi d))

The diagonal plane model is absolutely irreducible.

theorem BGS.Markoff.cageOffDiagonalPlanePolynomial_absolutelyIrreducible {K : Type u_1} [Field K] {xi eta : K} (hxi : xi ≠ 0) (heta : eta ≠ 0) (hXi : xi ^ 2 - 4 ≠ 0) (hEta : eta ^ 2 - 4 ≠ 0) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) {d : ℕ} (hd : 0 < d) (h2 : 2 ≠ 0) (hdegree : ↑(2 * d) ≠ 0) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) (cageOffDiagonalPlanePolynomial xi eta d))

The off-diagonal primitive quartic is absolutely irreducible.

theorem BGS.Markoff.cagePulledRadicandSecondCoordinate_degreeOf_first_le {K : Type u_1} [Field K] (xi : K) (d : ℕ) : MvPolynomial.degreeOf 0 (cagePulledRadicandSecondCoordinate xi d) ≤ 0

Coordinate-degree bound for a pulled radicand: it is independent of the root coordinate.

theorem BGS.Markoff.cagePulledRadicandSecondCoordinate_degreeOf_second_le {K : Type u_1} [Field K] (xi : K) (d : ℕ) : MvPolynomial.degreeOf 1 (cagePulledRadicandSecondCoordinate xi d) ≤ 4 * d

Coordinate-degree bound for a pulled radicand in the power parameter.

theorem BGS.Markoff.cageDiagonalPlanePolynomial_hasBidegreeAtMost {K : Type u_1} [Field K] (xi : K) (d : ℕ) : External.HasBidegreeAtMost (cageDiagonalPlanePolynomial xi d) 2 (4 * d)

The diagonal model has bidegree at most (2,4d).

theorem BGS.Markoff.cageOffDiagonalPlanePolynomial_hasBidegreeAtMost {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : External.HasBidegreeAtMost (cageOffDiagonalPlanePolynomial xi eta d) 4 (8 * d)

The primitive off-diagonal quartic has bidegree at most (4,8d).

theorem BGS.Markoff.eval_cagePulledRadicandSecondCoordinate {K : Type u_1} [Field K] (xi : K) (d : ℕ) (root parameter : K) : (MvPolynomial.eval ![root, parameter]) (cagePulledRadicandSecondCoordinate xi d) = Polynomial.eval parameter (cagePulledRadicand xi d)

Evaluation of the embedded radicand is ordinary univariate evaluation in the second coordinate.

theorem BGS.Markoff.eval_cageDiagonalPlanePolynomial_eq_zero_iff {K : Type u_1} [Field K] (xi : K) (d : ℕ) (root parameter : K) : (MvPolynomial.eval ![root, parameter]) (cageDiagonalPlanePolynomial xi d) = 0 ↔ root ^ 2 = Polynomial.eval parameter (cagePulledRadicand xi d)

Zeros of the diagonal plane model are exactly square roots of the pulled radicand.

theorem BGS.Markoff.eval_cageOffDiagonalPlanePolynomial {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) (sumRoot parameter : K) : (MvPolynomial.eval ![sumRoot, parameter]) (cageOffDiagonalPlanePolynomial xi eta d) = (sumRoot ^ 2 - (Polynomial.eval parameter (cagePulledRadicand xi d) + Polynomial.eval parameter (cagePulledRadicand eta d))) ^ 2 - 4 * Polynomial.eval parameter (cagePulledRadicand xi d) * Polynomial.eval parameter (cagePulledRadicand eta d)

Evaluation of the off-diagonal plane model is the primitive quartic in the two scalar radicand values.

theorem BGS.Markoff.primitiveQuarticEquation_iff_exists_rootPair {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {f g sumRoot : K} (hsum : sumRoot ≠ 0) : (sumRoot ^ 2 - (f + g)) ^ 2 - 4 * f * g = 0 ↔ ∃ (firstRoot : K) (secondRoot : K), firstRoot ^ 2 = f ∧ secondRoot ^ 2 = g ∧ firstRoot + secondRoot = sumRoot

Away from the primitive-coordinate boundary S = 0, the quartic equation is equivalent to retaining both quadratic roots. The explicit inverse is L = (S² + f - g)/(2S), M = (S² - f + g)/(2S).

theorem BGS.Markoff.eval_cageOffDiagonalPlanePolynomial_eq_zero_iff_exists_rootPair {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (xi eta : K) (d : ℕ) {sumRoot parameter : K} (hsum : sumRoot ≠ 0) : (MvPolynomial.eval ![sumRoot, parameter]) (cageOffDiagonalPlanePolynomial xi eta d) = 0 ↔ ∃ (firstRoot : K) (secondRoot : K), firstRoot ^ 2 = Polynomial.eval parameter (cagePulledRadicand xi d) ∧ secondRoot ^ 2 = Polynomial.eval parameter (cagePulledRadicand eta d) ∧ firstRoot + secondRoot = sumRoot

The preceding primitive-element equivalence applied to the actual cage plane equation.