MovingIntegralFrequencySplit.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact frequency and internal-prime splitting before real restrictions

All divisions here are integer divisions. Positivity is deliberately left to the existing real gate. The equivalence recovers integer divisibility from the two disjoint residue blocks, including at every descendant node.

def OAI.Ostmann.MovingSlotReversal.SignedIntegralAt line 15
def OAI.Ostmann.MovingSlotData.SignedIntegral line 20
def OAI.Ostmann.movingSignedFrequencyUnits line 28
theorem OAI.Ostmann.movingSignedFrequencyUnits_auxiliary line 36
theorem OAI.Ostmann.MovingSlotReversal.frequencyPivot_signed_modEq line 48
theorem OAI.Ostmann.pairwise_coprime_list_prod_int_dvd_iff line 62
theorem OAI.Ostmann.MovingSlotReversal.signedIntegral_of_prime_lines line 67

theorem OAI.Ostmann.moving_frequency_internal_split line 88

Source documentation

The frequency block and the simultaneous prime lines give precisely the original signed integer recursion with its subtree-frequency unit tests. This is an equivalence on every top pair, before the real support is imposed.

theorem moving_frequency_internal_split {σ : Type*}
    (tier : σ → ℕ) (value : σ → ℕ) (hprime : ∀ i, (value i).Prime)
    (hdisjoint : ∀ i j, tier i ≠ tier j → value i ≠ value j) (R : ℤ)
    (hsmall : ∀ i, IsCoprime (value i : ℤ) R)
    {n : ℕ} (T : MovingSlotData σ n) (hlevels : T.Levels tier)
    (hf : T.Frequencies (· ≠ 0))
    (hfmod : ∀ i, T.Frequencies (fun f => (f : ZMod (value i)) ≠ 0))
    (hR : T.frequencyProduct ∣ R) (hdistinct : T.CompensationDistinct value) (x y : ℤ) :
    movingFrequencyGate value R T x y ∧ movingPrimeLineSupport value T x y ↔
      T.SignedIntegral value x y ∧ movingSignedFrequencyUnits value T x y := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingFrequencyGate, OAI.Ostmann.movingPrimeLineSupport, OAI.Ostmann.movingSignedFrequencyUnits