Exceptional-prime consequences of Chen orbit divisibility

Chen's component-divisibility theorem, formalized here through Martin's later elementary proof, upgrades the giant-orbit half of Theorem 1 to strong approximation at every sufficiently large prime. This file records the resulting finite exceptional-prime set and derives the subpower exceptional-prime bound of Theorem 2.

theorem BGS.Markoff.exceptionalPrimeCount_le_of_eventually_strongApproximationAt (p0 : ℕ) (hstrong : ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → StrongApproximationAt p) (T : ℕ) : exceptionalPrimeCount T ≤ p0

If strong approximation holds at every prime beyond p0, then at most p0 primes are exceptional below any cutoff.

theorem BGS.Markoff.theoremTwoStatement_of_eventually_strongApproximationAt (hstrong : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → StrongApproximationAt p) : TheoremTwoStatement

Eventual strong approximation implies the subpower exceptional-prime estimate of TheoremTwoStatement.

theorem BGS.Markoff.eventually_puncturedMarkoffTransitiveAt_of_theoremOneStatement (hOne : TheoremOneStatement) : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → PuncturedMarkoffTransitiveAt p

The giant-orbit half of Theorem 1 and Chen orbit divisibility, via Martin's proof, imply eventual punctured finite-field transitivity.

theorem BGS.Markoff.eventually_strongApproximationAt_of_theoremOneStatement (hOne : TheoremOneStatement) : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → StrongApproximationAt p

Theorem 1 and Chen orbit divisibility, through Martin's proof, imply eventual strong approximation after applying natural Markoff connectivity.

theorem BGS.Markoff.eventually_strongApproximationAt_of_generalHasseWeil (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) : ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → StrongApproximationAt p

The general-interface form of eventual BGS Conjecture 1.

Theorem 1 and Chen's orbit-divisibility theorem, via Martin's proof, imply strong approximation at every sufficiently large prime. The parameter-free endpoint is BGS.Markoff.eventually_strongApproximationAt.

theorem BGS.Markoff.theoremTwoStatement_of_theoremOneStatement (hOne : TheoremOneStatement) : TheoremTwoStatement

Theorem 1 together with Chen's orbit-divisibility theorem, via Martin's elementary proof, implies Theorem 2.

theorem BGS.Markoff.theoremTwoStatement_of_generalHasseWeil (hHasse : External.GeneralBivariateAffineHasseWeilTheorem) : TheoremTwoStatement

The general-interface form of BGS Theorem 2.

The completed Theorem 1 assembly supplies the in-repository Corvaja--Zannier estimate. The parameter-free endpoint is BGS.Markoff.theoremTwoStatement.