MovingOccurrenceSquares.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The full square support as the actual occurrence line tests

def OAI.Ostmann.MovingSlotReversal.integerNumerator line 11

theorem OAI.Ostmann.MovingSlotData.squareTests_iff_occurrences line 18

Source documentation

All recursive exclusions are exactly the exclusions in the recorded occurrence list, evaluated along their actual natural paths.

theorem MovingSlotData.squareTests_iff_occurrences {σ : Type*} (value : σ → ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (XL XR : ℕ) :
    T.PrimeSquareTests value XL XR ↔
      ∀ o ∈ T.occurrences, ∀ i ∈ o.current.compensationSlots,
        ¬ (value i : ℤ) ^ 2 ∣ o.current.integerNumerator value
          (movingSlotNaturalPath value o.path (XL, XR)) := by
…

Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingSlotNaturalPath

theorem OAI.Ostmann.MovingSlotData.occurrence_compensation_level line 67
Source documentation
A current compensation slot belongs to the type immediately below the occurrence, including when a prime represents multiple occurrences.
```
theorem MovingSlotData.occurrence_compensation_level {σ : Type*} (tier : σ → ℕ)
    {n : ℕ} (T : MovingSlotData σ n) (hT : T.Levels tier) :
    ∀ o ∈ T.occurrences, ∀ i ∈ o.current.compensationSlots, tier i < o.level := by
…
```
Mentions: OAI.Ostmann.MovingSlotData
theorem OAI.Ostmann.MovingSlotData.occurrences_length line 85

theorem OAI.Ostmann.MovingSlotData.squareTests_iff_lines line 97

Source documentation

The full recursive support has only linear equations at the original pair of giants modulo the current compensation-prime squares.

theorem MovingSlotData.squareTests_iff_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) :
    T.PrimeSquareTests value XL XR ↔
      ∀ o ∈ T.occurrences, ∀ i ∈ o.current.compensationSlots,
        let φ := MovingSlotReversal.naturalReduction (value i ^ 2) value
…

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

theorem OAI.Ostmann.MovingSlotData.fullPairwise_iff_lines line 122

Source documentation

Full original pairwise support reduces to top coprimality and precisely these square-line exclusions. The arithmetic and frequency guards are kept.

theorem MovingSlotData.fullPairwise_iff_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)
    (hcoh : T.RegularCoherent) (hc : T.CompensationPrimeData value)
    (hf : ∀ i, T.Frequencies (fun s => (s : ZMod (value i)) ≠ 0))
    (XL XR : ℕ) (hI : T.Integral value XL XR)
    (hcross : T.CrossFrequencyUnits value XL XR) :
    T.FullPairwise value XL XR ↔ T.CurrentPairwise value XL XR ∧
      ∀ o ∈ T.occurrences, ∀ i ∈ o.current.compensationSlots,
        let φ := MovingSlotReversal.naturalReduction (value i ^ 2) value
…

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