Documentation

LeanPool.MarkoffModP.BGS.Markoff.Cage.AxisEquivalence

Coordinate-axis invariance of cage witnesses #

The cage geometry is symmetric in the three normalized coordinates, but its point-count argument is written for the canonical ordered pair of outer axes (.first, .second). The two incidence witnesses are independent points, so they may be permuted independently while their common bridge coordinate is sent to the third coordinate. This file records that symmetry as an actual equivalence, retaining the common trace exactly.

source
def BGS.Markoff.normalizedSwap12Equiv (R : Type u_1) :
NormalizedPoint R ≃ NormalizedPoint R

Swapping the first two normalized coordinates as an equivalence.

Equations
Instances For
    source
    def BGS.Markoff.normalizedSwap23Equiv (R : Type u_1) :
    NormalizedPoint R ≃ NormalizedPoint R

    Swapping the last two normalized coordinates as an equivalence.

    Equations
    Instances For
      source
      def BGS.Markoff.cageFirstPointCanonicalEquiv (R : Type u_1) (axis other : NormalizedCoordinateAxis) :
      NormalizedPoint R ≃ NormalizedPoint R

      Permute the first incidence point so that its outer coordinate is first and its bridge coordinate is third.

      Equations
      Instances For
        source
        def BGS.Markoff.cageSecondPointCanonicalEquiv (R : Type u_1) (axis other : NormalizedCoordinateAxis) :
        NormalizedPoint R ≃ NormalizedPoint R

        Permute the second incidence point so that its outer coordinate is second and its bridge coordinate is third.

        Equations
        Instances For
          source
          theorem BGS.Markoff.cageFirstPointCanonical_mem {R : Type u_1} [CommRing R] (axis other : NormalizedCoordinateAxis) (xi middle : R) {x : NormalizedPoint R} (hOuter : x ∈ normalizedFiberAt axis xi) (hMiddle : normalizedCoordinateAt (cageBridgeAxis axis other) x = middle) :
          (cageFirstPointCanonicalEquiv R axis other) x ∈ normalizedFiberAt NormalizedCoordinateAxis.first xi ∧ normalizedCoordinateAt NormalizedCoordinateAxis.third ((cageFirstPointCanonicalEquiv R axis other) x) = middle

          Canonicalizing the first incidence point preserves its outer and bridge coordinates.

          source
          theorem BGS.Markoff.cageSecondPointCanonical_mem {R : Type u_1} [CommRing R] (axis other : NormalizedCoordinateAxis) (eta middle : R) {x : NormalizedPoint R} (hOuter : x ∈ normalizedFiberAt other eta) (hMiddle : normalizedCoordinateAt (cageBridgeAxis axis other) x = middle) :
          (cageSecondPointCanonicalEquiv R axis other) x ∈ normalizedFiberAt NormalizedCoordinateAxis.second eta ∧ normalizedCoordinateAt NormalizedCoordinateAxis.third ((cageSecondPointCanonicalEquiv R axis other) x) = middle

          Canonicalizing the second incidence point preserves its outer and bridge coordinates.

          source
          def BGS.Markoff.cageMiddleWitnessToCanonical (p : ℕ) (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) :
          CageMiddleWitnessPair p axis other xi eta → CageMiddleWitnessPair p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta

          Send an arbitrary ordered pair of cage axes to the canonical ordered pair. The two points are permuted independently and their common bridge coordinate becomes the common third coordinate.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def BGS.Markoff.canonicalCageMiddleWitnessToAxes (p : ℕ) [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) :
            CageMiddleWitnessPair p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta → CageMiddleWitnessPair p axis other xi eta

            The inverse coordinate permutations reconstruct a witness on the original ordered pair of axes.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def BGS.Markoff.cageMiddleWitnessEquivCanonical (p : ℕ) [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) :
              CageMiddleWitnessPair p axis other xi eta ≃ CageMiddleWitnessPair p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta

              Cage witness pairs for arbitrary axes are canonically equivalent to the first--second model used by the plane equations.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem BGS.Markoff.cageMiddleWitnessEquivCanonical_trace (p : ℕ) [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) (z : CageMiddleWitnessPair p axis other xi eta) :
                cageMiddleWitnessTrace ((cageMiddleWitnessEquivCanonical p axis other xi eta) z) = cageMiddleWitnessTrace z

                Canonicalizing the axes preserves the common middle trace exactly.

                source
                def BGS.Markoff.cageMiddleWitnessPowerRangeEquivCanonical (p : ℕ) [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) (d : ℕ) :
                cageMiddleWitnessPowerRangeSolutions p axis other xi eta d ≃ cageMiddleWitnessPowerRangeSolutions p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta d

                Axis canonicalization extends to the one-sided power-range solutions used by the cage point count.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem BGS.Markoff.natCard_cageMiddleWitnessPowerRangeSolutions_eq_canonical (p : ℕ) [Fact (Nat.Prime p)] (axis other : NormalizedCoordinateAxis) (xi eta : ZMod p) (d : ℕ) :
                  Nat.card (cageMiddleWitnessPowerRangeSolutions p axis other xi eta d) = Nat.card (cageMiddleWitnessPowerRangeSolutions p NormalizedCoordinateAxis.first NormalizedCoordinateAxis.second xi eta d)

                  The witness-bearing cage count is independent of the chosen ordered pair of outer coordinate axes.