The descended seeded nonsplit trace curve

The Cayley coordinate converts the seeded nonsplit equation into one polynomial equation over the base field. This file constructs that polynomial, proves the scalar-extension formula and its bidegree bounds, and compares its base-field solutions exactly with the original torus solutions. Absolute irreducibility is deliberately a theorem to be proved, not an assumption.

@[instance_reducible]

noncomputable def BGS.Markoff.instFintypeQuadraticFiniteField_1 (p : ℕ) [Fact (Nat.Prime p)] : Fintype (quadraticFiniteField p)

Finiteness of the quadratic extension field used for the descended trace curve.

Equations

• BGS.Markoff.instFintypeQuadraticFiniteField_1 p = Fintype.ofFinite (BGS.Markoff.quadraticFiniteField p)

@[instance_reducible]

noncomputable def BGS.Markoff.instDecidableEqSubtypeUnitsQuadraticFiniteFieldMemSubgroupQuadraticNormOneTorus (p : ℕ) [Fact (Nat.Prime p)] : DecidableEq ↥(quadraticNormOneTorus p)

Classical equality on the norm-one torus for the descended trace curve.

Equations

• BGS.Markoff.instDecidableEqSubtypeUnitsQuadraticFiniteFieldMemSubgroupQuadraticNormOneTorus p = Classical.decEq ↥(BGS.Markoff.quadraticNormOneTorus p)

noncomputable def BGS.Markoff.quadraticCoefficientTracePolynomial (p : ℕ) [Fact (Nat.Prime p)] (P : Polynomial (quadraticFiniteField p)) : Polynomial (ZMod p)

Apply the quadratic field trace coefficientwise to a polynomial.

Equations

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

@[simp]

theorem BGS.Markoff.quadraticCoefficientTracePolynomial_coeff (p : ℕ) [Fact (Nat.Prime p)] (P : Polynomial (quadraticFiniteField p)) (n : ℕ) : (quadraticCoefficientTracePolynomial p P).coeff n = (Algebra.trace (ZMod p) (quadraticFiniteField p)) (P.coeff n)

theorem BGS.Markoff.quadraticCoefficientTracePolynomial_map (p : ℕ) [Fact (Nat.Prime p)] (P : Polynomial (quadraticFiniteField p)) : Polynomial.map (algebraMap (ZMod p) (quadraticFiniteField p)) (quadraticCoefficientTracePolynomial p P) = P + Polynomial.map (frobenius (quadraticFiniteField p) p) P

After scalar extension, coefficientwise trace is P + Frobenius(P).

noncomputable def BGS.Markoff.quadraticCayleyConjugateFactorPolynomial (p : ℕ) [Fact (Nat.Prime p)] : Polynomial (quadraticFiniteField p)

The linear Cayley factor whose zero is the Frobenius conjugate of the chosen nonbase element.

Equations

• BGS.Markoff.quadraticCayleyConjugateFactorPolynomial p = Polynomial.X - Polynomial.C (BGS.Markoff.quadraticNonbaseElement p ^ p)

noncomputable def BGS.Markoff.seededCayleyTraceNumeratorPolynomial (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d : ℕ) : Polynomial (ZMod p)

The seed-dependent numerator before descent.

Equations

• BGS.Markoff.seededCayleyTraceNumeratorPolynomial p s d = BGS.Markoff.quadraticCoefficientTracePolynomial p (Polynomial.C ↑s * BGS.Markoff.quadraticCayleyConjugateFactorPolynomial p ^ (2 * d))

theorem BGS.Markoff.seededCayleyTraceNumeratorPolynomial_map (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d : ℕ) : Polynomial.map (algebraMap (ZMod p) (quadraticFiniteField p)) (seededCayleyTraceNumeratorPolynomial p s d) = Polynomial.C ↑s * (Polynomial.X - Polynomial.C (quadraticNonbaseElement p ^ p)) ^ (2 * d) + Polynomial.C (↑s ^ p) * (Polynomial.X - Polynomial.C (quadraticNonbaseElement p)) ^ (2 * d)

noncomputable def BGS.Markoff.quadraticCayleyNormPolynomial (p : ℕ) [Fact (Nat.Prime p)] : Polynomial (ZMod p)

The norm of the Cayley linear factor, written directly over the base field.

Equations

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

