Möbius inclusion--exclusion for primitive endgame traces

This file formalizes published equations (35)--(36). For a fixed left power-map image and a finite cyclic right group, it partitions trace coincidences by the exact order of the right-hand element, applies Möbius inversion, and identifies the cumulative order-divisibility count with the corresponding right power-map image.

theorem BGS.Markoff.powMonoidHom_range_eq_ker_complementaryExponent {H : Type u_2} [CommGroup H] [Finite H] [IsCyclic H] (d : ℕ) (hdvd : d ∣ Nat.card H) : (powMonoidHom d).range = (powMonoidHom (Nat.card H / d)).ker

In a finite cyclic group, the image of the d-th power map is the kernel of the (card / d)-th power map whenever d divides the group order.

theorem BGS.Markoff.powMonoidHom_range_eq_zpowers_of_complementaryOrder {K : Type u_4} [CommGroup K] [Finite K] [IsCyclic K] (w : K) : (powMonoidHom (Nat.card K / orderOf w)).range = Subgroup.zpowers w

In a finite cyclic group, the image of the complementary power map is exactly the cyclic subgroup generated by the element whose order defines that complementary exponent. This is the bridge between the endgame count, which is naturally stated on a power-map image, and the rotation orbit, which is naturally stated as Subgroup.zpowers w.

noncomputable def BGS.Markoff.traceRelationPairs {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent : ℕ) : Finset (↥(powMonoidHom leftExponent).range × H)

All trace coincidences with the left coordinate restricted to one power-map image.

Equations

• BGS.Markoff.traceRelationPairs leftTrace rightTrace leftExponent = {z : ↥(powMonoidHom leftExponent).range × H | leftTrace ↑z.1 = rightTrace z.2}

noncomputable def BGS.Markoff.traceExactOrderSolutions {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent order : ℕ) : Finset (↥(powMonoidHom leftExponent).range × H)

Trace coincidences whose right coordinate has one exact multiplicative order.

Equations

• BGS.Markoff.traceExactOrderSolutions leftTrace rightTrace leftExponent order = {z ∈ BGS.Markoff.traceRelationPairs leftTrace rightTrace leftExponent | orderOf z.2 = order}

noncomputable def BGS.Markoff.tracePowerKernelSolutions {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent exponent : ℕ) : Finset (↥(powMonoidHom leftExponent).range × H)

Trace coincidences whose right coordinate is killed by one power.

Equations

• BGS.Markoff.tracePowerKernelSolutions leftTrace rightTrace leftExponent exponent = {z ∈ BGS.Markoff.traceRelationPairs leftTrace rightTrace leftExponent | z.2 ^ exponent = 1}

@[simp]

theorem BGS.Markoff.mem_traceExactOrderSolutions_iff {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent order : ℕ) (z : ↥(powMonoidHom leftExponent).range × H) : z ∈ traceExactOrderSolutions leftTrace rightTrace leftExponent order ↔ leftTrace ↑z.1 = rightTrace z.2 ∧ orderOf z.2 = order

@[simp]

theorem BGS.Markoff.mem_tracePowerKernelSolutions_iff {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent exponent : ℕ) (z : ↥(powMonoidHom leftExponent).range × H) : z ∈ tracePowerKernelSolutions leftTrace rightTrace leftExponent exponent ↔ leftTrace ↑z.1 = rightTrace z.2 ∧ z.2 ^ exponent = 1

theorem BGS.Markoff.sum_traceExactOrderSolutions_card_eq_tracePowerKernelSolutions_card {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent m : ℕ) (hm : 0 < m) : ∑ order ∈ m.divisors, (traceExactOrderSolutions leftTrace rightTrace leftExponent order).card = (tracePowerKernelSolutions leftTrace rightTrace leftExponent m).card

Exact-order classes partition the trace coincidences killed by the m-th power map.

theorem BGS.Markoff.moebius_sum_tracePowerKernelSolutions_card_eq_traceExactOrderSolutions_card {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent n : ℕ) (hn : 0 < n) : ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑(tracePowerKernelSolutions leftTrace rightTrace leftExponent x.2).card = ↑(traceExactOrderSolutions leftTrace rightTrace leftExponent n).card

Möbius inversion recovers the exact-order trace count from the power-kernel counts.

