Root-free joint maximal-divisor frontier

The improved arithmetic naturally controls the square of the sum of the two maximal-divisor counts. This module keeps that square envelope intact instead of taking an integer square root and losing information.

theorem BGS.Markoff.coefficient_mul_count_cube_lt_of_squareEnvelope {coefficient count envelope order : ℕ} (hsquare : count ^ 2 ≤ envelope) (hstrict : coefficient ^ 6 * envelope ^ 3 < order ^ 2) : (coefficient * count) ^ 3 < order

A square envelope converts a root-free sixth-power comparison into the cube inequality required by the middle game.

theorem BGS.Markoff.coefficient_mul_count_mul_order_lt_of_squareEnvelope {coefficient count envelope order p : ℕ} (hsquare : count ^ 2 ≤ envelope) (hstrict : coefficient ^ 2 * envelope * order ^ 2 < p ^ 2) : coefficient * count * order < p

A square envelope also converts the linear middle-game comparison into a root-free quadratic comparison.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_jointSquareEnvelope_frontier (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (squareEnvelope : ℕ → ℕ) (hsquare : ∀ (d : ℕ), maximalDivisorCountSum p (d + 1) ^ 2 ≤ squareEnvelope d) (hcube : ∀ (d : ℕ), 0 < d → p ≤ 2 * (2 + d * maximalDivisorCountSum p (d + 1)) ^ 2 → corvajaZannierCorollaryTwoSafeCoefficient ^ 6 * squareEnvelope d ^ 3 < d ^ 2) (hlinear : ∀ (d : ℕ), ↑d < ↑p ^ (5 / 6) → corvajaZannierCorollaryTwoSafeCoefficient ^ 2 * squareEnvelope d * d ^ 2 < p ^ 2) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : PuncturedMarkoffTransitiveAt p

Punctured transitivity from a square envelope for the two neighboring maximal-divisor counts. Both numerical hypotheses are polynomial inequalities over natural numbers.

theorem BGS.Markoff.puncturedMarkoffTransitiveAt_of_jointMaximalDivisorBounds (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpThree : 3 < p) (c : PuncturedMarkoffSurface (ZMod p)) (central productEnvelope : ℕ → ℕ) (hminus : ∀ (d : ℕ), (NumberTheory.maximalDivisorsBelow (p - 1) (d + 1)).card ≤ central d) (hplus : ∀ (d : ℕ), (NumberTheory.maximalDivisorsBelow (p + 1) (d + 1)).card ≤ central d) (hproduct : ∀ (d : ℕ), (NumberTheory.maximalDivisorsBelow (p - 1) (d + 1)).card * (NumberTheory.maximalDivisorsBelow (p + 1) (d + 1)).card ≤ productEnvelope d) (hcube : ∀ (d : ℕ), 0 < d → p ≤ 2 * (2 + d * maximalDivisorCountSum p (d + 1)) ^ 2 → corvajaZannierCorollaryTwoSafeCoefficient ^ 6 * (central d ^ 2 + 3 * productEnvelope d) ^ 3 < d ^ 2) (hlinear : ∀ (d : ℕ), ↑d < ↑p ^ (5 / 6) → corvajaZannierCorollaryTwoSafeCoefficient ^ 2 * (central d ^ 2 + 3 * productEnvelope d) * d ^ 2 < p ^ 2) (hlarge : ∀ (z : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (5 / 6) ≤ ↑(maximalCoordinateRotationOrder ↑z) → SameNormalizedComponent (normalizedSurfaceOfPunctured ((puncturedNormalizationEquiv (ZMod p)) c)) z) : PuncturedMarkoffTransitiveAt p

Specialization of the square-envelope frontier to the new C^2 + 3J bound.