Documentation

LeanPool.MarkoffModP.BGS.Markoff.Cage.HasseWeilAssumption

Explicit Hasse--Weil interface for the cage #

The external input is a point-count estimate on the actual finite set used by the cage inclusion--exclusion. Connectivity and primitive extraction are not assumed here.

source
def BGS.Markoff.IsSplitMaximalTrace (p : ℕ) (t : ZMod p) :
Prop

The selected cage core consists of split-maximal normalized traces. This is sufficient for Theorem 1 because the endgame constructed in this repository always reaches order p - 1.

Equations
Instances For
    source
    def BGS.Markoff.cageBridgeAxis :
    NormalizedCoordinateAxis → NormalizedCoordinateAxis → NormalizedCoordinateAxis

    Choose an axis different from both prescribed axes.

    Equations
    Instances For
      source
      theorem BGS.Markoff.cageBridgeAxis_ne_left (axis other : NormalizedCoordinateAxis) :
      cageBridgeAxis axis other ≠ axis
      source
      theorem BGS.Markoff.cageBridgeAxis_ne_right (axis other : NormalizedCoordinateAxis) :
      cageBridgeAxis axis other ≠ other
      source
      def BGS.Markoff.normalizedCoordinateAt (axis : NormalizedCoordinateAxis) {R : Type u_1} (x : NormalizedPoint R) :
      R

      Coordinate selected by an axis label.

      Equations
      Instances For
        source
        theorem BGS.Markoff.mem_normalizedFiberAt_iff {R : Type u_1} [CommRing R] {axis : NormalizedCoordinateAxis} {t : R} {x : NormalizedPoint R} :
        x ∈ normalizedFiberAt axis t ↔ IsNormalizedMarkoff x ∧ normalizedCoordinateAt axis x = t
        source
        def BGS.Markoff.CageMiddleTraceRelation (p : ℕ) [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) (u : (ZMod p)ˣ) :
        Prop

        The concrete incidence condition counted by the cage fiber-product curve.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def BGS.Markoff.CageMiddleWitnessPair (p : ℕ) (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) :
          Type

          A pair of actual intersection witnesses over a common middle trace.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def BGS.Markoff.cageMiddleWitnessTrace {p : ℕ} {axis other : NormalizedCoordinateAxis} {xi eta : ZMod p} (z : CageMiddleWitnessPair p axis other xi eta) :
            ZMod p

            The common middle coordinate of a witness pair.

            Equations
            Instances For
              source
              @[reducible, inline]
              abbrev BGS.Markoff.cageMiddleWitnessPowerRangeSolutions (p : ℕ) [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) (d : ℕ) :
              Type

              Witness-bearing solutions with the middle unit restricted to a power-map image.

              Equations
              Instances For
                source
                def BGS.Markoff.CageWitnessPointEstimate (coefficient : ℕ) :
                Prop

                Witness-bearing cage point-count target with the geometric component multiplicity exposed. The generic fiber product has multiplicity one, while the diagonal degeneration can have a larger main term. Requiring a single positive multiplicity for all divisor ranges is exactly what Möbius inversion needs; fixing it silently to one would make this statement false.

                This is not an allowed external assumption: it must ultimately be derived from the one general Hasse--Weil theorem.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem BGS.Markoff.exists_primitive_cageMiddleUnit_of_explicitInequality (coefficient : ℕ) (hHasse : CageWitnessPointEstimate coefficient) (p : ℕ) [Fact (Nat.Prime p)] (hpFive : 5 ≤ p) (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) (hxi : IsSplitMaximalTrace p xi) (heta : IsSplitMaximalTrace p eta) (hexplicit : ↑(Nat.card (ZMod p)ˣ).divisors.card ^ 2 * (↑coefficient * √↑p) < ↑p) :
                  ∃ (u : (ZMod p)ˣ), CageMiddleTraceRelation p axis other xi eta u ∧ orderOf u = Nat.card (ZMod p)ˣ

                  The Hasse--Weil range estimates imply a primitive middle unit once the explicit divisor error is smaller than the Möbius main term.

                  source
                  theorem BGS.Markoff.exists_threshold_primitive_cageMiddleUnit (coefficient : ℕ) (hHasse : CageWitnessPointEstimate coefficient) :
                  ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [inst : Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p), IsSplitMaximalTrace p xi → IsSplitMaximalTrace p eta → ∃ (u : (ZMod p)ˣ), CageMiddleTraceRelation p axis other xi eta u ∧ orderOf u = Nat.card (ZMod p)ˣ

                  Uniform large-prime form of the primitive cage bridge.

                  source
                  theorem BGS.Markoff.exists_threshold_splitMaximalFiberBridge (coefficient : ℕ) (hHasse : CageWitnessPointEstimate coefficient) :
                  ∃ (threshold : ℕ), ∀ (p : ℕ), threshold ≤ p → ∀ [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p), IsSplitMaximalTrace p xi → IsSplitMaximalTrace p eta → ∃ (middle : NormalizedCoordinateAxis) (y : ZMod p), middle ≠ axis ∧ middle ≠ other ∧ IsSplitMaximalTrace p y ∧ NormalizedFibersMeet (normalizedFiberAt axis xi) (normalizedFiberAt middle y) ∧ NormalizedFibersMeet (normalizedFiberAt other eta) (normalizedFiberAt middle y)

                  The primitive-incidence bridge derived from the Hasse--Weil count and Möbius inversion.