def BGS.Markoff.powerTraceRangeSolutionsEquivTracePowerKernelSolutions {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent rightExponent kernelExponent : ℕ) (hsubgroup : (powMonoidHom rightExponent).range = (powMonoidHom kernelExponent).ker) : powerTraceRangeSolutions leftTrace rightTrace leftExponent rightExponent ≃ ↥(tracePowerKernelSolutions leftTrace rightTrace leftExponent kernelExponent)

A right power-range solution is a right power-kernel solution whenever the two subgroups are identified.

Equations

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

theorem BGS.Markoff.natCard_powerTraceRangeSolutions_eq_tracePowerKernelSolutions_card {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent rightExponent kernelExponent : ℕ) (hsubgroup : (powMonoidHom rightExponent).range = (powMonoidHom kernelExponent).ker) : Nat.card (powerTraceRangeSolutions leftTrace rightTrace leftExponent rightExponent) = (tracePowerKernelSolutions leftTrace rightTrace leftExponent kernelExponent).card

Cardinal form of powerTraceRangeSolutionsEquivTracePowerKernelSolutions.

theorem BGS.Markoff.moebius_sum_powerTraceRangeSolutions_card_eq_traceExactOrderSolutions_card {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] [IsCyclic H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent : ℕ) : ∑ x ∈ (Nat.card H).divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑(Nat.card (powerTraceRangeSolutions leftTrace rightTrace leftExponent x.1)) = ↑(traceExactOrderSolutions leftTrace rightTrace leftExponent (Nat.card H)).card

Published equation (35): the exact-order trace count is the Möbius-weighted sum of the counts on right power-map images.

def BGS.Markoff.powerTraceRangeSolutionsSwapEquiv {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent rightExponent : ℕ) : powerTraceRangeSolutions leftTrace rightTrace leftExponent rightExponent ≃ powerTraceRangeSolutions rightTrace leftTrace rightExponent leftExponent

Swapping the two coordinates preserves a power-range trace equation.

Equations

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

theorem BGS.Markoff.natCard_powerTraceRangeSolutions_swap {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent rightExponent : ℕ) : Nat.card (powerTraceRangeSolutions leftTrace rightTrace leftExponent rightExponent) = Nat.card (powerTraceRangeSolutions rightTrace leftTrace rightExponent leftExponent)

theorem BGS.Markoff.card_divisorsAntidiagonal_eq_card_divisors (n : ℕ) : n.divisorsAntidiagonal.card = n.divisors.card

The number of divisor-antidiagonal pairs equals the number of divisors.

theorem BGS.Markoff.abs_moebius_weighted_sum_sub_le_divisors_card_mul (n : ℕ) (count mainTerm : ℕ × ℕ → ℝ) (error : ℝ) (hterm : ∀ x ∈ n.divisorsAntidiagonal, |count x - mainTerm x| ≤ error) : |∑ x ∈ n.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * count x - ∑ x ∈ n.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * mainTerm x| ≤ ↑n.divisors.card * error

Summing individually bounded errors with Möbius coefficients costs at most the divisor count.

theorem BGS.Markoff.traceExactOrderSolutions_card_error_le_moebiusMain {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] [IsCyclic H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent : ℕ) (mainTerm : ℕ → ℝ) (error : ℝ) (hRange : ∀ (d : ℕ), d ∣ Nat.card H → 0 < d → |↑(Nat.card (powerTraceRangeSolutions leftTrace rightTrace leftExponent d)) - mainTerm d| ≤ error) : |↑(traceExactOrderSolutions leftTrace rightTrace leftExponent (Nat.card H)).card - ∑ x ∈ (Nat.card H).divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * mainTerm x.1| ≤ ↑(Nat.card H).divisors.card * error

Equation (36), before simplifying its main term: pointwise range-count estimates give a divisor-count error envelope for the primitive trace count.

theorem BGS.Markoff.traceExactOrderSolutions_nonempty_of_divisorsError_lt_moebiusMain {G : Type u_1} {H : Type u_2} {T : Type u_3} [CommGroup G] [CommGroup H] [Finite G] [Finite H] [IsCyclic H] (leftTrace : G → T) (rightTrace : H → T) (leftExponent : ℕ) (mainTerm : ℕ → ℝ) (error : ℝ) (hRange : ∀ (d : ℕ), d ∣ Nat.card H → 0 < d → |↑(Nat.card (powerTraceRangeSolutions leftTrace rightTrace leftExponent d)) - mainTerm d| ≤ error) (hpositive : ↑(Nat.card H).divisors.card * error < ∑ x ∈ (Nat.card H).divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * mainTerm x.1) : (traceExactOrderSolutions leftTrace rightTrace leftExponent (Nat.card H)).Nonempty

