Documentation

LeanPool.BooleanMultiplication.N4.QuarticOrbits

The three rational quartic-plane orbits #

This file finishes the coordinate part of the low--low quartic exclusion. The only finite certificate is the left inverse in CubicDirect; the orbit arguments below are ordinary exterior algebra and coordinate extensionality.

source
def UnrestrictedBooleanMul.N4.infinityPlaceCoeff3 :
Fin 3 → F₂

Select evaluation at infinity among the three rational-place coordinates.

Equations
Instances For
    source
    def UnrestrictedBooleanMul.N4.oneInfinityCoeff3 :
    Fin 3 → F₂

    The sum of the evaluation-at-one and evaluation-at-infinity coordinates.

    Equations
    Instances For
      source
      def UnrestrictedBooleanMul.N4.zeroOneCoeff3 :
      Fin 3 → F₂

      The sum of the evaluation-at-zero and evaluation-at-one coordinates.

      Equations
      Instances For
        source
        def UnrestrictedBooleanMul.N4.zeroInfinityCoeff3 :
        Fin 3 → F₂

        The sum of the evaluation-at-zero and evaluation-at-infinity coordinates.

        Equations
        Instances For
          source
          @[simp]
          theorem UnrestrictedBooleanMul.N4.rationalTwo_infinityPlaceCoeff3 :
          rationalTwo infinityPlaceCoeff3 = rationalPlaceTwo 2
          source
          @[simp]
          theorem UnrestrictedBooleanMul.N4.rationalTwo_oneInfinityCoeff3 :
          rationalTwo oneInfinityCoeff3 = rationalPlaceTwo 1 + rationalPlaceTwo 2
          source
          @[simp]
          theorem UnrestrictedBooleanMul.N4.rationalTwo_zeroOneCoeff3 :
          rationalTwo zeroOneCoeff3 = rationalPlaceTwo 0 + rationalPlaceTwo 1
          source
          @[simp]
          theorem UnrestrictedBooleanMul.N4.rationalTwo_zeroInfinityCoeff3 :
          rationalTwo zeroInfinityCoeff3 = rationalPlaceTwo 0 + rationalPlaceTwo 2
          source
          theorem UnrestrictedBooleanMul.N4.quartic_cubic_kernel_zero_oneInfinity (x y : LinearForm) (h : vectorWedgeTwo x (rationalPlaceTwo 1 + rationalPlaceTwo 2) + vectorWedgeTwo y (rationalPlaceTwo 0) = 0) :
          x = 0 ∧ ∃ (c : F₂) (d : F₂), y = quarticPzeroVector c d

          Orbit span(r₀,r₁+r∞): the coefficient of the second generator vanishes, and the remaining coefficient lies in P₀.

          source
          theorem UnrestrictedBooleanMul.N4.quartic_cubic_kernel_zeroOne_zeroInfinity (x y : LinearForm) (h : vectorWedgeTwo x (rationalPlaceTwo 0 + rationalPlaceTwo 2) + vectorWedgeTwo y (rationalPlaceTwo 0 + rationalPlaceTwo 1) = 0) :
          x = 0 ∧ y = 0

          Orbit span(r₀+r₁,r₀+r∞): cubic cancellation kills both linear differences.

          source
          theorem UnrestrictedBooleanMul.N4.rationalProductCubic_equal_kernel (ell₀ m₀ ell₁ m₁ : LinearForm) (α β : Fin 3 → F₂) (h : rationalProductCubic ell₀ m₀ α β = rationalProductCubic ell₁ m₁ α β) :
          vectorWedgeTwo (ell₀ + ell₁) (rationalTwo β) + vectorWedgeTwo (m₀ + m₁) (rationalTwo α) = 0
          source
          theorem UnrestrictedBooleanMul.N4.aligned_lowLow_target_is_rational_of_kernel (α β : Fin 3 → F₂) (a₀ b₀ a₁ b₁ ax bx ay dy : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (t : TargetCoeff) (hx : ell₀ + ell₁ = quarticPoneVector ax bx) (hy : m₀ + m₁ = quarticPzeroVector ay dy) (hxw : vectorWedgeTwo (ell₀ + ell₁) (rationalTwo β) = 0) (hyw : vectorWedgeTwo (m₀ + m₁) (rationalTwo α) = 0) (hquadratic : targetTwo t = rationalProductQuadratic a₀ b₀ ell₀ m₀ α β + rationalProductQuadratic a₁ b₁ ell₁ m₁ α β) :
          IsRationalCoeff t

          Shared quadratic-shadow argument for the three low--low quartic orbits. Its hypotheses are exactly the output of the cubic direct-sum calculation: the two linear differences lie in P₁ and P₀, and their cubic contractions vanish.

          source
          theorem UnrestrictedBooleanMul.N4.aligned_zero_oneInfinity_lowLow_target_is_rational (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (t : TargetCoeff) (hcubic : rationalProductCubic ell₀ m₀ zeroPlaceCoeff3 oneInfinityCoeff3 = rationalProductCubic ell₁ m₁ zeroPlaceCoeff3 oneInfinityCoeff3) (hquadratic : targetTwo t = rationalProductQuadratic a₀ b₀ ell₀ m₀ zeroPlaceCoeff3 oneInfinityCoeff3 + rationalProductQuadratic a₁ b₁ ell₁ m₁ zeroPlaceCoeff3 oneInfinityCoeff3) :
          IsRationalCoeff t

          Low--low quartic collision for the orbit span(r₀,r₁+r∞).

          source
          theorem UnrestrictedBooleanMul.N4.aligned_zeroOne_zeroInfinity_lowLow_target_is_rational (a₀ b₀ a₁ b₁ : F₂) (ell₀ m₀ ell₁ m₁ : LinearForm) (t : TargetCoeff) (hcubic : rationalProductCubic ell₀ m₀ zeroOneCoeff3 zeroInfinityCoeff3 = rationalProductCubic ell₁ m₁ zeroOneCoeff3 zeroInfinityCoeff3) (hquadratic : targetTwo t = rationalProductQuadratic a₀ b₀ ell₀ m₀ zeroOneCoeff3 zeroInfinityCoeff3 + rationalProductQuadratic a₁ b₁ ell₁ m₁ zeroOneCoeff3 zeroInfinityCoeff3) :
          IsRationalCoeff t

          Low--low quartic collision for the orbit span(r₀+r₁,r₀+r∞).