theorem BGS.Markoff.quadraticCayleyNormPolynomial_map (p : ℕ) [Fact (Nat.Prime p)] : Polynomial.map (algebraMap (ZMod p) (quadraticFiniteField p)) (quadraticCayleyNormPolynomial p) = (Polynomial.X - Polynomial.C (quadraticNonbaseElement p ^ p)) * (Polynomial.X - Polynomial.C (quadraticNonbaseElement p))

theorem BGS.Markoff.algebraMap_eval_seededCayleyTraceNumeratorPolynomial (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d : ℕ) (z : ZMod p) : (algebraMap (ZMod p) (quadraticFiniteField p)) (Polynomial.eval z (seededCayleyTraceNumeratorPolynomial p s d)) = ↑s * ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) ^ (2 * d) + ↑s ^ p * ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p) ^ (2 * d)

theorem BGS.Markoff.algebraMap_eval_quadraticCayleyNormPolynomial (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : (algebraMap (ZMod p) (quadraticFiniteField p)) (Polynomial.eval z (quadraticCayleyNormPolynomial p)) = ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p ^ p) * ((algebraMap (ZMod p) (quadraticFiniteField p)) z - quadraticNonbaseElement p)

noncomputable def BGS.Markoff.univariateInFirstCoordinate {K : Type u_1} [CommSemiring K] (P : Polynomial K) : MvPolynomial (Fin 2) K

Embed a univariate polynomial in the first coordinate of a bivariate polynomial.

Equations

• BGS.Markoff.univariateInFirstCoordinate P = P.sum fun (n : ℕ) (c : K) => MvPolynomial.C c * MvPolynomial.X 0 ^ n

@[simp]

theorem BGS.Markoff.eval_univariateInFirstCoordinate {K : Type u_1} [CommSemiring K] (P : Polynomial K) (x y : K) : (MvPolynomial.eval ![x, y]) (univariateInFirstCoordinate P) = Polynomial.eval x P

theorem BGS.Markoff.univariateInFirstCoordinate_degreeOf_first_le {K : Type u_1} [CommSemiring K] [Nontrivial K] (P : Polynomial K) : MvPolynomial.degreeOf 0 (univariateInFirstCoordinate P) ≤ P.natDegree

theorem BGS.Markoff.univariateInFirstCoordinate_degreeOf_second_le {K : Type u_1} [CommSemiring K] [Nontrivial K] (P : Polynomial K) : MvPolynomial.degreeOf 1 (univariateInFirstCoordinate P) ≤ 0

theorem BGS.Markoff.seededCayleyTraceNumeratorPolynomial_natDegree_le (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d : ℕ) : (seededCayleyTraceNumeratorPolynomial p s d).natDegree ≤ 2 * d

theorem BGS.Markoff.quadraticCayleyNormPolynomial_natDegree_le (p : ℕ) [Fact (Nat.Prime p)] : (quadraticCayleyNormPolynomial p).natDegree ≤ 2

noncomputable def BGS.Markoff.seededNonsplitDescendedPolynomial (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) : MvPolynomial (Fin 2) (ZMod p)

The explicit bivariate polynomial over ZMod p defining the descended seeded nonsplit cover. Coordinate 0 is the Cayley affine coordinate and coordinate 1 is the base-field unit parameter.

Equations

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

theorem BGS.Markoff.eval_seededNonsplitDescendedPolynomial (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) (z u : ZMod p) : (MvPolynomial.eval ![z, u]) (seededNonsplitDescendedPolynomial p s d e) = Polynomial.eval z (seededCayleyTraceNumeratorPolynomial p s d) * u ^ e - Polynomial.eval z (quadraticCayleyNormPolynomial p) ^ d * (u ^ (2 * e) + 1)

theorem BGS.Markoff.seededNonsplitDescendedPolynomial_degreeOf_first_le (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) : MvPolynomial.degreeOf 0 (seededNonsplitDescendedPolynomial p s d e) ≤ 2 * d

theorem BGS.Markoff.seededNonsplitDescendedPolynomial_degreeOf_second_le (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) : MvPolynomial.degreeOf 1 (seededNonsplitDescendedPolynomial p s d e) ≤ 2 * e

theorem BGS.Markoff.seededNonsplitDescendedPolynomial_hasBidegreeAtMost (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) : External.HasBidegreeAtMost (seededNonsplitDescendedPolynomial p s d e) (2 * d) (2 * e)

