The geometric Corvaja--Zannier interface for the middle game

Corvaja--Zannier, JEMS 15 (2013), Corollary 2, bounds torsion points on an absolutely irreducible curve in a two-dimensional torus which is not a translate of a subtorus. The actual Markoff middle-game finset consists of solutions of

alpha * h + beta * h⁻¹ = k + k⁻¹, with h ∈ H₁ and k ∈ H₂.

This module embeds that finset into the exact geometric torsion intersection of the weighted trace curve. It keeps all hypotheses of the cited result visible. In particular, alpha * beta ≠ 1 is not silently identified with absolute irreducibility or with the non-subtorus condition.

The constant 20 printed in the Markoff paper is not the direct specialization of Corvaja--Zannier Corollary 2. For the (2,2) trace curve, the 12 d₁ d₂ / p term alone gives 48 m₁ m₂ / p. Accordingly the source-backed envelope in this module has constant 48; obtaining 20 requires a separate argument.

noncomputable def BGS.Markoff.weightedTraceTorusClosurePolynomial {K : Type u_1} [Field K] (alpha beta : K) : MvPolynomial (Fin 2) K

The affine closure polynomial of the weighted trace curve after removing the boundary monomial which appears when beta = 0. Variable 0 is the right trace parameter k and variable 1 is the left parameter h.

Removing this monomial is essential: Corvaja--Zannier concerns the curve in the torus, not the extra coordinate-axis component introduced by clearing denominators.

Equations

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

theorem BGS.Markoff.eval_weightedTraceTorusClosurePolynomial_eq_zero_iff {K : Type u_1} [Field K] (alpha beta : K) (k h : Kˣ) : (MvPolynomial.eval ![↑k, ↑h]) (weightedTraceTorusClosurePolynomial alpha beta) = 0 ↔ weightedSplitTorusTrace alpha beta h = splitTorusTrace k

On nonzero coordinates, the reduced affine polynomial cuts out exactly the weighted trace equation.

def BGS.Markoff.WeightedTraceCurveAbsolutelyIrreducible {K : Type u_1} [Field K] (alpha beta : K) : Prop

Absolute irreducibility of the actual torus closure, expressed as irreducibility after base change to an algebraic closure. This is a proposition, not a typeclass.

Equations

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

def BGS.Markoff.WeightedTraceCurveNotSubtorusTranslate {K : Type u_1} [Field K] (alpha beta : K) : Prop

Exact geometric non-specialness: over an algebraic closure, no nontrivial character is constant on the whole weighted trace curve. For an irreducible curve in G_m^2, this is equivalent to not being a translate of a one-dimensional subtorus.

Equations

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

def BGS.Markoff.WeightedTraceCurveIsCorvajaZannierAdmissible {K : Type u_1} [Field K] (alpha beta : K) : Prop

The concrete curve hypotheses needed by the weighted-trace specialization of Corvaja--Zannier Corollary 2. Both weights are nonzero, the curve is nondegenerate and absolutely irreducible, and it is not a translate of a subtorus. These conditions are kept separate from the external cardinal estimate.

Equations

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

noncomputable def BGS.Markoff.weightedTraceCurveTorsionIntersection {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (leftOrder rightOrder : ℕ) : Finset (Eˣ × Eˣ)

The geometric torsion intersection to which Corvaja--Zannier Corollary 2 applies. Coordinates are ordered (k, h) to match splitTraceCoverPolynomial.

Equations

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

@[simp]

theorem BGS.Markoff.mem_weightedTraceCurveTorsionIntersection_iff {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (leftOrder rightOrder : ℕ) (z : Eˣ × Eˣ) : z ∈ weightedTraceCurveTorsionIntersection alpha beta leftOrder rightOrder ↔ weightedSplitTorusTrace alpha beta z.2 = splitTorusTrace z.1 ∧ z.2 ^ leftOrder = 1 ∧ z.1 ^ rightOrder = 1

theorem BGS.Markoff.mem_weightedTraceCurveTorsionIntersection_iff_polynomial {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (leftOrder rightOrder : ℕ) (z : Eˣ × Eˣ) : z ∈ weightedTraceCurveTorsionIntersection alpha beta leftOrder rightOrder ↔ (MvPolynomial.eval ![↑z.1, ↑z.2]) (weightedTraceTorusClosurePolynomial alpha beta) = 0 ∧ z.2 ^ leftOrder = 1 ∧ z.1 ^ rightOrder = 1

The same intersection stated with the explicit affine closure polynomial. This is the line-level bridge from the finite set to the algebraic curve consumed by Corollary 2.

def BGS.Markoff.weightedTraceSubgroupSolutionToCurvePoint {E : Type u_1} [Field E] (H₁ H₂ : Subgroup Eˣ) : ↥H₁ × ↥H₂ → Eˣ × Eˣ

Swap a subgroup solution into the geometric coordinate order (k, h).

Equations

• BGS.Markoff.weightedTraceSubgroupSolutionToCurvePoint H₁ H₂ z = (↑z.2, ↑z.1)

theorem BGS.Markoff.weightedTraceSubgroupSolutionToCurvePoint_injective {E : Type u_1} [Field E] (H₁ H₂ : Subgroup Eˣ) : Function.Injective (weightedTraceSubgroupSolutionToCurvePoint H₁ H₂)

theorem BGS.Markoff.weightedTraceSubgroupSolutionToCurvePoint_mem_torsionIntersection {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) (z : ↥H₁ × ↥H₂) (hz : z ∈ weightedTraceEquationSolutions alpha beta H₁ H₂) : weightedTraceSubgroupSolutionToCurvePoint H₁ H₂ z ∈ weightedTraceCurveTorsionIntersection alpha beta (Nat.card ↥H₁) (Nat.card ↥H₂)

Every actual subgroup solution gives a point in the corresponding geometric torsion intersection. The subgroup cardinalities become the two root-of-unity exponents by Lagrange's theorem.

theorem BGS.Markoff.weightedTraceEquationSolutions_card_le_curveTorsionIntersection {E : Type u_1} [Field E] [Fintype E] (alpha beta : E) (H₁ H₂ : Subgroup Eˣ) : (weightedTraceEquationSolutions alpha beta H₁ H₂).card ≤ (weightedTraceCurveTorsionIntersection alpha beta (Nat.card ↥H₁) (Nat.card ↥H₂)).card

The actual weighted solution count is bounded by the exact geometric torsion intersection count. This theorem contains no Corvaja--Zannier assumption.