The one-sided power cover of the cage witness equations

This file identifies the exact d-fold cover counted before passage to the power-map range with the two pulled radicand equations. Both incidence roots remain part of the data.

theorem BGS.Markoff.scaled_incidenceEquation_iff_pulledRadicand {K : Type u_1} [Field K] (u xi root : K) (hu : u ≠ 0) (d : ℕ) : (xi ^ 2 - 4) * (u ^ d + (u ^ d)⁻¹) ^ 2 - root ^ 2 = 4 * xi ^ 2 ↔ (u ^ d * root) ^ 2 = Polynomial.eval u (cagePulledRadicand xi d)

Clearing the denominator in one incidence equation gives exactly the pulled radicand.

structure BGS.Markoff.CagePulledRootPair (p : ℕ) [Fact (Nat.Prime p)] (xi eta : ZMod p) (d : ℕ) : Type

The exact pulled pair of quadratic roots over a nonzero power parameter.

• parameter : (ZMod p)ˣ

  The parameter before applying the d-th power map.

• firstRoot : ZMod p

  The first denominator-cleared incidence root.

• secondRoot : ZMod p

  The second denominator-cleared incidence root.

• firstEquation : self.firstRoot ^ 2 = Polynomial.eval (↑self.parameter) (cagePulledRadicand xi d)

  First pulled radicand equation.

• secondEquation : self.secondRoot ^ 2 = Polynomial.eval (↑self.parameter) (cagePulledRadicand eta d)

  Second pulled radicand equation.

theorem BGS.Markoff.CagePulledRootPair.ext {p : ℕ} [Fact (Nat.Prime p)] {xi eta : ZMod p} {d : ℕ} {x y : CagePulledRootPair p xi eta d} (hparameter : x.parameter = y.parameter) (hfirst : x.firstRoot = y.firstRoot) (hsecond : x.secondRoot = y.secondRoot) : x = y

theorem BGS.Markoff.CagePulledRootPair.ext_iff {p : ℕ} [Fact (Nat.Prime p)] {xi eta : ZMod p} {d : ℕ} {x y : CagePulledRootPair p xi eta d} : x = y ↔ x.parameter = y.parameter ∧ x.firstRoot = y.firstRoot ∧ x.secondRoot = y.secondRoot

@[reducible, inline]

abbrev BGS.Markoff.canonicalCagePowerCoverSolutions (p : ℕ) [Fact (Nat.Prime p)] (xi eta : ZMod p) (d : ℕ) : Type

The canonical witness-bearing one-sided cover.

Equations

• BGS.Markoff.canonicalCagePowerCoverSolutions p xi eta d = BGS.rightPowerTraceCoverSolutions BGS.Markoff.cageMiddleWitnessTrace BGS.Markoff.splitTorusTrace d

def BGS.Markoff.canonicalCagePowerCoverToPulled (p : ℕ) [Fact (Nat.Prime p)] (xi eta : ZMod p) (d : ℕ) : canonicalCagePowerCoverSolutions p xi eta d → CagePulledRootPair p xi eta d

Scale the two retained incidence roots by the common denominator.

Equations

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

def BGS.Markoff.canonicalCagePulledToPowerCover (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) (d : ℕ) : CagePulledRootPair p xi eta d → canonicalCagePowerCoverSolutions p xi eta d

Recover the unscaled incidence roots and the two actual Markoff points.

Equations

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

@[simp]

theorem BGS.Markoff.canonicalCageWitnessToEquations_equationsToWitness (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) (z : CageIncidenceEquationWitness p xi eta) : canonicalCageWitnessToEquations p xi eta (canonicalCageEquationsToWitness p hpTwo xi eta z) = z

def BGS.Markoff.canonicalCagePowerCoverEquivPulled (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) (d : ℕ) : canonicalCagePowerCoverSolutions p xi eta d ≃ CagePulledRootPair p xi eta d

The canonical one-sided cage power cover is exactly the pulled pair of radicand equations.

Equations

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

theorem BGS.Markoff.natCard_cagePulledRootPair_eq_mul_canonicalPowerRange (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) (d : ℕ) (hd : d ∣ p - 1) : Nat.card (CagePulledRootPair p xi eta d) = d * Nat.card (cageMiddleWitnessPowerRangeSolutions p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta d)

Exact division of the pulled affine cover by the d-th power-map fibers.