Documentation

LeanPool.Zeta32.PrimeEdge.Blocks

the proof notes, §6: fixed local matrices and exact determinant identities. lowBlockMatrix = [V⁰(u^{i+k} r_L)], highBlockMatrix = [V⁰(u^{i+k} r_H)], M₀ = [V⁰(u^{i+k} r_0)] with V⁰(u^e) = e B_{e-1}, V⁰((u+m)^{-1}) = 2 H_m^{(3)} and r_L = u³/((u+1)(u+2)(u+3)(u+4)), r_H = u³/((u+1)(u+2)(u+3)), r_0 = u/((u+1)(u+2)(u+3)(u+4)) (exact rationals of code/local_blocks_453.py and the FIX table of code/prime_edge_crt453.py). The Hankel entries depend only on i+k; the moment sequences are recorded separately.

source
def Zeta32.PrimeEdge.lowMoment :
Fin 5 → ℚ

V⁰(u^e r_L), e = 0, …, 4.

Equations
Instances For
    source
    def Zeta32.PrimeEdge.highMoment :
    Fin 3 → ℚ

    V⁰(u^e r_H), e = 0, …, 2.

    Equations
    Instances For
      source
      def Zeta32.PrimeEdge.zeroMoment :
      Fin 7 → ℚ

      V⁰(u^e r_0), e = 0, …, 6.

      Equations
      Instances For
        source
        def Zeta32.PrimeEdge.lowBlockMatrix :
        Matrix (Fin 3) (Fin 3) ℚ

        The three-by-three Hankel block formed from the low moments.

        Equations
        Instances For
          source
          def Zeta32.PrimeEdge.highBlockMatrix :
          Matrix (Fin 2) (Fin 2) ℚ

          The two-by-two Hankel block formed from the high moments.

          Equations
          Instances For
            source
            def Zeta32.PrimeEdge.M₀ :
            Matrix (Fin 4) (Fin 4) ℚ

            The four-by-four Hankel block formed from the zero moments.

            Equations
            Instances For
              source
              theorem Zeta32.PrimeEdge.M_L_eq :
              lowBlockMatrix = !![1565 / 648, -15575 / 648, 101261 / 648; -15575 / 648, 101261 / 648, -545255 / 648; 101261 / 648, -545255 / 648, 2649929 / 648]
              source
              theorem Zeta32.PrimeEdge.M_H_eq :
              highBlockMatrix = !![-115 / 8, 481 / 8; 481 / 8, -1731 / 8]
              source
              theorem Zeta32.PrimeEdge.M₀_eq :
              M₀ = !![1 / 1296, 7 / 648, 1565 / 648, -15575 / 648; 7 / 648, 1565 / 648, -15575 / 648, 101261 / 648; 1565 / 648, -15575 / 648, 101261 / 648, -545255 / 648; -15575 / 648, 101261 / 648, -545255 / 648, 2649929 / 648]
              source
              theorem Zeta32.PrimeEdge.det_M_L :
              lowBlockMatrix.det = -31336873 / 1296
              source
              theorem Zeta32.PrimeEdge.det_M_H :
              highBlockMatrix.det = -4037 / 8
              source
              theorem Zeta32.PrimeEdge.det_M₀ :
              M₀.det = -12931 / 324