Geometry of the normalized cage incidence curve

The cage uses normalized trace coordinates, whereas the incidence geometry already proved in IncidenceCoordinateRing uses the paper's original Markoff coordinates. This file supplies the missing exact scaling bridge. Dividing the trace, common coordinate, and both retained roots by three identifies the two pairs of quadratic equations.

The off-diagonal geometric-integrality theorem below therefore reuses the existing biquadratic coordinate-ring proof. It does not assert geometric integrality of the subsequent power-trace pullback; that is the next Kummer obligation in the cage Hasse--Weil argument.

def BGS.Markoff.NormalizedIncidenceAux {K : Type u_1} [Field K] (xi eta middle firstRoot secondRoot : K) : Prop

The two retained incidence equations in normalized trace coordinates.

Equations

• BGS.Markoff.NormalizedIncidenceAux xi eta middle firstRoot secondRoot = ((xi ^ 2 - 4) * middle ^ 2 - firstRoot ^ 2 = 4 * xi ^ 2 ∧ (eta ^ 2 - 4) * middle ^ 2 - secondRoot ^ 2 = 4 * eta ^ 2)

structure BGS.Markoff.IncidenceAuxEquationWitness (K : Type u_2) [Field K] (a b : K) : Type u_2

A witness-bearing point of the original-coordinate incidence auxiliary curve.

• middle : K

  The common original-coordinate incidence parameter.

• firstRoot : K

  The retained root for the first quadratic equation.

• secondRoot : K

  The retained root for the second quadratic equation.

• equations : IncidenceAux a b self.middle self.firstRoot self.secondRoot

  Both original-coordinate incidence equations.

theorem BGS.Markoff.IncidenceAuxEquationWitness.ext {K : Type u_1} [Field K] {a b : K} {x y : IncidenceAuxEquationWitness K a b} (hmiddle : x.middle = y.middle) (hfirst : x.firstRoot = y.firstRoot) (hsecond : x.secondRoot = y.secondRoot) : x = y

theorem BGS.Markoff.IncidenceAuxEquationWitness.ext_iff {K : Type u_1} [Field K] {a b : K} {x y : IncidenceAuxEquationWitness K a b} : x = y ↔ x.middle = y.middle ∧ x.firstRoot = y.firstRoot ∧ x.secondRoot = y.secondRoot

theorem BGS.Markoff.normalizedIncidenceAux_iff_incidenceAux_div_three {K : Type u_1} [Field K] (h3 : 3 ≠ 0) (xi eta middle firstRoot secondRoot : K) : NormalizedIncidenceAux xi eta middle firstRoot secondRoot ↔ IncidenceAux (xi / 3) (eta / 3) (middle / 3) (firstRoot / 3) (secondRoot / 3)

Dividing all five normalized coordinates by three gives exactly the original-coordinate incidence equations.

theorem BGS.Markoff.normalizedIncidenceAuxGeometricallyIntegral_of_nondegenerate {K : Type u_1} [Field K] (h2 : 2 ≠ 0) (h3 : 3 ≠ 0) {xi eta : K} (hxi : xi ≠ 0) (heta : eta ≠ 0) (hXi : xi ^ 2 - 4 ≠ 0) (hEta : eta ^ 2 - 4 ≠ 0) (hneq : xi ^ 2 ≠ eta ^ 2) : IncidenceAuxGeometricallyIntegral (xi / 3) (eta / 3)

The normalized nondegeneracy conditions imply geometric integrality of the proved original-coordinate model.

@[reducible, inline]

abbrev BGS.Markoff.NormalizedCageIncidenceCoordinateRing (K : Type u_2) [Field K] (xi eta : K) : Type u_2

The original-coordinate coordinate-ring model of the normalized cage incidence curve. The accompanying point equivalence below records the coordinate scaling, rather than identifying the two coordinate systems.

Equations

• BGS.Markoff.NormalizedCageIncidenceCoordinateRing K xi eta = BGS.Markoff.IncidenceAuxCoordinateRing K (xi / 3) (eta / 3)

def BGS.Markoff.NormalizedCageIncidenceGeometricallyIntegral {K : Type u_2} [Field K] (xi eta : K) : Prop

Geometric integrality of the normalized incidence curve through its explicit original-coordinate model.

Equations

• BGS.Markoff.NormalizedCageIncidenceGeometricallyIntegral xi eta = BGS.Markoff.IncidenceAuxGeometricallyIntegral (xi / 3) (eta / 3)

theorem BGS.Markoff.splitMaximalTrace_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) (t : ZMod p) (hmax : IsSplitMaximalTrace p t) : t ≠ 0

A split-maximal cage trace is nonzero for the primes used by the cage.

theorem BGS.Markoff.splitMaximalTrace_sq_ne_four (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) (t : ZMod p) (hmax : IsSplitMaximalTrace p t) : t ^ 2 ≠ 4

A split-maximal cage trace is not parabolic.

theorem BGS.Markoff.normalizedCageIncidence_offDiagonal_geometricallyIntegral (p : ℕ) [Fact (Nat.Prime p)] (hpSeven : 7 ≤ p) (xi eta : ZMod p) (hxi : IsSplitMaximalTrace p xi) (heta : IsSplitMaximalTrace p eta) (hoffDiagonal : xi ^ 2 ≠ eta ^ 2) : NormalizedCageIncidenceGeometricallyIntegral xi eta

The off-diagonal base incidence curve occurring in the cage is geometrically integral under the cage's actual split-maximal hypotheses.

def BGS.Markoff.cageIncidenceEquationWitnessScaleEquiv {p : ℕ} [Fact (Nat.Prime p)] (h3 : 3 ≠ 0) (xi eta : ZMod p) : CageIncidenceEquationWitness p xi eta ≃ IncidenceAuxEquationWitness (ZMod p) (xi / 3) (eta / 3)

Witness-preserving equivalence between the normalized cage equations and the original-coordinate incidence equations.

Equations

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