Documentation

LeanPool.MarkoffModP.BGS.Markoff.Incidence.NormalizedGraph

The normalized incidence graph and its parabolic vertices #

The published proof of Proposition 8 dismisses the case p ≡ 1 (mod 4) as simpler because of the parabolic lines. This file records the missing argument without folding normalized trace coordinates back into the original Markoff coordinates.

The key fact is stronger than mere connectivity: after choosing i² = -1, a fiber whose normalized coordinate is 2 or -2 meets every fiber on either different coordinate axis.

source
inductive BGS.Markoff.NormalizedCoordinateAxis :
Type

The three coordinate axes used to index normalized conic fibers.

Instances For
    source
    @[instance_reducible]
    instance BGS.Markoff.instDecidableEqNormalizedCoordinateAxis :
    DecidableEq NormalizedCoordinateAxis
    Equations
    source
    @[instance_reducible]
    instance BGS.Markoff.instReprNormalizedCoordinateAxis :
    Repr NormalizedCoordinateAxis
    Equations
    source
    def BGS.Markoff.instReprNormalizedCoordinateAxis.repr :
    NormalizedCoordinateAxis → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance BGS.Markoff.instFintypeNormalizedCoordinateAxis :
      Fintype NormalizedCoordinateAxis
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def BGS.Markoff.normalizedFiberAt {R : Type u} [CommRing R] :
      NormalizedCoordinateAxis → R → Set (NormalizedPoint R)

      A normalized conic fiber, indexed without identifying normalized and original coordinates.

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

        The action of swapping the first two coordinates on axis labels.

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

          The action of swapping the last two coordinates on axis labels.

          Equations
          Instances For
            source
            theorem BGS.Markoff.normalizedSwap12_mem_fiberAt {R : Type u} [CommRing R] {axis : NormalizedCoordinateAxis} {a : R} {x : NormalizedPoint R} (hx : x ∈ normalizedFiberAt axis a) :
            normalizedSwap12 x ∈ normalizedFiberAt (normalizedSwap12Axis axis) a
            source
            theorem BGS.Markoff.normalizedSwap23_mem_fiberAt {R : Type u} [CommRing R] {axis : NormalizedCoordinateAxis} {a : R} {x : NormalizedPoint R} (hx : x ∈ normalizedFiberAt axis a) :
            normalizedSwap23 x ∈ normalizedFiberAt (normalizedSwap23Axis axis) a
            source
            def BGS.Markoff.NormalizedFibersMeet {R : Type u} (s t : Set (NormalizedPoint R)) :
            Prop

            Two normalized conic fibers meet when their set-theoretic intersection is nonempty.

            Equations
            Instances For
              source
              theorem BGS.Markoff.normalizedFibersMeet_comm {R : Type u} {s t : Set (NormalizedPoint R)} :
              NormalizedFibersMeet s t ↔ NormalizedFibersMeet t s
              source
              theorem BGS.Markoff.normalizedFibersMeet_swap12 {R : Type u} [CommRing R] {axis other : NormalizedCoordinateAxis} {a b : R} (h : NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt other b)) :
              NormalizedFibersMeet (normalizedFiberAt (normalizedSwap12Axis axis) a) (normalizedFiberAt (normalizedSwap12Axis other) b)

              Coordinate swapping transports a meeting of normalized fibers.

              source
              theorem BGS.Markoff.normalizedFibersMeet_swap23 {R : Type u} [CommRing R] {axis other : NormalizedCoordinateAxis} {a b : R} (h : NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt other b)) :
              NormalizedFibersMeet (normalizedFiberAt (normalizedSwap23Axis axis) a) (normalizedFiberAt (normalizedSwap23Axis other) b)

              Swapping the last two coordinates transports a meeting of normalized fibers.

              source
              def BGS.Markoff.IsNormalizedParabolicCoordinate {R : Type u} [OfNat R 4] [Pow R ℕ] (a : R) :
              Prop

              The intrinsic normalized-coordinate condition for a parabolic trace.

              Equations
              Instances For
                source
                def BGS.Markoff.IsNormalizedExceptionalCoordinate {R : Type u} [OfNat R 0] [OfNat R 4] [Pow R ℕ] (a : R) :
                Prop

                The normalized coordinates excluded by the existing admissible-incidence argument.

                Equations
                Instances For
                  source
                  def BGS.Markoff.unscaleNormalizedCoordinate {R : Type u} [CommRing R] [Invertible 3] (u : R) :
                  R

                  Divide a normalized trace coordinate by three without identifying its type with an original Markoff coordinate.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem BGS.Markoff.three_mul_unscaleNormalizedCoordinate {R : Type u} [CommRing R] [Invertible 3] (u : R) :
                    3 * unscaleNormalizedCoordinate u = u
                    source
                    @[simp]
                    theorem BGS.Markoff.unscaleNormalizedCoordinate_three_mul {R : Type u} [CommRing R] [Invertible 3] (a : R) :
                    unscaleNormalizedCoordinate (3 * a) = a
                    source
                    theorem BGS.Markoff.isAdmissibleCoordinate_unscaleNormalizedCoordinate_iff {p : ℕ} [Fact (Nat.Prime p)] [Invertible 3] (u : ZMod p) :
                    IsAdmissibleCoordinate (unscaleNormalizedCoordinate u) ↔ ¬IsNormalizedExceptionalCoordinate u

                    Original-coordinate admissibility is exactly the complement of the zero and parabolic normalized trace values.

                    source
                    theorem BGS.Markoff.normalizedFibersMeet_fiber1_fiber3_of_original {R : Type u} [Field R] [Invertible 3] {a c : R} (h : FibersMeet (fiber1 a) (fiber3 c)) :
                    NormalizedFibersMeet (normalizedFiber1 (3 * a)) (normalizedFiber3 (3 * c))

                    Scaling a meeting of an original first-axis and third-axis fiber gives the corresponding meeting in normalized trace coordinates.

                    source
                    theorem BGS.Markoff.normalizedFibersMeet_fiber2_fiber3_of_original {R : Type u} [Field R] [Invertible 3] {b c : R} (h : FibersMeet (fiber2 b) (fiber3 c)) :
                    NormalizedFibersMeet (normalizedFiber2 (3 * b)) (normalizedFiber3 (3 * c))

                    Scaling a meeting of an original second-axis and third-axis fiber gives the corresponding meeting in normalized trace coordinates.

                    source
                    def BGS.Markoff.NormalizedAdmissibleBridgeAt (p : ℕ) (hp : Nat.Prime p) :
                    Prop

                    The normalized, type-distinct form of the existing admissible bridge for the first two axes.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem BGS.Markoff.normalizedAdmissibleBridgeAt_of_incidenceBridgeAt (p : ℕ) (hp : Nat.Prime p) [Invertible 3] (hbridge : IncidenceBridgeAt p hp) :
                      NormalizedAdmissibleBridgeAt p hp

                      Transport the proved original-coordinate admissible bridge through the explicit scaling equivalence.

                      source
                      theorem BGS.Markoff.normalizedAdmissibleBridge_mod_one (hHasse : ZModLegendrePointCardHasseBound) :
                      ∃ (p0 : ℕ), ∀ (p : ℕ) (hp : Nat.Prime p), p0 ≤ p → p % 4 = 1 → NormalizedAdmissibleBridgeAt p hp

                      The normalized admissible bridge for primes congruent to one modulo four.

                      source
                      def BGS.Markoff.NormalizedAdmissibleGraphBridgeAt (p : ℕ) (hp : Nat.Prime p) :
                      Prop

                      The graph-level admissible bridge, with coordinate permutations made explicit.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem BGS.Markoff.normalizedAdmissibleGraphBridgeAt_of_fixedAxes {p : ℕ} {hp : Nat.Prime p} (hbridge : NormalizedAdmissibleBridgeAt p hp) :
                        NormalizedAdmissibleGraphBridgeAt p hp

                        The fixed-axis admissible bridge implies the full graph-level bridge. Every coordinate permutation is applied to the actual intersection witness.

                        source
                        theorem BGS.Markoff.normalizedAdmissibleGraphBridge_mod_one (hHasse : ZModLegendrePointCardHasseBound) :
                        ∃ (p0 : ℕ), ∀ (p : ℕ) (hp : Nat.Prime p), p0 ≤ p → p % 4 = 1 → NormalizedAdmissibleGraphBridgeAt p hp

                        The graph-level admissible bridge for all sufficiently large primes congruent to one modulo four.

                        source
                        theorem BGS.Markoff.normalizedFiber1_two_meets_fiber2 {R : Type u} [CommRing R] [NoZeroDivisors R] (i b : R) (hi : i ^ 2 = -1) :
                        NormalizedFibersMeet (normalizedFiber1 2) (normalizedFiber2 b)

                        The trace-2 fiber on the first axis meets every second-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedFiber1_neg_two_meets_fiber2 {R : Type u} [CommRing R] [NoZeroDivisors R] (i b : R) (hi : i ^ 2 = -1) :
                        NormalizedFibersMeet (normalizedFiber1 (-2)) (normalizedFiber2 b)

                        The trace--2 fiber on the first axis meets every second-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedFiber1_parabolic_meets_fiber2 {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) {a : R} (ha : IsNormalizedParabolicCoordinate a) (b : R) :
                        NormalizedFibersMeet (normalizedFiber1 a) (normalizedFiber2 b)

                        A parabolic first-axis fiber meets every second-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedFiber1_two_meets_fiber3 {R : Type u} [CommRing R] [NoZeroDivisors R] (i c : R) (hi : i ^ 2 = -1) :
                        NormalizedFibersMeet (normalizedFiber1 2) (normalizedFiber3 c)

                        The trace-2 fiber on the first axis meets every third-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedFiber1_neg_two_meets_fiber3 {R : Type u} [CommRing R] [NoZeroDivisors R] (i c : R) (hi : i ^ 2 = -1) :
                        NormalizedFibersMeet (normalizedFiber1 (-2)) (normalizedFiber3 c)

                        The trace--2 fiber on the first axis meets every third-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedFiber1_parabolic_meets_fiber3 {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) {a : R} (ha : IsNormalizedParabolicCoordinate a) (c : R) :
                        NormalizedFibersMeet (normalizedFiber1 a) (normalizedFiber3 c)

                        A parabolic first-axis fiber meets every third-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedFiber1_zero_meets_fiber2 {R : Type u} [CommRing R] (i b : R) (hi : i ^ 2 = -1) :
                        NormalizedFibersMeet (normalizedFiber1 0) (normalizedFiber2 b)

                        When i² = -1, the zero fiber on the first axis meets every second-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedFiber1_zero_meets_fiber3 {R : Type u} [CommRing R] (i c : R) (hi : i ^ 2 = -1) :
                        NormalizedFibersMeet (normalizedFiber1 0) (normalizedFiber3 c)

                        When i² = -1, the zero fiber on the first axis meets every third-axis fiber.

                        source
                        theorem BGS.Markoff.normalizedParabolicFiber_meets_distinctAxis {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) {axis other : NormalizedCoordinateAxis} (haxis : axis ≠ other) {a : R} (ha : IsNormalizedParabolicCoordinate a) (b : R) :
                        NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt other b)

                        A parabolic fiber on any axis meets every fiber on a different axis.

                        source
                        theorem BGS.Markoff.normalizedZeroFiber_meets_distinctAxis {R : Type u} [CommRing R] (i : R) (hi : i ^ 2 = -1) {axis other : NormalizedCoordinateAxis} (haxis : axis ≠ other) (b : R) :
                        NormalizedFibersMeet (normalizedFiberAt axis 0) (normalizedFiberAt other b)

                        A zero-coordinate fiber meets every fiber on a different axis when -1 is a square.

                        source
                        theorem BGS.Markoff.normalizedExceptionalFiber_meets_distinctAxis {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) {axis other : NormalizedCoordinateAxis} (haxis : axis ≠ other) {a : R} (ha : IsNormalizedExceptionalCoordinate a) (b : R) :
                        NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt other b)

                        Every coordinate excluded by admissibility meets every fiber on a different axis when -1 is a square.

                        source
                        theorem BGS.Markoff.normalizedParabolicFiber_commonNeighbor_sameAxis {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) (axis other : NormalizedCoordinateAxis) (haxis : axis ≠ other) {a b : R} (ha : IsNormalizedParabolicCoordinate a) (hb : (normalizedFiberAt axis b).Nonempty) :
                        ∃ (c : R), NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt other c) ∧ NormalizedFibersMeet (normalizedFiberAt axis b) (normalizedFiberAt other c)

                        If one vertex is parabolic and the other vertex is on the same axis, any point of the other fiber supplies a common neighbor on either different axis.

                        source
                        def BGS.Markoff.normalizedBridgeAxis :
                        NormalizedCoordinateAxis → NormalizedCoordinateAxis → NormalizedCoordinateAxis

                        A deterministic choice of an axis different from each of two supplied axes.

                        Equations
                        Instances For
                          source
                          theorem BGS.Markoff.normalizedBridgeAxis_ne_left (axis other : NormalizedCoordinateAxis) :
                          normalizedBridgeAxis axis other ≠ axis
                          source
                          theorem BGS.Markoff.normalizedBridgeAxis_ne_right (axis other : NormalizedCoordinateAxis) :
                          normalizedBridgeAxis axis other ≠ other
                          source
                          theorem BGS.Markoff.normalizedFiber_meets_some_fiber_on_distinctAxis {R : Type u} [CommRing R] {axis other : NormalizedCoordinateAxis} (haxis : axis ≠ other) {b : R} (hb : (normalizedFiberAt axis b).Nonempty) :
                          ∃ (c : R), NormalizedFibersMeet (normalizedFiberAt axis b) (normalizedFiberAt other c)

                          A nonempty fiber meets some fiber on every different axis: use the corresponding coordinate of a point already in the first fiber.

                          source
                          theorem BGS.Markoff.normalizedParabolicFiber_has_commonNeighbor {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) (axis other : NormalizedCoordinateAxis) {a b : R} (ha : IsNormalizedParabolicCoordinate a) (hb : (normalizedFiberAt other b).Nonempty) :
                          ∃ (middle : NormalizedCoordinateAxis) (c : R), middle ≠ axis ∧ middle ≠ other ∧ NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt middle c) ∧ NormalizedFibersMeet (normalizedFiberAt other b) (normalizedFiberAt middle c)

                          The complete parabolic bridge suppressed by the published proof.

                          For a parabolic vertex on axis and any nonempty vertex on other, this produces a common neighbor on an axis different from both. Thus all interactions involving a parabolic vertex have graph distance at most two; no admissibility hypothesis is imposed on the other vertex.

                          source
                          theorem BGS.Markoff.normalizedExceptionalFiber_has_commonNeighbor {R : Type u} [CommRing R] [NoZeroDivisors R] (i : R) (hi : i ^ 2 = -1) (axis other : NormalizedCoordinateAxis) {a b : R} (ha : IsNormalizedExceptionalCoordinate a) (hb : (normalizedFiberAt other b).Nonempty) :
                          ∃ (middle : NormalizedCoordinateAxis) (c : R), middle ≠ axis ∧ middle ≠ other ∧ NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt middle c) ∧ NormalizedFibersMeet (normalizedFiberAt other b) (normalizedFiberAt middle c)

                          The same graph-level bridge for every coordinate omitted by the admissible argument, including the zero-coordinate lines that also occur when -1 is a square.

                          source
                          theorem BGS.Markoff.normalizedParabolicIncidenceBridge_mod_one (p : ℕ) [Fact (Nat.Prime p)] (hmod : p % 4 = 1) (axis other : NormalizedCoordinateAxis) {a b : ZMod p} :
                          IsNormalizedParabolicCoordinate a → (normalizedFiberAt other b).Nonempty → ∃ (middle : NormalizedCoordinateAxis) (c : ZMod p), middle ≠ axis ∧ middle ≠ other ∧ NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt middle c) ∧ NormalizedFibersMeet (normalizedFiberAt other b) (normalizedFiberAt middle c)

                          For primes congruent to one modulo four, every parabolic incidence vertex has a common neighbor with every nonempty incidence vertex, uniformly over all coordinate axes.

                          source
                          theorem BGS.Markoff.normalizedExceptionalIncidenceBridge_mod_one (p : ℕ) [Fact (Nat.Prime p)] (hmod : p % 4 = 1) (axis other : NormalizedCoordinateAxis) {a b : ZMod p} :
                          IsNormalizedExceptionalCoordinate a → (normalizedFiberAt other b).Nonempty → ∃ (middle : NormalizedCoordinateAxis) (c : ZMod p), middle ≠ axis ∧ middle ≠ other ∧ NormalizedFibersMeet (normalizedFiberAt axis a) (normalizedFiberAt middle c) ∧ NormalizedFibersMeet (normalizedFiberAt other b) (normalizedFiberAt middle c)

                          At primes congruent to one modulo four, the zero and parabolic fibers omitted by the admissible incidence argument all have distance at most two from every nonempty fiber.

                          source
                          def BGS.Markoff.NormalizedFullSurfaceFiberBridgeAt (p : ℕ) :
                          Prop

                          A full-surface fiber bridge. This does not yet remove the normalized origin from intersection witnesses, so it is intentionally not called the punctured incidence graph.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            theorem BGS.Markoff.normalizedFullSurfaceFiberBridge_mod_one (hHasse : ZModLegendrePointCardHasseBound) :
                            ∃ (p0 : ℕ), ∀ (p : ℕ), Nat.Prime p → p0 ≤ p → p % 4 = 1 → NormalizedFullSurfaceFiberBridgeAt p

                            The complete incidence bridge for sufficiently large primes congruent to one modulo four. The proof combines the transported admissible bridge with the separately proved zero and parabolic line geometry.