OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeLineGate.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPrimeLineSupport line 10
2. theorem OAI.Ostmann.movingPrimeLineSupport_leaf line 17
3. theorem OAI.Ostmann.movingPrimeLineSupport_root line 22
4. theorem OAI.Ostmann.movingPrimeLineSupport_node line 44

   Source documentation

   Decomposition of the top-coordinate line gate after just the current integer relation is known; descendant integrality is not an assumption.

   theorem movingPrimeLineSupport_node {σ : Type*} (value : σ → ℕ)
       (hprime : ∀ i, (value i).Prime) {n : ℕ}
       (s : ℤ) (CL CR U : List σ) (left right : MovingSlotData σ n) (x y p : ℤ)
       (hrel : (MovingSlotData.step s CL CR U left right false).signedNumerator value x y =
         s * (MovingSlotReversal.naturalProduct value U : ℤ) * p)
       (hUL : ∀ o ∈ left.occurrences, ∀ i ∈ o.current.compensationSlots,
         MovingSlotReversal.naturalReduction (value i) value
           (MovingSlotData.step s CL CR U left right true).polynomial.u ≠ 0)
       (hUR : ∀ o ∈ right.occurrences, ∀ i ∈ o.current.compensationSlots,
         MovingSlotReversal.naturalReduction (value i) value
           (MovingSlotData.step s CL CR U left right false).polynomial.u ≠ 0) :
       movingPrimeLineSupport value (.node s CL CR U left right) x y ↔
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.MovingSlotData.step, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.MovingSlotReversal.naturalReduction, OAI.Ostmann.movingPrimeLineSupport

5. theorem OAI.Ostmann.MovingSlotData.compensation_ancestor_unit line 109
6. theorem OAI.Ostmann.movingPrimeLineSupport_node_of_levels line 122