A positive Möbius main term larger than the error envelope forces an actual primitive trace solution.

noncomputable def BGS.Markoff.primitiveTraceMoebiusMainTerm (groupOrder fieldCard fixedExponent : ℕ) : ℝ

The common Möbius main term for a field of size fieldCard, a fixed power exponent, and a primitive target group of order groupOrder.

Equations

• BGS.Markoff.primitiveTraceMoebiusMainTerm groupOrder fieldCard fixedExponent = ∑ x ∈ groupOrder.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * (↑fieldCard / (↑x.1 * ↑fixedExponent))

theorem BGS.Markoff.sum_moebius_mul_complementaryDivisor_eq_totient (n : ℕ) (hn : 0 < n) : ∑ x ∈ n.divisorsAntidiagonal, ArithmeticFunction.moebius x.1 * ↑x.2 = ↑n.totient

Möbius inversion of sum_totient: the signed complementary-divisor sum is the totient.

theorem BGS.Markoff.primitiveTraceMoebiusMainTerm_eq_totient (groupOrder fieldCard fixedExponent : ℕ) (hgroup : 0 < groupOrder) (hfixed : 0 < fixedExponent) : primitiveTraceMoebiusMainTerm groupOrder fieldCard fixedExponent = ↑fieldCard * ↑groupOrder.totient / (↑fixedExponent * ↑groupOrder)

Closed form of the primitive-trace Möbius main term.

theorem BGS.Markoff.le_totient_mul_card_divisors (n : ℕ) (hn : 0 < n) : n ≤ n.totient * n.divisors.card

The totient times the divisor count dominates the integer itself.

theorem BGS.Markoff.fieldCard_div_fixed_mul_divisors_le_primitiveTraceMoebiusMainTerm (groupOrder fieldCard fixedExponent : ℕ) (hgroup : 0 < groupOrder) (hfixed : 0 < fixedExponent) : ↑fieldCard / (↑fixedExponent * ↑groupOrder.divisors.card) ≤ primitiveTraceMoebiusMainTerm groupOrder fieldCard fixedExponent

The elementary lower envelope for the Möbius main term used in the endgame.

theorem BGS.Markoff.divisorsError_lt_primitiveTraceMoebiusMainTerm_of_explicitInequality (groupOrder fieldCard fixedExponent coefficient : ℕ) (hgroup : 0 < groupOrder) (hfixed : 0 < fixedExponent) (hexplicit : ↑fixedExponent * ↑groupOrder.divisors.card ^ 2 * (↑coefficient * √↑fieldCard) < ↑fieldCard) : ↑groupOrder.divisors.card * (↑coefficient * √↑fieldCard) < primitiveTraceMoebiusMainTerm groupOrder fieldCard fixedExponent

The explicit inequality used after the divisor bound is sufficient for primitive-trace positivity.

