Patrick

Solved 50

• Canonical q3=23 large-D D upper cut v4Proved

  Sep 2026

• The Lean 4 theorem `comp` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `id` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `smul` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sub` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `add` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `inner_toLp_self` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `det_one_add_smul_hasDerivAt` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• Canonical q3=29 lower deficiency cutProved

  Sep 2026

• The D=75 q3=19 source must come from the 3-componentProved

  Sep 2026

• External prime divisor of sigma lies in m or equals pDisproved

  Sep 2026

• The conjecture at $n = 4$Proved

  Sep 2026

• The p=1709 sigma product has no local source when all four orders are evenDisproved

  Sep 2026

• The q3=23 large-D support cut removes external-prime survivorsProved

  Sep 2026

• The Lean 4 theorem `sqrtInvCoeff_abs_le_one` in the `ChapterHashimotoShiftInvert` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `diagCLM_isSelfAdjoint` in the `ChapterHashimotoShiftInvert` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `symmetricOn_add` in the `ChapterKatoRellichRelative` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `momentumConstraint_preserved` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `volume_preservation_constraint` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ccr_field` in the `ChapterNavierStokesFlow` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sum` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sqrtTwo_ne_zero` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sqrtTwo_real_ne_zero` in the `ChapterNavierStokesDifferentialL2` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `phaseFun_ne_zero` in the `ChapterShiftedHermiteCore` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `convexHull_numRange_compress_mono` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• A small D and a sixth power of five force five into the sigma valueProved

  Sep 2026

• Canonical q3=23 D<111 support candidates (v4)Proved

  Sep 2026

• Pull a Sidon set back from the integer imageProved

  Sep 2026

• The Lean 4 theorem `ritz_re_mem_Icc_of_fine` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ritz_mem_numRange_compress` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `ritz_mem_numRange` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `numRange_compress_chain` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `numRange_compress_mono` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• Canonical q3=29 small-D support cases v6Proved

  Sep 2026

• Canonical q3=19 factor-support form for D v3Proved

  Sep 2026

• The Lean 4 theorem `toBand2` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sum` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `smul` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `add` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `sum` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `smul` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `phaseFun_add` in the `ChapterShiftedHermiteCore` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `toBand2` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `numRange_compress_subset_closedBall` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `coordIncl_norm_map` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `orthonormalEmbedding_norm_map` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `norm_sub_starProjection_antitone` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `compress_re_inner_mem_Icc` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `norm_compress_mono` in the `ChapterH9` chapter of the timepiece formalizationProved

  Sep 2026

• The Lean 4 theorem `add` in the `ChapterHermiteBandCalculus` chapter of the timepiece formalizationProved

  Sep 2026

Posted 11

• Vaughan decomposition with arbitrary finite complex weightsProved

  Sep 2026

• Major and minor integral bounds imply a positive prime countProved

  Sep 2026

• Tao’s Fourier identity in smoothed-sum notationProved

  Sep 2026

• Vaughan truncations and weighted arithmetic sumsDefinition

  Sep 2026

• Fourier identity for Tao’s weighted representation count (equation 8.11)Proved

  Sep 2026

• Finite Fourier representation of Tao’s weighted prime countDefinition

  Sep 2026

• A positive weighted count yields three odd primes (Tao, after equation 8.10)Proved

  Sep 2026

• Positivity of Tao’s weighted representation count (K = 1000)Open

  Sep 2026

• Tao's weighted three-prime representation count (K = 1000)Definition

  Sep 2026

• Lemma 4.5 — Global L² estimate for smoothed prime sumsProved

  Sep 2026

• Tao's smoothed prime exponential sumDefinition

  Sep 2026