OAI/Computability/QuantumFactoring/OrderTrialFurther2.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.OrderTrial.largeQ line 12
2. lemma OAI.ExactQuantumFactoring.OrderTrial.majorantSum_bounds line 22

   Source documentation

   The literal majorant-sum estimate at the standing Q=B^16.

   lemma majorantSum_bounds {B d : ℕ} (hB : 2 ≤ B) (hd : 0 < d) (hdB : d < B) (j : ℕ) :
       1/(128*(d:ℝ)) ≤ (majorantSum (B^16) B d j:ℝ) ∧
         (majorantSum (B^16) B d j:ℝ) ≤ 2 := by
   …

   Mentions: OAI.ExactQuantumFactoring.OrderTrial.majorantSum

3. def OAI.ExactQuantumFactoring.OrderTrial.roundedNumerator line 40

   Source documentation

   Integer numerator retained by upward rounding at an integer argument.

   noncomputable def roundedNumerator (D : ℕ) (p : ℚ[X]) (u : ℕ) : ℤ :=
   …

4. lemma OAI.ExactQuantumFactoring.OrderTrial.roundedValue_numerator line 43
5. def OAI.ExactQuantumFactoring.OrderTrial.majorantNumerator line 51
6. lemma OAI.ExactQuantumFactoring.OrderTrial.majorant_numerator line 54
7. lemma OAI.ExactQuantumFactoring.OrderTrial.majorantSum_numerator line 62
8. def OAI.ExactQuantumFactoring.OrderTrial.IsDyadic line 69

   Source documentation

   Dyadic means an integer over a nonnegative integral power of two.

   def IsDyadic (x : ℚ) : Prop := ∃ k : ℕ, ∃ z : ℤ, x = (z:ℚ)/2^k

9. lemma OAI.ExactQuantumFactoring.OrderTrial.majorant_dyadic line 71
10. lemma OAI.ExactQuantumFactoring.OrderTrial.majorantSum_dyadic line 79
11. def OAI.ExactQuantumFactoring.OrderTrial.powerSumValue line 95

    Source documentation

    Five closed power-sum formulas, not an enumeration up to the endpoint.

    def powerSumValue (q : ℕ) (M : ℚ) : ℚ :=
    …

12. lemma OAI.ExactQuantumFactoring.OrderTrial.powerSumValue_correct line 104
13. lemma OAI.ExactQuantumFactoring.OrderTrial.powerSumValue_sub line 113
14. def OAI.ExactQuantumFactoring.OrderTrial.fiveTermSum line 118

    Source documentation

    Constant-length arithmetic formula for summing a degree-four expression.

    def fiveTermSum (a : ℕ → ℚ) (lo hi : ℕ) : ℚ :=
    …

15. lemma OAI.ExactQuantumFactoring.OrderTrial.fiveTermSum_correct line 121
16. def OAI.ExactQuantumFactoring.OrderTrial.intervalLo line 132

    Source documentation

    Clipped natural endpoints for the intersection of two rational intervals.

    def intervalLo (a c : ℚ) : ℕ := max ⌈a⌉.toNat ⌈c⌉.toNat

17. def OAI.ExactQuantumFactoring.OrderTrial.intervalHi line 134
18. lemma OAI.ExactQuantumFactoring.OrderTrial.interval_mem_iff line 136
19. lemma OAI.ExactQuantumFactoring.OrderTrial.quarterIndex_eq line 150
20. lemma OAI.ExactQuantumFactoring.OrderTrial.shiftedQuarter_eq line 156
21. def OAI.ExactQuantumFactoring.OrderTrial.quarterPairs line 165

    Source documentation

    Exactly 32 possible quarter pairs.

    noncomputable def quarterPairs : Finset (ℤ × ℤ) := (Finset.Ico 0 4) ×ˢ (Finset.Ico (-2) 6)

22. def OAI.ExactQuantumFactoring.OrderTrial.pieceLabel line 167
23. lemma OAI.ExactQuantumFactoring.OrderTrial.pieceLabel_mem line 170
24. lemma OAI.ExactQuantumFactoring.OrderTrial.quarterPairs_card line 180
25. def OAI.ExactQuantumFactoring.OrderTrial.pieceLo line 182
26. def OAI.ExactQuantumFactoring.OrderTrial.pieceHi line 185
27. lemma OAI.ExactQuantumFactoring.OrderTrial.piece_fiber line 188
28. def OAI.ExactQuantumFactoring.OrderTrial.packedPieceSum line 203

    Source documentation

    Each piece sum is computed with five closed power sums plus its length.

    noncomputable def packedPieceSum (Q B d j : ℕ) (q : ℤ × ℤ) : ℚ :=
    …

29. lemma OAI.ExactQuantumFactoring.OrderTrial.packedPieceSum_correct line 210
30. def OAI.ExactQuantumFactoring.OrderTrial.packedMajorantSum line 230

    Source documentation

    Exact constant-piece evaluation: no traversal of the d residues.

    noncomputable def packedMajorantSum (Q B d j : ℕ) : ℚ :=
    …

31. lemma OAI.ExactQuantumFactoring.OrderTrial.packedMajorantSum_correct line 233
32. def OAI.ExactQuantumFactoring.OrderTrial.prescribedMass line 254

    Source documentation

    Exact prescribed per-numerator mass, with the manuscript's ceiling.

    def prescribedMass (d : ℕ) : ℚ := 1/(2:ℚ)^(Nat.clog 2 d+10)

