Unconditional BGS assembly

The closed function-field Hasse--Weil theorem now supplies the general affine plane-curve estimate used by the split, nonsplit, and cage arguments. These short wrappers close the final parameter of the existing BGS assembly.

theorem BGS.Markoff.theoremOneStatement : TheoremOneStatement

BGS Theorem 1, with both Corvaja--Zannier and affine Hasse--Weil discharged in the repository.

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

The eventual form of BGS Conjecture 1: strong approximation holds at every sufficiently large prime.

theorem BGS.Markoff.theoremTwoStatement : TheoremTwoStatement

BGS Theorem 2, obtained from the unconditional Theorem 1 and Chen's orbit-divisibility theorem, using Martin's later elementary proof.