theorem BGS.Markoff.eventually_endgamePrimitiveTrace_explicitInequality (coefficient : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ (orbitExponent : ℕ), ↑orbitExponent ≤ ↑p ^ (1 / 2 - δ) → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Uniformly for large p, an orbit exponent at most p^(1/2-δ) satisfies the explicit primitive-trace inequality. This is the asymptotic calculation behind the last sentence after published equation (36).

theorem BGS.Markoff.exists_threshold_endgamePrimitiveTrace_explicitInequality (coefficient : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ (orbitExponent : ℕ), ↑orbitExponent ≤ ↑p ^ (1 / 2 - δ) → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Threshold form of eventually_endgamePrimitiveTrace_explicitInequality.

theorem BGS.Markoff.orbitExponent_le_rpow_of_mul_order_eq_card_sub_one (p orbitExponent orbitOrder : ℕ) {δ : ℝ} (hp : 0 < p) (hmul : orbitExponent * orbitOrder = p - 1) (horder : ↑p ^ (1 / 2 + δ) ≤ ↑orbitOrder) : ↑orbitExponent ≤ ↑p ^ (1 / 2 - δ)

A large orbit order gives the upper bound on its complementary power exponent used by the primitive-trace asymptotic.

theorem BGS.Markoff.orbitExponent_le_two_mul_rpow_of_mul_order_eq_card_add_one (p orbitExponent orbitOrder : ℕ) {δ : ℝ} (hp : 0 < p) (hmul : orbitExponent * orbitOrder = p + 1) (horder : ↑p ^ (1 / 2 + δ) ≤ ↑orbitOrder) : ↑orbitExponent ≤ 2 * ↑p ^ (1 / 2 - δ)

In the nonsplit torus, whose order is p + 1, a large orbit gives the same complementary exponent bound up to the harmless fixed factor two.

theorem BGS.Markoff.exists_threshold_endgamePrimitiveTrace_explicitInequality_of_largeNonsplitOrder (coefficient : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ (orbitExponent orbitOrder : ℕ), orbitExponent * orbitOrder = p + 1 → ↑p ^ (1 / 2 + δ) ≤ ↑orbitOrder → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Nonsplit threshold form: a complementary exponent in the norm-one torus of order p + 1 satisfies the same primitive-trace inequality for all sufficiently large p.

theorem BGS.Markoff.exists_threshold_endgamePrimitiveTrace_explicitInequality_of_largeOrder (coefficient : ℕ) {δ : ℝ} (hδ : 0 < δ) : ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ (orbitExponent orbitOrder : ℕ), orbitExponent * orbitOrder = p - 1 → ↑p ^ (1 / 2 + δ) ≤ ↑orbitOrder → ↑orbitExponent * ↑(p - 1).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p

Threshold form directly in terms of the large orbit order and its complementary exponent.

theorem BGS.Markoff.finset_nonempty_of_card_error_le_and_error_lt_main {α : Type u_4} (s : Finset α) (mainTerm error : ℝ) (henvelope : |↑s.card - mainTerm| ≤ error) (hpositive : error < mainTerm) : s.Nonempty

A numerical main-term domination criterion turns a point-count envelope into nonemptiness.

@[reducible, inline]

noncomputable abbrev BGS.Markoff.splitPrimitiveTraceSolutions (p : ℕ) [Fact (Nat.Prime p)] (alpha beta : ZMod p) (orbitExponent : ℕ) : Finset (↥(powMonoidHom orbitExponent).range × (ZMod p)ˣ)

Split trace coincidences with the orbit coordinate in the fixed power image and the other coordinate primitive in the full base-field multiplicative group.

Equations

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

theorem BGS.Markoff.splitPrimitiveTraceSolutions_card_error_le_of_weilBoundAssumption (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : WeightedSplitTraceWeilBoundAssumption coefficient) (alpha beta : ZMod p) (orbitExponent : ℕ) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (horbitPositive : 0 < orbitExponent) (horbitChar : ↑orbitExponent ≠ 0) (horbitDvd : orbitExponent ∣ Nat.card (ZMod p)ˣ) : |↑(splitPrimitiveTraceSolutions p alpha beta orbitExponent).card - primitiveTraceMoebiusMainTerm (Nat.card (ZMod p)ˣ) p orbitExponent| ≤ ↑(Nat.card (ZMod p)ˣ).divisors.card * (↑coefficient * √↑p)

Published equation (36) for the split branch, with every error and multiplicity supplied by the preceding formal interfaces.

theorem BGS.Markoff.splitPrimitiveTraceSolutions_nonempty_of_moebiusMain_gt_divisorsError (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : WeightedSplitTraceWeilBoundAssumption coefficient) (alpha beta : ZMod p) (orbitExponent : ℕ) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (horbitPositive : 0 < orbitExponent) (horbitChar : ↑orbitExponent ≠ 0) (horbitDvd : orbitExponent ∣ Nat.card (ZMod p)ˣ) (hmain : ↑(Nat.card (ZMod p)ˣ).divisors.card * (↑coefficient * √↑p) < primitiveTraceMoebiusMainTerm (Nat.card (ZMod p)ˣ) p orbitExponent) : (splitPrimitiveTraceSolutions p alpha beta orbitExponent).Nonempty

Once the explicit Möbius main term dominates the accumulated Weil errors, an actual split primitive trace pair exists.

theorem BGS.Markoff.exists_splitPrimitiveTracePair_of_explicitInequality (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : WeightedSplitTraceWeilBoundAssumption coefficient) (alpha beta : ZMod p) (orbitExponent : ℕ) (halpha : alpha ≠ 0) (hbeta : beta ≠ 0) (hnondegenerate : alpha * beta ≠ 1) (horbitPositive : 0 < orbitExponent) (horbitChar : ↑orbitExponent ≠ 0) (horbitDvd : orbitExponent ∣ Nat.card (ZMod p)ˣ) (hexplicit : ↑orbitExponent * ↑(Nat.card (ZMod p)ˣ).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p) : ∃ (z : ↥(powMonoidHom orbitExponent).range × (ZMod p)ˣ), weightedSplitTorusTrace alpha beta ↑z.1 = splitTorusTrace z.2 ∧ orderOf z.2 = Nat.card (ZMod p)ˣ

The fully numerical split inclusion--exclusion criterion produces a primitive trace pair.

@[reducible, inline]

noncomputable abbrev BGS.Markoff.existingConicSeedNonsplitPrimitiveTraceSolutions (p : ℕ) [Fact (Nat.Prime p)] (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (orbitExponent : ℕ) : Finset (↥(powMonoidHom orbitExponent).range × (ZMod p)ˣ)

Corrected seeded nonsplit trace coincidences with primitive base-field right coordinate.

Equations

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

theorem BGS.Markoff.existingConicSeedNonsplitPrimitiveTraceSolutions_card_error_le_of_weilBoundAssumption (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : SeededNonsplitTraceWeilBoundAssumption coefficient) (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (orbitExponent : ℕ) (horbitPositive : 0 < orbitExponent) (horbitChar : ↑orbitExponent ≠ 0) (horbitDvd : orbitExponent ∣ Nat.card ↥(quadraticNormOneTorus p)) : |↑(existingConicSeedNonsplitPrimitiveTraceSolutions p t ht ht0 s orbitExponent).card - primitiveTraceMoebiusMainTerm (Nat.card (ZMod p)ˣ) p orbitExponent| ≤ ↑(Nat.card (ZMod p)ˣ).divisors.card * (↑coefficient * √↑p)

Published equation (36) for the corrected seeded nonsplit branch.

theorem BGS.Markoff.existingConicSeedNonsplitPrimitiveTraceSolutions_nonempty_of_moebiusMain_gt_divisorsError (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : SeededNonsplitTraceWeilBoundAssumption coefficient) (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (orbitExponent : ℕ) (horbitPositive : 0 < orbitExponent) (horbitChar : ↑orbitExponent ≠ 0) (horbitDvd : orbitExponent ∣ Nat.card ↥(quadraticNormOneTorus p)) (hmain : ↑(Nat.card (ZMod p)ˣ).divisors.card * (↑coefficient * √↑p) < primitiveTraceMoebiusMainTerm (Nat.card (ZMod p)ˣ) p orbitExponent) : (existingConicSeedNonsplitPrimitiveTraceSolutions p t ht ht0 s orbitExponent).Nonempty

Numerical main-term domination produces an actual primitive base-field trace pair in the corrected nonsplit branch.

theorem BGS.Markoff.exists_existingConicSeedNonsplitPrimitiveTracePair_of_explicitInequality (p : ℕ) [Fact (Nat.Prime p)] (coefficient : ℕ) (hWeil : SeededNonsplitTraceWeilBoundAssumption coefficient) (hpTwo : p ≠ 2) (t : ZMod p) (ht : t ^ 2 ≠ 4) (ht0 : t ≠ 0) (s : ↑(quadraticConicNormFiber p t ht ht0)) (orbitExponent : ℕ) (horbitPositive : 0 < orbitExponent) (horbitChar : ↑orbitExponent ≠ 0) (horbitDvd : orbitExponent ∣ Nat.card ↥(quadraticNormOneTorus p)) (hexplicit : ↑orbitExponent * ↑(Nat.card (ZMod p)ˣ).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p) : ∃ (z : ↥(powMonoidHom orbitExponent).range × (ZMod p)ˣ), existingConicSeedNonsplitTorusTrace p t ht ht0 s ↑z.1 = splitTorusTrace z.2 ∧ orderOf z.2 = Nat.card (ZMod p)ˣ

The fully numerical nonsplit inclusion--exclusion criterion produces a primitive base-field trace pair on the corrected seeded norm-one orbit.