Reduction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Reduction of Ostmann's conjecture to two infinite summands

The equivalence here is a reduction, not a proof of either main statement. In particular, the two-infinite-summand assertion is not a published input. The finite-factor argument has been proved using library Dirichlet and CRT.

theorem OAI.Ostmann.inverseGoldbach_of_twoInfiniteSummandsImpossible line 19
Source documentation
Reduction described after Theorem 2.3 in the manuscript.
```
theorem inverseGoldbach_of_twoInfiniteSummandsImpossible
    (hmain : TwoInfiniteSummandsImpossible) : InverseGoldbach := by
…
```
Mentions: OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.twoInfiniteSummandsImpossible_of_inverseGoldbach line 27
Source documentation
The technical two-infinite-set assertion follows from the main statement.
```
theorem twoInfiniteSummandsImpossible_of_inverseGoldbach
    (hmain : InverseGoldbach) : TwoInfiniteSummandsImpossible := by
…
```
Mentions: OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.inverseGoldbach_iff_twoInfiniteSummandsImpossible line 33
Source documentation
Finite summands create no additional unresolved case of the conjecture.
```
theorem inverseGoldbach_iff_twoInfiniteSummandsImpossible :
    InverseGoldbach ↔ TwoInfiniteSummandsImpossible :=
…
```
Mentions: OAI.Ostmann.TwoInfiniteSummandsImpossible
theorem OAI.Ostmann.no_decomposition_of_finite_modification line 39
Source documentation
The finite-modification wording follows from the symmetric-difference wording.
```
theorem no_decomposition_of_finite_modification
    (hmain : InverseGoldbach) {P A B : Set ℕ}
    (hP : (P ∆ primes).Finite) (hA : A.Nontrivial) (hB : B.Nontrivial) :
    sumset A B ≠ P := by
…
```
Mentions: OAI.Ostmann.primes, OAI.Ostmann.sumset