LevelCounts.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExactQuantumFactoring.dvd_div_pow_two_iff line 16
Source documentation
Dividing a positive multiple by a power of two preserves exactly the order divisors with enough 2-adic slack.
```
theorem dvd_div_pow_two_iff {d r k : ℕ} (hr : r ≠ 0) (hdr : d ∣ r) (hk : 2 ^ k ∣ r) :
    d ∣ r / 2 ^ k ↔ padicValNat 2 d + k ≤ padicValNat 2 r := by
…
```
theorem OAI.ExactQuantumFactoring.level_le_iff_dvd_cutoff line 39
Source documentation
For a divisor, an exact valuation cutoff is a single ordinary divisibility test; hence its size is a cyclic-group root count, not residue enumeration.
```
theorem level_le_iff_dvd_cutoff {d r t : ℕ} (hr : r ≠ 0) (hdr : d ∣ r) :
    padicValNat 2 d ≤ t ↔ d ∣ r / 2 ^ (padicValNat 2 r - t) := by
…
```
def OAI.ExactQuantumFactoring.cumulativeLevelCount line 47
def OAI.ExactQuantumFactoring.levelCount line 51
theorem OAI.ExactQuantumFactoring.cumulativeLevelCount_eq line 56
Source documentation
The cumulative law of levels in every finite cyclic group.
```
theorem cumulativeLevelCount_eq (G : Type*) [CommGroup G] [Fintype G] [IsCyclic G] (t : ℕ) :
    cumulativeLevelCount G t = Fintype.card G / 2 ^ (padicValNat 2 (Fintype.card G) - t) := by
…
```
Mentions: OAI.ExactQuantumFactoring.cumulativeLevelCount
theorem OAI.ExactQuantumFactoring.levelCount_eq_cumulative line 76
Source documentation
Fibers are obtained by differencing two consecutive cumulative counts.
```
theorem levelCount_eq_cumulative (G : Type*) [Group G] [Fintype G] (t : ℕ) :
    levelCount G t = if t = 0 then cumulativeLevelCount G 0
      else cumulativeLevelCount G t - cumulativeLevelCount G (t - 1) := by
…
```
Mentions: OAI.ExactQuantumFactoring.levelCount, OAI.ExactQuantumFactoring.cumulativeLevelCount

theorem OAI.ExactQuantumFactoring.levelCount_cyclic line 100

Source documentation

Exact level counts use only cardinal arithmetic, powers of two and division.

theorem levelCount_cyclic (G : Type*) [CommGroup G] [Fintype G] [IsCyclic G] (t : ℕ) :
    levelCount G t = if t = 0 then
      Fintype.card G / 2 ^ padicValNat 2 (Fintype.card G)
    else Fintype.card G / 2 ^ (padicValNat 2 (Fintype.card G) - t) -
      Fintype.card G / 2 ^ (padicValNat 2 (Fintype.card G) - (t - 1)) := by
…

Mentions: OAI.ExactQuantumFactoring.levelCount