FactorSplitting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExactQuantumFactoring.dvd_half_of_level_lt line 12
Source documentation
Strictly smaller 2-adic level makes a divisor divide the half-order.
```
theorem dvd_half_of_level_lt {d r : ℕ} (hr : r ≠ 0) (hdr : d ∣ r)
    (hlevel : padicValNat 2 d < padicValNat 2 r) : d ∣ r / 2 := by
…
```
theorem OAI.ExactQuantumFactoring.level_le_of_dvd line 24
Source documentation
Divisibility cannot increase the 2-adic valuation.
```
theorem level_le_of_dvd {d r : ℕ} (hr : r ≠ 0) (hdr : d ∣ r) :
    padicValNat 2 d ≤ padicValNat 2 r := by
…
```
def OAI.ExactQuantumFactoring.halfOrderResidue line 31
Source documentation
The actual representative used by bounded modular gcd arithmetic.
```
noncomputable def halfOrderResidue {m : ℕ} (a : (ZMod m)ˣ) : ℕ :=
…
```
def OAI.ExactQuantumFactoring.splitGcd line 34

theorem OAI.ExactQuantumFactoring.splitGcd_proper_of_lower_component line 39

Source documentation

A single lower-level component suffices for a proper nontrivial split. The largest-level component is not assumed to have a chosen generator.

theorem splitGcd_proper_of_lower_component {m d : ℕ} (hm : 2 ≤ m) (hd : 2 ≤ d)
    (hdm : d ∣ m) (a : (ZMod m)ˣ)
    (hlevel : padicValNat 2 (orderOf (Units.map (ZMod.castHom hdm (ZMod d)).toMonoidHom a))
      < padicValNat 2 (orderOf a)) :
    1 < splitGcd a ∧ splitGcd a < m ∧ splitGcd a ∣ m := by
…

Mentions: OAI.ExactQuantumFactoring.splitGcd

theorem OAI.ExactQuantumFactoring.splitGcd_proper_of_unequal_components line 90

Source documentation

Two unequal local levels guarantee that one of them is below the global level, so the verified order always supplies a nontrivial gcd.

theorem splitGcd_proper_of_unequal_components {m d e : ℕ} (hm : 2 ≤ m)
    (hd : 2 ≤ d) (he : 2 ≤ e) (hdm : d ∣ m) (hem : e ∣ m) (a : (ZMod m)ˣ)
    (hne : padicValNat 2 (orderOf (Units.map (ZMod.castHom hdm (ZMod d)).toMonoidHom a)) ≠
      padicValNat 2 (orderOf (Units.map (ZMod.castHom hem (ZMod e)).toMonoidHom a))) :
    1 < splitGcd a ∧ splitGcd a < m ∧ splitGcd a ∣ m := by
…

Mentions: OAI.ExactQuantumFactoring.splitGcd