OAI/NumberTheory/Ostmann/Characters/QuartetBadCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.pair_inverse_ratio_held line 11

   Source documentation

   The inverse ratio uses the square of the first, now held, entry.

   theorem pair_inverse_ratio_held {p : ℕ} [Fact p.Prime]
       (D s s₁ s₂ C₁ C₂ V X m₁ m₂ : (ZMod p)ˣ) :
       ((s₁ / s₂) * ((X * C₂ * m₂) / (V * C₁ * m₁)))⁻¹ =
         ((D * s₂ / (s₁ * s)) * (V * C₁) ^ 2 * m₁ ^ 2) *
           rationalTreeArgument s (C₁ * C₂) D V X (m₁ * m₂) := by
   …

   Mentions: OAI.Ostmann.rationalTreeArgument

2. theorem OAI.Ostmann.rationalQuartet_shared_square line 24

   Source documentation

   The common reconstructed entry has the exact square needed to cancel one difference from each child pair. The child products need only agree.

   theorem rationalQuartet_shared_square {p : ℕ} [Fact p.Prime]
       (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (V XL XR M N : (ZMod p)ˣ) :
       V ^ 2 = (Q.sL * Q.sR / (Q.s * D * Q.u ^ 2)) *
         rationalTreeArgument Q.s (Q.CL * Q.CR) D XL XR (M * N) /
           (rationalTreeArgument Q.sL (Q.u * Q.CL) D V XL M *
             rationalTreeArgument Q.sR (Q.u * Q.CR) D V XR N) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.rationalTreeArgument

3. theorem OAI.Ostmann.bad_ratio_of_shared_square line 37

   Source documentation

   Algebraic cancellation producing lambda / e in the bad orientation.

   theorem bad_ratio_of_shared_square {p : ℕ} [Fact p.Prime]
       (K C y V d e m : (ZMod p)ˣ) (hV : V ^ 2 = C * y / (d * e)) :
       (K * (V * m) ^ 2) * d = (K * C * y) * m ^ 2 / e := by
   …

4. theorem OAI.Ostmann.bad_ratio_of_shared_square_right line 46

   Source documentation

   The corresponding cancellation on the right produces lambda / d.

   theorem bad_ratio_of_shared_square_right {p : ℕ} [Fact p.Prime]
       (K C y V d e m : (ZMod p)ˣ) (hV : V ^ 2 = C * y / (d * e)) :
       (K * (V * m) ^ 2) * e = (K * C * y) * m ^ 2 / d := by
   …

5. def OAI.Ostmann.quartetSharedConstant line 52
6. def OAI.Ostmann.quartetLeftBadHeld line 56
7. def OAI.Ostmann.quartetRightBadHeld line 61
8. theorem OAI.Ostmann.rationalQuartet_left_bad_ratio line 67

   Source documentation

   Holding the reconstructed entry on the left gives exactly the bad ratio.

   theorem rationalQuartet_left_bad_ratio {p : ℕ} [Fact p.Prime]
       (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (V XL XR m₁ m₂ m₃ m₄ : (ZMod p)ˣ) :
       ((Q.s₁ / Q.s₂) * ((XL * Q.C₂ * m₂) / (V * Q.C₁ * m₁)))⁻¹ =
         (quartetLeftBadHeld D Q XL XR ((m₁ * m₂) * (m₃ * m₄)) * m₁ ^ 2) /
           rationalTreeArgument Q.sR (Q.u * Q.CR) D V XR (m₃ * m₄) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.quartetLeftBadHeld, OAI.Ostmann.rationalTreeArgument

9. theorem OAI.Ostmann.rationalQuartet_right_bad_ratio line 84

   Source documentation

   The right held reconstructed entry gives the other bad ratio.

   theorem rationalQuartet_right_bad_ratio {p : ℕ} [Fact p.Prime]
       (D : (ZMod p)ˣ) (Q : RationalQuartetData (ZMod p)ˣ)
       (V XL XR m₁ m₂ m₃ m₄ : (ZMod p)ˣ) :
       ((Q.s₃ / Q.s₄) * ((XR * Q.C₄ * m₄) / (V * Q.C₃ * m₃)))⁻¹ =
         (quartetRightBadHeld D Q XL XR ((m₁ * m₂) * (m₃ * m₄)) * m₃ ^ 2) /
           rationalTreeArgument Q.sL (Q.u * Q.CL) D V XL (m₁ * m₂) := by
   …

   Mentions: OAI.Ostmann.RationalQuartetData, OAI.Ostmann.quartetRightBadHeld, OAI.Ostmann.rationalTreeArgument