MovingCompensationLines.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Compensation divisibility is the current internal-prime line condition

The equivalence below is used before imposing integrality of the new giant. Thus the line condition recovers the original compensation division instead of merely being a consequence of an already integral history.

theorem OAI.Ostmann.pairwise_coprime_list_prod_dvd_iff line 16
theorem OAI.Ostmann.compensation_dvd_iff_numerator line 31

theorem OAI.Ostmann.movingSlotLine_prime_zero_iff line 50

Source documentation

The cleared line and the actual current numerator have the same zero test modulo an internal prime. Only the earlier path must be integral.

theorem movingSlotLine_prime_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 value
…

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

theorem OAI.Ostmann.moving_compensation_division_iff_lines line 79

Source documentation

At a supported transfer node, the internal-prime congruences are equivalent to the original compensation-product divisibility.

theorem moving_compensation_division_iff_lines {σ : Type*}
    (value : σ → ℕ) (path : List (MovingSlotReversal σ))
    (current : MovingSlotReversal σ) (XL XR Q : ℕ)
    (hvalid : MovingSlotPathIntegral value path (XL, XR))
    (hprime : ∀ i ∈ current.compensationSlots, (value i).Prime)
    (hpair : (current.compensationSlots.map value).Pairwise Nat.Coprime)
    (hs : ∀ i ∈ current.compensationSlots, ¬ value i ∣ current.rootFrequency.natAbs)
    (hu : ∀ i ∈ current.compensationSlots, ∀ s ∈ path,
      MovingSlotReversal.naturalReduction (value i) value s.polynomial.u ≠ 0)
    (hN : current.integerNumerator value (movingSlotNaturalPath value path (XL, XR)) =
      current.rootFrequency * Q) :
    MovingSlotReversal.naturalProduct value current.compensationSlots ∣ Q ↔
…

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

theorem OAI.Ostmann.MovingSlotData.integral_compensation_lines line 111

Source documentation

Every internal-prime line of the original integral tree vanishes. This uses the actual occurrence path and allows a prime to represent several nodes.

theorem MovingSlotData.integral_compensation_lines {σ : Type*}
    (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
    (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j)
    {n : ℕ} (T : MovingSlotData σ n) (hlevels : T.Levels tier)
    (hfreq : ∀ i, T.Frequencies (fun s => (s : ZMod (value i)) ≠ 0))
    (XL XR : ℕ) (hI : T.Integral value XL XR) :
    ∀ o ∈ T.occurrences, ∀ i ∈ o.current.compensationSlots,
      let φ := MovingSlotReversal.naturalReduction (value i) value
…

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