Transporting primitive trace pairs back to rotation orbits

The endgame count returns an element of a complementary power-map image. The rotation parametrizations use the cyclic subgroup generated by the rotation eigenvalue. This file proves the exact transport between those two representations in the split and nonsplit cases.

theorem BGS.Markoff.complementaryExponent_pos {G : Type u_1} [Group G] [Finite G] (w : G) : 0 < Nat.card G / orderOf w

theorem BGS.Markoff.complementaryExponent_dvd_natCard {G : Type u_1} [Group G] (w : G) : Nat.card G / orderOf w ∣ Nat.card G

theorem BGS.Markoff.splitComplementaryExponent_cast_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (w : (ZMod p)ˣ) : ↑(Nat.card (ZMod p)ˣ / orderOf w) ≠ 0

theorem BGS.Markoff.nonsplitComplementaryExponent_cast_ne_zero (p : ℕ) [Fact (Nat.Prime p)] (w : ↥(quadraticNormOneTorus p)) : ↑(Nat.card ↥(quadraticNormOneTorus p) / orderOf w) ≠ 0

theorem BGS.Markoff.exists_pow_eq_of_mem_complementaryPowerRange {G : Type u_1} [CommGroup G] [Finite G] [IsCyclic G] (w : G) (h : ↥(powMonoidHom (Nat.card G / orderOf w)).range) : ∃ (n : ℕ), w ^ n = ↑h

A point in the complementary power-map image is reached by a natural power of the element whose order defines the complementary exponent.

theorem BGS.Markoff.exists_iterate_splitFiberPoint_eq_of_mem_complementaryPowerRange {F : Type u_1} [Field F] [Finite F] [IsCyclic Fˣ] (w s : Fˣ) (h : ↥(powMonoidHom (Nat.card Fˣ / orderOf w)).range) : ∃ (n : ℕ), normalizedRotate1^[n] (splitFiberPoint w s) = splitFiberPoint w (s * ↑h)

Split transport: every parameter returned by the primitive count is an actual forward iterate of the starting split-fiber point.

theorem BGS.Markoff.exists_iterate_splitFiberPoint_with_primitive_secondTrace (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : WeightedSplitTraceWeilBoundAssumption coefficient) (hpTwo : p ≠ 2) (w s : (ZMod p)ˣ) (hw : ↑w ^ 2 ≠ 1) (htrace : splitTorusTrace w ≠ 0) (horbitPositive : 0 < Nat.card (ZMod p)ˣ / orderOf w) (horbitChar : ↑(Nat.card (ZMod p)ˣ / orderOf w) ≠ 0) (horbitDvd : Nat.card (ZMod p)ˣ / orderOf w ∣ Nat.card (ZMod p)ˣ) (hexplicit : ↑(Nat.card (ZMod p)ˣ / orderOf w) * ↑(Nat.card (ZMod p)ˣ).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p) : ∃ (n : ℕ) (u : (ZMod p)ˣ), (normalizedRotate1^[n] (splitFiberPoint w s)).u2 = splitTorusTrace u ∧ orderOf u = Nat.card (ZMod p)ˣ

The split primitive-count theorem, with its power-image output transported all the way to an actual forward rotation iterate. Only the explicit Weil estimate and its arithmetic hypotheses remain as inputs.

