The shifted cage trace cover

The off-diagonal cage base is the biquadratic incidence function field in the common original coordinate y. The next cover adjoins a root R of

R^2 - (3y) * R + 1.

This file proves the genuinely new branch calculation: the discriminant 9y^2 - 4 is independent of both incidence square classes, remains a nonsquare after the two quadratic adjunctions, and hence makes the trace quadratic irreducible over the exact incidence function-field presentation.

It deliberately does not claim that R is not a q-th power. That place-at-infinity statement is the remaining Kummer obstruction for the full shifted Laurent cover.

noncomputable def BGS.Markoff.cageTraceBranchPolynomial {K : Type u_1} [Field K] : Polynomial K

The discriminant 9y² - 4 of the normalized trace quadratic.

Equations

• BGS.Markoff.cageTraceBranchPolynomial = Polynomial.C 9 * Polynomial.X ^ 2 - Polynomial.C 4

noncomputable def BGS.Markoff.traceRootPolynomial {R : Type u_2} [CommRing R] (trace : R) : Polynomial R

The quadratic whose root is a unit with prescribed trace.

Equations

• BGS.Markoff.traceRootPolynomial trace = Polynomial.X ^ 2 - Polynomial.C trace * Polynomial.X + 1

theorem BGS.Markoff.traceRootPolynomial_monic {R : Type u_2} [Nontrivial R] [CommRing R] (trace : R) : (traceRootPolynomial trace).Monic

The prescribed-trace quadratic is monic.

@[simp]

theorem BGS.Markoff.traceRootPolynomial_natDegree {R : Type u_2} [Nontrivial R] [CommRing R] (trace : R) : (traceRootPolynomial trace).natDegree = 2

The prescribed-trace quadratic has degree two.

theorem BGS.Markoff.traceRootPolynomial_irreducible_of_discriminant_not_isSquare {R : Type u_2} [CommRing R] [IsDomain R] (trace : R) (hdisc : ¬IsSquare (trace ^ 2 - 4)) : Irreducible (traceRootPolynomial trace)

A prescribed-trace quadratic over a domain is irreducible when its discriminant is not a square.

theorem BGS.Markoff.cageTraceBranchPolynomial_natDegree {K : Type u_1} [Field K] (h3 : 3 ≠ 0) : cageTraceBranchPolynomial.natDegree = 2

The trace discriminant polynomial has degree two outside characteristic three.

theorem BGS.Markoff.cageTraceBranchPolynomial_not_isUnit {K : Type u_1} [Field K] (h3 : 3 ≠ 0) : ¬IsUnit cageTraceBranchPolynomial

The trace discriminant polynomial is not a unit.

theorem BGS.Markoff.cageTraceBranchPolynomial_separable {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) : cageTraceBranchPolynomial.Separable

The two trace branch points are distinct outside characteristics two and three.

theorem BGS.Markoff.incidenceBranchPolynomial_cageTrace_linearCombination {K : Type u_1} [Field K] (a : K) : Polynomial.C (9 * a ^ 2 - 4) * cageTraceBranchPolynomial - Polynomial.C 9 * incidenceBranchPolynomial a = Polynomial.C 16

An explicit constant Bezout combination of an incidence branch polynomial and the trace discriminant polynomial.

theorem BGS.Markoff.incidenceBranchPolynomial_isCoprime_cageTrace {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (a : K) : IsCoprime (incidenceBranchPolynomial a) cageTraceBranchPolynomial

Every nondegenerate incidence branch polynomial is coprime to the trace discriminant polynomial; the Bezout constant is 16.

theorem BGS.Markoff.cageTraceBranchSquareClasses_independent_ratFunc {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) cageTraceBranchPolynomial) ∧ ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (incidenceBranchPolynomial a * cageTraceBranchPolynomial)) ∧ ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (incidenceBranchPolynomial b * cageTraceBranchPolynomial)) ∧ ¬IsSquare ((algebraMap (Polynomial K) (RatFunc K)) (incidenceBranchPolynomial a * incidenceBranchPolynomial b * cageTraceBranchPolynomial))

