Documentation

LeanPool.MarkoffModP.BGS.Markoff.Assembly.PuncturedSmallOrderCount

Small-order counts on the punctured Markoff surface #

This module transports the normalized small-order set through the core punctured-normalization equivalence. Keeping these finite-set estimates here prevents the core equivalence module from depending on the giant-orbit counting layer.

source
noncomputable def BGS.Markoff.normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders (p : ℕ) [Fact (Nat.Prime p)] (bound : ℕ) :
Finset ↑(normalizedPuncturedSurface (ZMod p))

The canonical small-order set, restricted to the normalized punctured surface.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem BGS.Markoff.mem_normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders_iff {p : ℕ} [Fact (Nat.Prime p)] {bound : ℕ} {x : ↑(normalizedPuncturedSurface (ZMod p))} :
    x ∈ normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound ↔ rotationOrder (↑x).u1 < bound ∧ rotationOrder (↑x).u2 < bound
    source
    theorem BGS.Markoff.normalizedPuncturedSmallOrderValues_subset {p : ℕ} [Fact (Nat.Prime p)] (bound : ℕ) :
    Finset.map { toFun := Subtype.val, inj' := ⋯ } (normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound) ⊆ normalizedMarkoffPointsWithSmallFirstTwoRotationOrders p bound

    Forgetting the puncture proof embeds the normalized punctured small-order set in the canonical normalized small-order set.

    source
    theorem BGS.Markoff.normalizedPuncturedSmallOrderValues_eq_erase_origin {p : ℕ} [Fact (Nat.Prime p)] (bound : ℕ) :
    Finset.map { toFun := Subtype.val, inj' := ⋯ } (normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound) = (normalizedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).erase normalizedOrigin

    After forgetting the puncture proof, the punctured small-order set is exactly the canonical ambient small-order set with the normalized origin erased. Thus the puncture is exposed rather than silently discarded during transport.

    source
    theorem BGS.Markoff.normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders_card_le_ambient {p : ℕ} [Fact (Nat.Prime p)] (bound : ℕ) :
    (normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card ≤ (normalizedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card

    Removing the normalized origin cannot enlarge the canonical small-order set.

    source
    noncomputable def BGS.Markoff.puncturedMarkoffPointsWithSmallFirstTwoRotationOrders (p : ℕ) [Fact (Nat.Prime p)] [Invertible 3] (bound : ℕ) :
    Finset (PuncturedMarkoffSurface (ZMod p))

    Original punctured Markoff points obtained by transporting the canonical normalized punctured small-order set.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem BGS.Markoff.puncturedMarkoffPointsWithSmallFirstTwoRotationOrders_card_eq_normalized {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (bound : ℕ) :
      (puncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card = (normalizedPuncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card

      The transported original punctured set has exactly the cardinality of its normalized source.

      source
      theorem BGS.Markoff.puncturedMarkoffPointsWithSmallFirstTwoRotationOrders_card_eq_normalized_erase_origin {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (bound : ℕ) :
      (puncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card = ((normalizedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).erase normalizedOrigin).card

      Equivalently, the transported original set has exactly the cardinality of the ambient canonical normalized small-order set after its origin is removed.

      source
      theorem BGS.Markoff.puncturedMarkoffPointsWithSmallFirstTwoRotationOrders_card_le {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (bound : ℕ) :
      (puncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card ≤ 2 * (2 + 2 * bound ^ 2) ^ 2

      The elementary normalized small-order count therefore bounds the transported finite set on the original punctured surface.

      source
      theorem BGS.Markoff.puncturedMarkoffPointsWithSmallFirstTwoRotationOrders_card_le_divisor_sensitive {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (bound : ℕ) :
      (puncturedMarkoffPointsWithSmallFirstTwoRotationOrders p bound).card ≤ 2 * (2 + (bound - 1) * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 2

      The divisor-sensitive normalized count also bounds the transported punctured set.

      source
      theorem BGS.Markoff.puncturedMarkoffPointsWithSmallFirstTwoRotationOrders_succ_card_le_divisor_sensitive {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (hpTwo : p ≠ 2) (d : ℕ) :
      (puncturedMarkoffPointsWithSmallFirstTwoRotationOrders p (d + 1)).card ≤ 2 * (2 + d * ((p - 1).divisors.card + (p + 1).divisors.card)) ^ 2