theorem BGS.Markoff.exists_iterate_quadraticNormFiberPoint_eq_of_mem_complementaryPowerRange (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (s : ↑(quadraticConicNormFiber p t ht ht0)) (h : ↥(powMonoidHom (Nat.card ↥(quadraticNormOneTorus p) / orderOf w)).range) : ∃ (n : ℕ), normalizedRotate1^[n] (quadraticNormFiberPoint p t ht ht0 w s) = quadraticNormFiberPoint p t ht ht0 w (quadraticNormFiberMulNormOne p (quadraticFiberProductUnit p t ht ht0) s ↑h)

Nonsplit transport: every norm-one parameter returned by the seeded primitive count is an actual forward iterate of the starting point on the base-field conic.

theorem BGS.Markoff.existingConicSeedNonsplitTorusTrace_eq_quadraticNormFiberPoint_u2 (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (s : ↑(quadraticConicNormFiber p t ht ht0)) (h : ↥(quadraticNormOneTorus p)) : existingConicSeedNonsplitTorusTrace p t ht ht0 s h = (quadraticNormFiberPoint p t ht ht0 w (quadraticNormFiberMulNormOne p (quadraticFiberProductUnit p t ht ht0) s h)).u2

The seeded trace counted in the nonsplit endgame is exactly the second coordinate of the corresponding point in the base-field conic parametrization.

theorem BGS.Markoff.exists_iterate_quadraticNormFiberPoint_with_primitive_secondTrace (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : SeededNonsplitTraceWeilBoundAssumption coefficient) (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)) (htrace : quadraticNormOneTrace p w = t) (s : ↑(quadraticConicNormFiber p t ht ht0)) (horbitPositive : 0 < Nat.card ↥(quadraticNormOneTorus p) / orderOf w) (horbitChar : ↑(Nat.card ↥(quadraticNormOneTorus p) / orderOf w) ≠ 0) (horbitDvd : Nat.card ↥(quadraticNormOneTorus p) / orderOf w ∣ Nat.card ↥(quadraticNormOneTorus p)) (hexplicit : ↑(Nat.card ↥(quadraticNormOneTorus p) / orderOf w) * ↑(Nat.card (ZMod p)ˣ).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p) : ∃ (n : ℕ) (u : (ZMod p)ˣ), (normalizedRotate1^[n] (quadraticNormFiberPoint p t ht ht0 w s)).u2 = splitTorusTrace u ∧ orderOf u = Nat.card (ZMod p)ˣ

The corrected nonsplit primitive-count theorem, transported to an actual forward iterate on the base-field conic.

theorem BGS.Markoff.exists_threshold_splitFiberPoint_with_primitive_secondTrace (coefficient : ℕ) (hWeil : WeightedSplitTraceWeilBoundAssumption coefficient) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (w s : (ZMod p)ˣ), ↑w ^ 2 ≠ 1 → splitTorusTrace w ≠ 0 → ↑p ^ (1 / 2 + δ) ≤ ↑(orderOf w) → ∃ (n : ℕ) (u : (ZMod p)ˣ), (normalizedRotate1^[n] (splitFiberPoint w s)).u2 = splitTorusTrace u ∧ orderOf u = Nat.card (ZMod p)ˣ

Uniform large-order split endgame, still expressed in the explicit split-fiber parametrization.

theorem BGS.Markoff.exists_threshold_quadraticNormFiberPoint_with_primitive_secondTrace (coefficient : ℕ) (hWeil : SeededNonsplitTraceWeilBoundAssumption coefficient) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (w : ↥(quadraticNormOneTorus p)), quadraticNormOneTrace p w = t → ∀ (s : ↑(quadraticConicNormFiber p t ht ht0)), ↑p ^ (1 / 2 + δ) ≤ ↑(orderOf w) → ∃ (n : ℕ) (u : (ZMod p)ˣ), (normalizedRotate1^[n] (quadraticNormFiberPoint p t ht ht0 w s)).u2 = splitTorusTrace u ∧ orderOf u = Nat.card (ZMod p)ˣ

Uniform large-order nonsplit endgame in the corrected seeded conic parametrization.

theorem BGS.Markoff.exists_split_or_nonsplitFiberParameter (p : ℕ) [Fact (Nat.Prime p)] (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (x : ↑(normalizedFiber1 t)) : (∃ (w : (ZMod p)ˣ), splitTorusTrace w = t ∧ ↑w ^ 2 ≠ 1 ∧ ∃ (s : (ZMod p)ˣ), splitFiberPoint w s = ↑x) ∨ ∃ (w : ↥(quadraticNormOneTorus p)), quadraticNormOneTrace p w = t ∧ ↑↑w ^ 2 ≠ 1 ∧ ∃ (s : ↑(quadraticConicNormFiber p t ht ht0)), quadraticNormFiberPoint p t ht ht0 w s = ↑x

The missing classified witness bridge: an arbitrary point on a nonzero nonparabolic fiber is represented by the explicit split or nonsplit conic parametrization attached to the eigenvalue supplied by trace classification.

theorem BGS.Markoff.exists_threshold_nonparabolicPoint_with_primitive_secondTrace (splitCoefficient : ℕ) (hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (t : ZMod p), t ^ 2 ≠ 4 → t ≠ 0 → ∀ (x : ↑(normalizedFiber1 t)), ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder t) → ∃ (n : ℕ) (u : (ZMod p)ˣ), (normalizedRotate1^[n] ↑x).u2 = splitTorusTrace u ∧ orderOf u = Nat.card (ZMod p)ˣ

Classified semisimple endgame: every nonzero nonparabolic normalized Markoff point with a large first-coordinate rotation reaches a point whose second coordinate is the trace of a primitive base-field unit.

theorem BGS.Markoff.exists_threshold_nonparabolicPoint_with_maximal_secondRotation (splitCoefficient : ℕ) (hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (t : ZMod p), t ^ 2 ≠ 4 → t ≠ 0 → ∀ (x : ↑(normalizedFiber1 t)), ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder t) → ∃ (n : ℕ), rotationOrder (normalizedRotate1^[n] ↑x).u2 = p - 1

Proposition 10 for the nonparabolic branches, stated directly as maximal matrix rotation order in the newly reached second coordinate.