The trace discriminant and its products with either incidence branch class are all nonsquares in the rational function field.

theorem BGS.Markoff.incidenceBiquadraticTraceBranch_not_isSquare {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : ¬IsSquare ((algebraMap (IncidenceFirstQuadraticRatFuncRing K a) (IncidenceBiquadraticRatFuncRing K a b)) ((algebraMap (RatFunc K) (IncidenceFirstQuadraticRatFuncRing K a)) ((algebraMap (Polynomial K) (RatFunc K)) cageTraceBranchPolynomial)))

The discriminant of the trace quadratic remains nonsquare after adjoining both incidence square roots.

noncomputable def BGS.Markoff.incidenceBiquadraticNormalizedTrace {K : Type u_1} [Field K] (a b : K) : IncidenceBiquadraticRatFuncRing K a b

The normalized common coordinate 3y inside the biquadratic incidence function field.

Equations

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

theorem BGS.Markoff.incidenceBiquadraticNormalizedTrace_discriminant {K : Type u_1} [Field K] (a b : K) : incidenceBiquadraticNormalizedTrace a b ^ 2 - 4 = (algebraMap (IncidenceFirstQuadraticRatFuncRing K a) (IncidenceBiquadraticRatFuncRing K a b)) ((algebraMap (RatFunc K) (IncidenceFirstQuadraticRatFuncRing K a)) ((algebraMap (Polynomial K) (RatFunc K)) cageTraceBranchPolynomial))

The discriminant of the normalized trace inside the biquadratic field is the image of 9y² - 4.

theorem BGS.Markoff.incidenceBiquadraticNormalizedTrace_discriminant_not_isSquare {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : ¬IsSquare (incidenceBiquadraticNormalizedTrace a b ^ 2 - 4)

The normalized trace discriminant remains nonsquare in the complete biquadratic incidence function field.

noncomputable def BGS.Markoff.incidenceBiquadraticTraceRootPolynomial {K : Type u_1} [Field K] (a b : K) : Polynomial (IncidenceBiquadraticRatFuncRing K a b)

The trace quadratic over the exact incidence biquadratic field presentation.

Equations

• BGS.Markoff.incidenceBiquadraticTraceRootPolynomial a b = Polynomial.X ^ 2 - Polynomial.C (BGS.Markoff.incidenceBiquadraticNormalizedTrace a b) * Polynomial.X + 1

theorem BGS.Markoff.incidenceBiquadraticTraceRootPolynomial_irreducible {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {a b : K} (ha : a ≠ 0) (hb : b ≠ 0) (hA : 9 * a ^ 2 - 4 ≠ 0) (hB : 9 * b ^ 2 - 4 ≠ 0) (hab : a ^ 2 ≠ b ^ 2) : Irreducible (incidenceBiquadraticTraceRootPolynomial a b)

The trace quadratic is irreducible over the off-diagonal incidence biquadratic function field.

@[reducible, inline]

abbrev BGS.Markoff.IncidenceTraceFunctionField (K : Type u_2) [Field K] (a b : K) : Type u_2

The quadratic trace extension of the cage incidence function field.

Equations

• BGS.Markoff.IncidenceTraceFunctionField K a b = AdjoinRoot (BGS.Markoff.incidenceBiquadraticTraceRootPolynomial a b)

noncomputable def BGS.Markoff.incidenceTraceRoot {K : Type u_1} [Field K] (a b : K) : IncidenceTraceFunctionField K a b

The canonical unit-trace root in the quadratic trace extension.

Equations

• BGS.Markoff.incidenceTraceRoot a b = AdjoinRoot.root (BGS.Markoff.incidenceBiquadraticTraceRootPolynomial a b)

theorem BGS.Markoff.incidenceTraceRoot_quadratic_relation {K : Type u_1} [Field K] (a b : K) : incidenceTraceRoot a b ^ 2 - (algebraMap (IncidenceBiquadraticRatFuncRing K a b) (IncidenceTraceFunctionField K a b)) (incidenceBiquadraticNormalizedTrace a b) * incidenceTraceRoot a b + 1 = 0

The canonical trace root satisfies R² - (3y)R + 1 = 0.