Documentation

LeanPool.MarkoffModP.BGS.Markoff.Cage.Connectivity

Connectivity of the selected split cage #

source
def BGS.Markoff.IsInSplitCage (p : ℕ) (x : NormalizedMarkoffSurface (ZMod p)) :
Prop

Membership in the selected split cage core.

Equations
Instances For
    source
    theorem BGS.Markoff.mem_normalizedFiberAt_coordinate {R : Type u_1} [CommRing R] (axis : NormalizedCoordinateAxis) (x : NormalizedMarkoffSurface R) :
    ↑x ∈ normalizedFiberAt axis (normalizedCoordinateAt axis ↑x)
    source
    theorem BGS.Markoff.isNormalizedMarkoff_of_mem_normalizedFiberAt {R : Type u_1} [CommRing R] {axis : NormalizedCoordinateAxis} {t : R} {x : NormalizedPoint R} (hx : x ∈ normalizedFiberAt axis t) :
    IsNormalizedMarkoff x
    source
    theorem BGS.Markoff.sameNormalizedComponent_of_mem_splitMaximal_firstFiber (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSeven : 7 ≤ p) (t : ZMod p) (hmax : IsSplitMaximalTrace p t) (x y : ↑(normalizedFiber1 t)) :
    SameNormalizedComponent ⟨↑x, ⋯⟩ ⟨↑y, ⋯⟩

    On a split-maximal first-coordinate fiber, the normalized rotation is transitive.

    source
    theorem BGS.Markoff.sameNormalizedComponent_of_mem_same_splitMaximalFiber (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (hpSeven : 7 ≤ p) (axis : NormalizedCoordinateAxis) (t : ZMod p) (hmax : IsSplitMaximalTrace p t) (x y : NormalizedMarkoffSurface (ZMod p)) (hx : ↑x ∈ normalizedFiberAt axis t) (hy : ↑y ∈ normalizedFiberAt axis t) :
    SameNormalizedComponent x y

    Any two normalized surface points in the same split-maximal fiber, on any coordinate axis, lie in the same Markoff component.

    source
    theorem BGS.Markoff.exists_threshold_splitCage_connected (coefficient : ℕ) (hHasse : CageWitnessPointEstimate coefficient) :
    ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (hpThree : p ≠ 3) (x y : NormalizedMarkoffSurface (ZMod p)), IsInSplitCage p x → IsInSplitCage p y → SameNormalizedComponent x y

    The selected split cage is connected for all sufficiently large primes, relative only to the explicit cage Hasse--Weil count assumption.

    source
    theorem BGS.Markoff.exists_threshold_largeOrder_to_splitCage (splitCoefficient : ℕ) (hSplitWeil : WeightedSplitTraceWeilBoundAssumption splitCoefficient) (nonsplitCoefficient : ℕ) (hNonsplitWeil : SeededNonsplitTraceWeilBoundAssumption nonsplitCoefficient) {δ : ℝ} (hδ : 0 < δ) :
    ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (hpThree : p ≠ 3) (x : NormalizedMarkoffSurface (ZMod p)), ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder (↑x).u1) ∨ ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder (↑x).u2) ∨ ↑p ^ (1 / 2 + δ) ≤ ↑(rotationOrder (↑x).u3) → ∃ (y : NormalizedMarkoffSurface (ZMod p)), SameNormalizedComponent x y ∧ IsInSplitCage p y

    The completed endgame lands in the selected split cage core.