SeparatorArithmetic.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Integer arithmetic for the low-angular separators

The polynomial recurrence and integer sign inequalities in Appendix cert:winding use Gaussian integer coefficients in ascending order.

def OAI.DefocusingNLS.SeparatorArithmetic.scale line 16
def OAI.DefocusingNLS.SeparatorArithmetic.centerB line 17
def OAI.DefocusingNLS.SeparatorArithmetic.centerZ line 18
def OAI.DefocusingNLS.SeparatorArithmetic.addCoefficients line 20
def OAI.DefocusingNLS.SeparatorArithmetic.scaleCoefficients line 25
def OAI.DefocusingNLS.SeparatorArithmetic.mulLinear line 29
Source documentation
Multiplication by the linear polynomial a + scale * X.
```
def mulLinear (a : GaussianInt) (xs : List GaussianInt) : List GaussianInt :=
…
```
def OAI.DefocusingNLS.SeparatorArithmetic.backwardStep line 34
Source documentation
The exact backward recurrence, from n = 7 down to n = 0.
```
def backwardStep (ℓ n : ℕ) (xy : List GaussianInt × List GaussianInt) :
    List GaussianInt × List GaussianInt :=
…
```
def OAI.DefocusingNLS.SeparatorArithmetic.backwardCoefficients line 41
def OAI.DefocusingNLS.SeparatorArithmetic.windingCoefficient line 45
Source documentation
The coefficient Im ∑ xₖ conj(yⱼ₋ₖ) of the degree-fifteen polynomial.
```
def windingCoefficient (ℓ j : ℕ) : ℤ :=
…
```
def OAI.DefocusingNLS.SeparatorArithmetic.evaluationTerms line 52
Source documentation
Terms in the denominator-cleared evaluation of an axis polynomial at w = ε (q/100)². The coordinate is 0 for real and 1 for imaginary.
```
def evaluationTerms (ℓ c : ℕ) (ε q : ℤ) : List ℤ :=
…
```
def OAI.DefocusingNLS.SeparatorArithmetic.separatorMargin line 56
theorem OAI.DefocusingNLS.SeparatorArithmetic.sign_of_positive_margin line 61
Source documentation
A positive relative integer margin proves the requested strict sign.
```
theorem sign_of_positive_margin (ℓ c : ℕ) (ε q e : ℤ)
    (h : 0 < separatorMargin ℓ c ε q e) :
    0 < e * (evaluationTerms ℓ c ε q).sum := by
…
```
Mentions: OAI.DefocusingNLS.SeparatorArithmetic.separatorMargin, OAI.DefocusingNLS.SeparatorArithmetic.evaluationTerms
def OAI.DefocusingNLS.SeparatorArithmetic.positiveArguments line 79
def OAI.DefocusingNLS.SeparatorArithmetic.signCycle line 85
def OAI.DefocusingNLS.SeparatorArithmetic.signOffset line 92
def OAI.DefocusingNLS.SeparatorArithmetic.rowMargins line 99
Source documentation
All margins in one row of the appendix, including the negative-argument tests when they are required.
```
def rowMargins (ℓ : ℕ) : List ℤ :=
…
```
theorem OAI.DefocusingNLS.SeparatorArithmetic.row_zero_margin line 109
Source documentation
The four exact minimum margins reported in cert:separator-margins.
```
theorem row_zero_margin : (rowMargins 0).min? = some 583 := by decide +kernel
```
Mentions: OAI.DefocusingNLS.SeparatorArithmetic.rowMargins
theorem OAI.DefocusingNLS.SeparatorArithmetic.row_one_margin line 111
theorem OAI.DefocusingNLS.SeparatorArithmetic.row_two_margin line 113
theorem OAI.DefocusingNLS.SeparatorArithmetic.row_three_margin line 115
theorem OAI.DefocusingNLS.SeparatorArithmetic.row_margin_pos line 117