Basic.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Sets in Ostmann's inverse Goldbach problem

We use ℕ for the manuscript's nonnegative integers. The threshold convention uses N ≤ n; changing finitely many initial values does not affect it.

def OAI.Ostmann.EventuallyPrimeSumset line 17
Source documentation
Both prime coverage and exclusion of composite sums beyond one threshold.
Also declared: ComparatorChallenges/OstmannComplete.lean:13 (same declaration text).
```
def EventuallyPrimeSumset (A B : Set ℕ) : Prop :=
…
```
theorem OAI.Ostmann.sumset_comm line 20
theorem OAI.Ostmann.EventuallyPrimeSumset.symm line 27
theorem OAI.Ostmann.finite_symmDiff_iff line 34
Source documentation
The manuscript's finite symmetric difference and threshold formulations agree.
```
theorem finite_symmDiff_iff (A B : Set ℕ) :
    (sumset A B ∆ primes).Finite ↔ EventuallyPrimeSumset A B := by
…
```
Mentions: OAI.Ostmann.sumset, OAI.Ostmann.primes, OAI.Ostmann.EventuallyPrimeSumset
theorem OAI.Ostmann.EventuallyPrimeSumset.prime_add line 56
Source documentation
Each sufficiently large sum of elements of the summands is prime.
```
theorem EventuallyPrimeSumset.prime_add {A B : Set ℕ}
    (h : EventuallyPrimeSumset A B) :
    ∃ N, ∀ a ∈ A, ∀ b ∈ B, N ≤ a + b → (a + b).Prime := by
…
```
Mentions: OAI.Ostmann.EventuallyPrimeSumset
def OAI.Ostmann.TwoInfiniteSummandsImpossible line 63
Source documentation
The two infinite summands formulation, stated independently of its proof.
Also declared: ComparatorChallenges/OstmannComplete.lean:16 (same declaration text).
```
def TwoInfiniteSummandsImpossible : Prop :=
…
```
def OAI.Ostmann.InverseGoldbach line 67
Source documentation
Ostmann's main statement, including all finite modifications of the primes.
Distinct definitions of this name: ComparatorChallenges/OstmannComplete.lean:19 (same statement text; different proof or body). Qualify references as OAI.Ostmann.InverseGoldbach@path.
```
def InverseGoldbach : Prop :=
…
```