Explicit strong approximation

The explicit punctured-transitivity theorem, together with natural Markoff connectivity, gives surjectivity of reduction from natural-number Markoff solutions.

theorem BGS.Markoff.markoffReduction_surjective_of_concreteExplicitBound (p : ℕ) (hpPrime : Nat.Prime p) (hp : 2 ^ 9 * (48 ^ 3 + 1) ^ 18 * (2 ^ 9 * (9 ^ 9) ^ 2 ^ 9) ^ 8 + 1 ≤ p) : Function.Surjective (markoffReduction p)

Explicit strong approximation in its source-faithful form. For every prime above the closed cutoff, every Markoff solution modulo p is the reduction of a natural-number solution.

theorem BGS.Markoff.markoffReduction_surjective_of_concretePreliminaryBound (p : ℕ) (hpPrime : Nat.Prime p) (hp : 2 ^ 1833 * (48 ^ 3 + 1) ^ 10 + 1 ≤ p) : Function.Surjective (markoffReduction p)

Strong approximation obtained from the elementary preliminary route.

theorem BGS.Markoff.reduction_surjective_of_explicitBound : have p₀ := 35721 ^ 5 * 2 ^ 1547 * 32769 ^ 2 + 1; ∀ (p : ℕ), Nat.Prime p → p₀ ≤ p → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Markoff.map (CommSemiRingCat.ofHom (Nat.castRingHom (ZMod p)))))

The weighted certificate-free Euler-seven coarse-support theorem in the functor presentation used by the Comparator challenge.