theorem BGS.Markoff.eval_seededNonsplitDescendedPolynomial_eq_zero_iff (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (z : ZMod p) (u : (ZMod p)ˣ) : (MvPolynomial.eval ![z, ↑u]) (seededNonsplitDescendedPolynomial p (↑s) d e) = 0 ↔ SeededNonsplitTraceCoverEquation p k s d e (quadraticCayleyPoint p z) u

Vanishing of the descended base-field polynomial is exactly the seeded nonsplit trace equation at the Cayley point.

noncomputable def BGS.Markoff.seededNonsplitDescendedSolutions (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) : Finset (ZMod p × (ZMod p)ˣ)

Base-field solutions of the descended affine equation with the second coordinate restricted to a unit.

Equations

• BGS.Markoff.seededNonsplitDescendedSolutions p s d e = {z : ZMod p × (ZMod p)ˣ | (MvPolynomial.eval ![z.1, ↑z.2]) (BGS.Markoff.seededNonsplitDescendedPolynomial p s d e) = 0}

@[simp]

theorem BGS.Markoff.mem_seededNonsplitDescendedSolutions_iff (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) (z : ZMod p × (ZMod p)ˣ) : z ∈ seededNonsplitDescendedSolutions p s d e ↔ (MvPolynomial.eval ![z.1, ↑z.2]) (seededNonsplitDescendedPolynomial p s d e) = 0

noncomputable def BGS.Markoff.seededNonsplitNonidentitySolutions (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) : Finset ({ w : ↥(quadraticNormOneTorus p) // w ≠ 1 } × (ZMod p)ˣ)

Seeded nonsplit solutions with the identity point removed from the norm-one torus.

Equations

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

@[simp]

theorem BGS.Markoff.mem_seededNonsplitNonidentitySolutions_iff (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (z : { w : ↥(quadraticNormOneTorus p) // w ≠ 1 } × (ZMod p)ˣ) : z ∈ seededNonsplitNonidentitySolutions p k s d e ↔ SeededNonsplitTraceCoverEquation p k s d e (↑z.1) z.2

theorem BGS.Markoff.seededNonsplitDescendedSolutions_card_eq_nonidentity_card (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) : (seededNonsplitDescendedSolutions p (↑s) d e).card = (seededNonsplitNonidentitySolutions p k s d e).card

Cayley parametrization gives an exact bijection, with no multiplicity, between descended solutions and nonidentity torus solutions.

theorem BGS.Markoff.quadraticCayleyNormPolynomial_eval_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (z : ZMod p) : Polynomial.eval z (quadraticCayleyNormPolynomial p) ≠ 0

theorem BGS.Markoff.eval_seededNonsplitDescendedPolynomial_zero_second_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) (_hd : 0 < d) (he : 0 < e) (z : ZMod p) : (MvPolynomial.eval ![z, 0]) (seededNonsplitDescendedPolynomial p s d e) ≠ 0

For positive exponents the descended plane curve has no affine zero with second coordinate zero. Thus the affine Hasse--Weil count introduces no hidden u = 0 boundary.

theorem BGS.Markoff.affinePlaneCurveZeros_seededNonsplitDescendedPolynomial_card_eq (p : ℕ) [Fact (Nat.Prime p)] (s : (quadraticFiniteField p)ˣ) (d e : ℕ) (hd : 0 < d) (he : 0 < e) : (External.affinePlaneCurveZeros (ZMod p) (seededNonsplitDescendedPolynomial p s d e)).card = (seededNonsplitDescendedSolutions p s d e).card

The general affine-plane zero set and the unit-restricted descended set have exactly the same cardinality for positive exponents.

noncomputable def BGS.Markoff.seededNonsplitTraceCurveSolutions (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) : Finset (↥(quadraticNormOneTorus p) × (ZMod p)ˣ)

All seeded nonsplit torus solutions, including the identity point.

Equations

• BGS.Markoff.seededNonsplitTraceCurveSolutions p k s d e = {z : ↥(BGS.Markoff.quadraticNormOneTorus p) × (ZMod p)ˣ | BGS.Markoff.SeededNonsplitTraceCoverEquation p k s d e z.1 z.2}

@[simp]

theorem BGS.Markoff.mem_seededNonsplitTraceCurveSolutions_iff (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (z : ↥(quadraticNormOneTorus p) × (ZMod p)ˣ) : z ∈ seededNonsplitTraceCurveSolutions p k s d e ↔ SeededNonsplitTraceCoverEquation p k s d e z.1 z.2

noncomputable def BGS.Markoff.seededNonsplitIdentityBoundarySolutions (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) : Finset (ZMod p)ˣ

The precise omitted Cayley boundary: solutions lying above the identity of the norm-one torus.

Equations

• BGS.Markoff.seededNonsplitIdentityBoundarySolutions p k s d e = {u : (ZMod p)ˣ | BGS.Markoff.SeededNonsplitTraceCoverEquation p k s d e 1 u}

@[simp]

theorem BGS.Markoff.mem_seededNonsplitIdentityBoundarySolutions_iff (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (u : (ZMod p)ˣ) : u ∈ seededNonsplitIdentityBoundarySolutions p k s d e ↔ SeededNonsplitTraceCoverEquation p k s d e 1 u

theorem BGS.Markoff.seededNonsplitTraceCurveSolutions_card_eq_descended_add_identityBoundary (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) : (seededNonsplitTraceCurveSolutions p k s d e).card = (seededNonsplitDescendedSolutions p (↑s) d e).card + (seededNonsplitIdentityBoundarySolutions p k s d e).card

Exact count comparison, including the unique missing Cayley chart fiber w = 1.

noncomputable def BGS.Markoff.seededNonsplitIdentityBoundaryPolynomial (p : ℕ) [Fact (Nat.Prime p)] (s : quadraticFiniteField p) (e : ℕ) : Polynomial (ZMod p)

The one-variable polynomial cutting out the identity Cayley boundary.

Equations

• BGS.Markoff.seededNonsplitIdentityBoundaryPolynomial p s e = Polynomial.X ^ (2 * e) - Polynomial.C ((Algebra.trace (ZMod p) (BGS.Markoff.quadraticFiniteField p)) s) * Polynomial.X ^ e + 1

theorem BGS.Markoff.seededNonsplitIdentityBoundaryEquation_iff (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (u : (ZMod p)ˣ) : SeededNonsplitTraceCoverEquation p k s d e 1 u ↔ Polynomial.eval (↑u) (seededNonsplitIdentityBoundaryPolynomial p (↑↑s) e) = 0

theorem BGS.Markoff.seededNonsplitIdentityBoundaryPolynomial_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (s : quadraticFiniteField p) (e : ℕ) (he : 0 < e) : seededNonsplitIdentityBoundaryPolynomial p s e ≠ 0

theorem BGS.Markoff.seededNonsplitIdentityBoundaryPolynomial_natDegree_le (p : ℕ) [Fact (Nat.Prime p)] (s : quadraticFiniteField p) (e : ℕ) : (seededNonsplitIdentityBoundaryPolynomial p s e).natDegree ≤ 2 * e

theorem BGS.Markoff.seededNonsplitIdentityBoundarySolutions_card_le (p : ℕ) [Fact (Nat.Prime p)] (k : (ZMod p)ˣ) (s : ↑(quadraticNormFiber p k)) (d e : ℕ) (he : 0 < e) : (seededNonsplitIdentityBoundarySolutions p k s d e).card ≤ 2 * e

The omitted identity fiber contributes at most 2e points.

theorem BGS.Markoff.existingConicSeedNonsplitTraceCurveSolutions_eq_seeded (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) : existingConicSeedNonsplitTraceCurveSolutions p t ht ht0 s d e = seededNonsplitTraceCurveSolutions p (quadraticFiberProductUnit p t ht ht0) s d e

The generic seeded solution set is definitionally the existing-conic solution set after specializing its norm-fiber index.

theorem BGS.Markoff.existingConicSeedNonsplitTraceCurveSolutions_card_eq_affine_add_identityBoundary (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (d e : ℕ) (hd : 0 < d) (he : 0 < e) : (existingConicSeedNonsplitTraceCurveSolutions p t ht ht0 s d e).card = (External.affinePlaneCurveZeros (ZMod p) (seededNonsplitDescendedPolynomial p (↑s) d e)).card + (seededNonsplitIdentityBoundarySolutions p (quadraticFiberProductUnit p t ht ht0) s d e).card

Exact existing-conic count comparison with both affine boundaries exposed: u = 0 contributes nothing for positive exponents, while w = 1 is the displayed boundary term.