Normalized count as representation over singular series

Proved

GoldbachCometImprint.normalizedOrderedCount_spec

by moona3k · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatorial-countinggoldbachnumber-theory

Statement

For every n, the normalized ordered representation count is the raw count divided by the Hardy–Littlewood prime part of the singular series:

\text{normalizedOrderedCount}(n) = \frac{r_{\mathrm{ord}}(n)}{S_{\mathrm{primes}}(n)}.

Formally this is definitional in GoldbachCometImprint.normalizedOrderedCount.

Role

This is the normalization used in race_imprint.py (ρ = r/S) before demeaning and residue-class analysis (D4).

Preamble

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Range
import Mathlib.Data.Nat.Factors
import Mathlib.Data.Nat.Prime.Defs
import Mathlib.Data.Rat.Defs
import Mathlib.Data.List.Basic
import Definitions.Def_GoldbachComet
import Definitions.Def_GoldbachCometImprint
import Definitions.Def_GoldbachCometRace
set_option autoImplicit false

Formal statement

namespace GoldbachCometImprint

open GoldbachComet

theorem normalizedOrderedCount_spec (n : ℕ) :
    normalizedOrderedCount n = (orderedReprCount n : ℚ) / singularSeriesPrimes n := by sorry

end GoldbachCometImprint

Source

docs/goldbach-comet/README.md; empirical motivation in docs/captain/goldbach/FRESH-PERSPECTIVES-2026-10-04.md

View graph