Witness-preserving equations for the cage fiber product

This file gives the exact algebraic bridge for the canonical pair of axes. It deliberately retains the two intersection witnesses. No point-count or irreducibility assertion is made here.

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

Scalar coordinates of the two incidence witnesses with common third coordinate. The roots record the two quadratic choices separately.

• middle : ZMod p

  The common coordinate of the two incidence points.

• firstRoot : ZMod p

  The discriminant root retaining the first incidence point.

• secondRoot : ZMod p

  The discriminant root retaining the second incidence point.

• firstEquation : (xi ^ 2 - 4) * self.middle ^ 2 - self.firstRoot ^ 2 = 4 * xi ^ 2

  The quadratic incidence equation for the first fixed trace.

• secondEquation : (eta ^ 2 - 4) * self.middle ^ 2 - self.secondRoot ^ 2 = 4 * eta ^ 2

  The quadratic incidence equation for the second fixed trace.

theorem BGS.Markoff.CageIncidenceEquationWitness.ext {p : ℕ} [Fact (Nat.Prime p)] {xi eta : ZMod p} {x y : CageIncidenceEquationWitness p xi eta} (hmiddle : x.middle = y.middle) (hfirst : x.firstRoot = y.firstRoot) (hsecond : x.secondRoot = y.secondRoot) : x = y

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

theorem BGS.Markoff.normalized_first_third_point_of_discriminant_equation {K : Type u_1} [Field K] (hTwo : 2 ≠ 0) (xi middle root : K) (hEquation : (xi ^ 2 - 4) * middle ^ 2 - root ^ 2 = 4 * xi ^ 2) : normalizedPolynomial { u1 := xi, u2 := (xi * middle - root) / 2, u3 := middle } = 0

A first-coordinate discriminant equation reconstructs a normalized Markoff point.

theorem BGS.Markoff.normalized_second_third_point_of_discriminant_equation {K : Type u_1} [Field K] (hTwo : 2 ≠ 0) (eta middle root : K) (hEquation : (eta ^ 2 - 4) * middle ^ 2 - root ^ 2 = 4 * eta ^ 2) : normalizedPolynomial { u1 := (eta * middle - root) / 2, u2 := eta, u3 := middle } = 0

A second-coordinate discriminant equation reconstructs a normalized Markoff point.

def BGS.Markoff.canonicalCageWitnessToEquations (p : ℕ) [Fact (Nat.Prime p)] (xi eta : ZMod p) : CageMiddleWitnessPair p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta → CageIncidenceEquationWitness p xi eta

A canonical cage witness pair gives the two quadratic incidence roots, without projecting either root away.

Equations

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

def BGS.Markoff.canonicalCageEquationsToWitness (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) : CageIncidenceEquationWitness p xi eta → CageMiddleWitnessPair p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta

Reconstruct both actual Markoff points from the common coordinate and the two retained roots.

Equations

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

def BGS.Markoff.canonicalCageWitnessEquivIncidenceEquations (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (xi eta : ZMod p) : CageMiddleWitnessPair p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta ≃ CageIncidenceEquationWitness p xi eta

For odd characteristic, the canonical witness pair is exactly the pair of quadratic equations. In particular this equivalence exposes the diagonal case: the two root fields remain independent even when the two equations coincide.

Equations

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