OAI/NumberTheory/Ostmann/Arithmetic/MovingSquareLines.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.naturalReduction_square line 11
2. theorem OAI.Ostmann.movingSlotLine_square_denominator_unit line 20
3. theorem OAI.Ostmann.movingSlotLine_square_zero_iff line 34

   Source documentation

   The exact numerator test modulo p² is the cleared line test at the two original giants. Only ancestor denominators need to be units.

   theorem movingSlotLine_square_zero_iff {σ : Type*} {p : ℕ} [Fact p.Prime]
       (value : σ → ℕ) (path : List (MovingSlotReversal σ))
       (current : MovingSlotReversal σ) (XL XR : ℕ)
       (hvalid : MovingSlotPathIntegral value path (XL, XR))
       (hu : ∀ s ∈ path, MovingSlotReversal.naturalReduction p value s.polynomial.u ≠ 0) :
       let φ := MovingSlotReversal.naturalReduction (p ^ 2) value
   …

   Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.MovingSlotPathIntegral, OAI.Ostmann.MovingSlotReversal.naturalReduction

4. theorem OAI.Ostmann.movingSlotLines_square_loss line 69

   Source documentation

   The uniform lift loss for any finite collection of actual occurrences. All rows are proved nonzero from the ancestor and current frequency units.

   theorem movingSlotLines_square_loss {σ I : Type*} [Fintype I] {p : ℕ} [Fact p.Prime]
       (value : σ → ℕ) (path : I → List (MovingSlotReversal σ))
       (current : I → MovingSlotReversal σ)
       (hunit : ∀ i s, s ∈ path i →
         MovingSlotReversal.naturalReduction p value s.polynomial.v ≠ 0 ∧
         MovingSlotReversal.naturalReduction p value s.polynomial.w ≠ 0 ∧
         MovingSlotReversal.naturalReduction p value s.polynomial.u ≠ 0)
       (hc : ∀ i, MovingSlotReversal.naturalReduction p value (current i).polynomial.v ≠ 0 ∧
         MovingSlotReversal.naturalReduction p value (current i).polynomial.w ≠ 0)
       (x₀ y₀ : ZMod p) (hy : y₀ ≠ 0)
       (hbase : ∀ i, MovingSlotReversal.naturalReduction p value (movingSlotLine (path i) (current i)).a * x₀ +
         MovingSlotReversal.naturalReduction p value (movingSlotLine (path i) (current i)).b * y₀ = 0)
   …

   Mentions: OAI.Ostmann.MovingSlotReversal, OAI.Ostmann.MovingSlotReversal.naturalReduction, OAI.Ostmann.movingSlotLine