Ordered Goldbach count as left-prime cardinality

Proved

GoldbachComet.orderedReprCount_eq_card

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

combinatorial-countinggoldbachnumber-theory

Statement

For every natural number n, the number of ordered Goldbach representations equals the cardinality of the left-prime finset:

r_{\mathrm{ord}}(n) = \bigl|\{ p \in \{0,\ldots,n\} : 2 \le p,\ 2 \le n-p,\ p\ \text{prime},\ n-p\ \text{prime}\}\bigr|.

Formally: GoldbachComet.orderedReprCount n = (GoldbachComet.primeLeftSummand n).card.

Proof idea

By definition, orderedReprCount n is the cardinality of orderedReprPairs n, which is (primeLeftSummand n).map (pairEmbedding n). The map pairEmbedding n is injective on its domain, so Finset.card_map gives equality with (primeLeftSummand n).card.

Role in the imprint program

This is the direct cardinality form of the pairing lemma (M1a). Together they identify r_{\mathrm{ord}}(n) with a sum over left primes, which is the discrete backbone for Hardy–Littlewood–type expansions and prime-race corrections.

References

Same counting conventions as Definitions/Def_GoldbachComet.lean.
Empirical motivation: docs/captain/goldbach/FRESH-PERSPECTIVES-2026-10-04.md (D4).

Preamble

import Mathlib.Data.Nat.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Image
import Mathlib.Data.Finset.Range
import Mathlib.Data.Nat.Prime.Defs
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Definitions.Def_GoldbachComet
open scoped BigOperators
set_option autoImplicit false

Formal statement

namespace GoldbachComet

theorem orderedReprCount_eq_card (n : ℕ) :
    orderedReprCount n = (primeLeftSummand n).card := by sorry

end GoldbachComet

Source

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

View graph