Complete.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Ostmann's inverse Goldbach theorems

The quadratic large sieve and the exact character-zero density estimate give both the two-infinite-summands contradiction and asymptotic indecomposability.

theorem OAI.Ostmann.twoInfiniteSummandsImpossible line 16
Source documentation
Theorem 2.3: two infinite nonnegative summands cannot give the primes outside a finite initial interval.
Distinct definitions of this name: ComparatorChallenges/OstmannComplete.lean:33 (same statement text; different proof or body). Qualify references as OAI.Ostmann.twoInfiniteSummandsImpossible@path.
```
theorem twoInfiniteSummandsImpossible : TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach line 21
Source documentation
Theorem 1.1: every sum of two nontrivial sets of nonnegative integers has infinite symmetric difference with the primes.
Distinct definitions of this name: ComparatorChallenges/OstmannComplete.lean:30 (same statement text; different proof or body). Qualify references as OAI.Ostmann.inverseGoldbach@path.
```
theorem inverseGoldbach : InverseGoldbach :=
…
```