MovingPatternLogLeafBridge.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual initial leaf weights in the pattern prime observable

theorem OAI.Ostmann.movingPatternTwoPrimeObservable_log_leaf line 32
Source documentation
Exact identification with the retained-log observable. The outside spectator profile is a scalar; every variable terminal factor remains inside.
```
theorem movingPatternTwoPrimeObservable_log_leaf (x : Fin (N + 1) → primes) :
    let value := fun i => (x i : ℕ)
…
```
Mentions: OAI.Ostmann.primes

theorem OAI.Ostmann.movingPattern_log_slot_lengths line 70

Source documentation

The concrete pattern automatically meets the retained-log comparison's terminal length bound.

theorem movingPattern_log_slot_lengths {B C : Type*} {N n m r₀ : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (t : Bool → FrequencyTree ℤ n)
    (small : Bool → TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
    (perm : Equiv.Perm (TreeLeafIndex n × Fin m)) (pattern : Bool × MovingSampleIndex n → C)
    (tier : Fin (N + 1) → ℕ) (k : ℕ) (hsmall : ∀ b, MovingLeafLengthLE n (small b) r₀) :
    ∀ j, (movingPairedLogSlots tier k
      (movingPatternFinBulkData e n m t small slot perm pattern) j).length ≤
        2 ^ n * (r₀ + m + 4 * n) :=
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.MovingLeafLengthLE, OAI.Ostmann.movingPairedLogSlots, OAI.Ostmann.movingPatternFinBulkData