33. lemma OAI.ExactQuantumFactoring.OrderTrial.prescribedMass_pos line 256
34. lemma OAI.ExactQuantumFactoring.OrderTrial.prescribedMass_upper line 260
35. lemma OAI.ExactQuantumFactoring.OrderTrial.prescribedMass_lower line 270
36. def OAI.ExactQuantumFactoring.OrderTrial.modeCoeff line 290

    Source documentation

    Downward dyadic ratio rounding, as in (mode-coefficient).

    def modeCoeff (n : ℕ) (lam S : ℚ) : ℚ :=
    …

37. def OAI.ExactQuantumFactoring.OrderTrial.modeRemainder line 293
38. lemma OAI.ExactQuantumFactoring.OrderTrial.modeCoeff_basic line 295
39. lemma OAI.ExactQuantumFactoring.OrderTrial.modeRemainder_basic line 312
40. lemma OAI.ExactQuantumFactoring.OrderTrial.modeCoeff_bounds line 324
41. lemma OAI.ExactQuantumFactoring.OrderTrial.sum_residue_permutation line 341
42. lemma OAI.ExactQuantumFactoring.OrderTrial.IsDyadic.intCast line 365
43. lemma OAI.ExactQuantumFactoring.OrderTrial.IsDyadic.add line 367
44. lemma OAI.ExactQuantumFactoring.OrderTrial.IsDyadic.neg line 375
45. lemma OAI.ExactQuantumFactoring.OrderTrial.IsDyadic.sub line 379
46. lemma OAI.ExactQuantumFactoring.OrderTrial.IsDyadic.mul line 382
47. lemma OAI.ExactQuantumFactoring.OrderTrial.prescribedMass_dyadic line 390
48. lemma OAI.ExactQuantumFactoring.OrderTrial.modeCoeff_dyadic line 393
49. lemma OAI.ExactQuantumFactoring.OrderTrial.modeRemainder_dyadic line 396
50. def OAI.ExactQuantumFactoring.OrderTrial.firstModeMass line 401

    Source documentation

    The three actual branches, including mode selection and uniform-label masses.

    noncomputable def firstModeMass (n Q B d j : ℕ) : ℝ :=
    …

51. def OAI.ExactQuantumFactoring.OrderTrial.secondModeMass line 405
52. def OAI.ExactQuantumFactoring.OrderTrial.thirdModeMass line 411
53. lemma OAI.ExactQuantumFactoring.OrderTrial.first_second_mass line 416

    Source documentation

    Exact cancellation, not an estimate: Mode 2 fills precisely U-P.

    lemma first_second_mass {n Q B d j : ℕ} (hB : 0 < B) (hd : 0 < d)
        (hj : Nat.Coprime j d) :
        firstModeMass n Q B d j + secondModeMass n Q B d j =
          (modeCoeff n (prescribedMass d) (majorantSum Q B d j):ℝ) *
          (majorantSum Q B d j:ℝ) := by
    …

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.firstModeMass, OAI.ExactQuantumFactoring.OrderTrial.secondModeMass, OAI.ExactQuantumFactoring.OrderTrial.modeCoeff, OAI.ExactQuantumFactoring.OrderTrial.prescribedMass, OAI.ExactQuantumFactoring.OrderTrial.majorantSum

54. lemma OAI.ExactQuantumFactoring.OrderTrial.third_mode_mass line 439
55. lemma OAI.ExactQuantumFactoring.OrderTrial.three_mode_mass line 447

    Source documentation

    The exact mass per reduced label, including the d=1, j=0 boundary case.

    lemma three_mode_mass {n Q B d j : ℕ} (hB : 0 < B) (hd : 0 < d)
        (hj : Nat.Coprime j d) :
        firstModeMass n Q B d j + secondModeMass n Q B d j + thirdModeMass n Q B d j =
          (prescribedMass d:ℝ) := by
    …

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.firstModeMass, OAI.ExactQuantumFactoring.OrderTrial.secondModeMass, OAI.ExactQuantumFactoring.OrderTrial.thirdModeMass, OAI.ExactQuantumFactoring.OrderTrial.prescribedMass

56. lemma OAI.ExactQuantumFactoring.OrderTrial.largeQ_cube line 455
57. lemma OAI.ExactQuantumFactoring.OrderTrial.discrepancy_retention_bounds line 462

    Source documentation

    The artificial discrepancy is a valid probability even at false labels.

    lemma discrepancy_retention_bounds {B d t : ℕ} (hB : 2 ≤ B) (hd : 0 < d)
        (hdB : d < B) (ht : t < d) (j : ℕ) {c : ℝ} (hc₀ : 0 ≤ c) (hc₁ : c ≤ 1) :
        0 ≤ 2*(B:ℝ)^3*((majorant (B^16) B d j ((j*t)%d):ℝ)-
          residueProbability (B^16) d j t)*c ∧
        2*(B:ℝ)^3*((majorant (B^16) B d j ((j*t)%d):ℝ)-
          residueProbability (B^16) d j t)*c ≤ 1 := by
    …

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.majorant, OAI.ExactQuantumFactoring.OrderTrial.residueProbability

58. lemma OAI.ExactQuantumFactoring.OrderTrial.remainder_retention_bounds line 489