Pulled-back cage radicands

After writing the common normalized trace as t^d + t⁻ᵈ and multiplying an incidence root by t^d, the retained quadratic equation becomes

L² = (ξ² - 4) (t^(2d) + 1)² - 4 ξ² t^(2d).

This file proves the square-class facts needed for the direct affine-plane Hasse--Weil model. In particular, the off-diagonal argument is not hidden behind a geometric-integrality assumption: the two pulled radicands are proved squarefree and coprime explicitly.

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

The radicand obtained after pulling an incidence conic back along the power-trace parameter t ↦ t^d + t⁻ᵈ and clearing t⁻ᵈ.

Equations

• BGS.Markoff.cagePulledRadicand xi d = Polynomial.C (xi ^ 2 - 4) * (Polynomial.X ^ (2 * d) + 1) ^ 2 - Polynomial.C (4 * xi ^ 2) * Polynomial.X ^ (2 * d)

@[simp]

theorem BGS.Markoff.cagePulledRadicand_eval_zero {K : Type u_1} [Field K] (xi : K) {d : ℕ} (hd : 0 < d) : Polynomial.eval 0 (cagePulledRadicand xi d) = xi ^ 2 - 4

@[simp]

theorem BGS.Markoff.cagePulledRadicand_eval_one {K : Type u_1} [Field K] (xi : K) (d : ℕ) : Polynomial.eval 1 (cagePulledRadicand xi d) = -16

theorem BGS.Markoff.cagePulledRadicand_sub {K : Type u_1} [Field K] (xi eta : K) (d : ℕ) : cagePulledRadicand xi d - cagePulledRadicand eta d = Polynomial.C (xi ^ 2 - eta ^ 2) * (Polynomial.X ^ (2 * d) - 1) ^ 2

Distinct squared cage traces give radicands whose difference is a nonzero scalar times (t^(2d) - 1)².

theorem BGS.Markoff.cagePulledRadicand_derivative {K : Type u_1} [Field K] (xi : K) (d : ℕ) : Polynomial.derivative (cagePulledRadicand xi d) = Polynomial.C ↑(2 * d) * Polynomial.X ^ (2 * d - 1) * (2 * Polynomial.C (xi ^ 2 - 4) * (Polynomial.X ^ (2 * d) + 1) - Polynomial.C (4 * xi ^ 2))

Formal derivative of the pulled radicand.

theorem BGS.Markoff.cagePulledRadicand_separable {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {xi : K} (hxi : xi ≠ 0) (hparabolic : xi ^ 2 - 4 ≠ 0) {d : ℕ} (hd : 0 < d) (hdegree : ↑(2 * d) ≠ 0) : (cagePulledRadicand xi d).Separable

The pulled radicand has no repeated geometric root under the exact nondegeneracy assumptions used in the cage.

theorem BGS.Markoff.cagePulledRadicand_expanded {K : Type u_1} [Field K] (xi : K) (d : ℕ) : cagePulledRadicand xi d = Polynomial.C (xi ^ 2 - 4) * Polynomial.X ^ (4 * d) - Polynomial.C (2 * (xi ^ 2 + 4)) * Polynomial.X ^ (2 * d) + Polynomial.C (xi ^ 2 - 4)

Expanded form, used to read off the leading coefficient and degree.

theorem BGS.Markoff.cagePulledRadicand_coeff_four_mul {K : Type u_1} [Field K] (xi : K) {d : ℕ} (hd : 0 < d) : (cagePulledRadicand xi d).coeff (4 * d) = xi ^ 2 - 4

The coefficient of t^(4d) is the nonparabolic factor xi² - 4.

theorem BGS.Markoff.cagePulledRadicand_not_isUnit {K : Type u_1} [Field K] {xi : K} (hparabolic : xi ^ 2 - 4 ≠ 0) {d : ℕ} (hd : 0 < d) : ¬IsUnit (cagePulledRadicand xi d)

A nonparabolic pulled radicand is not a polynomial unit.

theorem BGS.Markoff.cagePulledRadicand_isCoprime {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {xi eta : K} (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) (d : ℕ) : IsCoprime (cagePulledRadicand xi d) (cagePulledRadicand eta d)

Off the diagonal, the two pulled radicands have disjoint geometric zero sets. The displayed difference reduces a hypothetical common zero to t^(2d)=1, where every radicand takes the value -16.

theorem BGS.Markoff.cagePulledRadicand_squarefree_and_product {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {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) (hdegree : ↑(2 * d) ≠ 0) : Squarefree (cagePulledRadicand xi d) ∧ Squarefree (cagePulledRadicand eta d) ∧ Squarefree (cagePulledRadicand xi d * cagePulledRadicand eta d)

The two off-diagonal radicands and their product are squarefree.

theorem BGS.Markoff.cagePulledRadicand_squareClasses_independent_ratFunc {K : Type u_1} [Field K] (h2 : 2 ≠ 0) {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) (hdegree : ↑(2 * d) ≠ 0) : ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (cagePulledRadicand xi d)) ∧ ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (cagePulledRadicand eta d)) ∧ ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (cagePulledRadicand xi d * cagePulledRadicand eta d))

The pulled radicands define two independent quadratic square classes in the rational function field. This is the algebraic content of the paper's disjoint-branch argument.