MixedObstruction.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.Certificate.MixedData.false_of_certificate line 13
Source documentation
The checked integer identity is incompatible with a nonnegative Gram expression and the actual uniform moment bounds.
```
theorem false_of_certificate (x : Fin 3237 → ℝ)
    (hx : ∀ i, |x i| ≤ 1) (hzero : x 0 = 1)
    (hsources : ∀ k, Integer.Sparse.eval (sourceRows k) x = 0)
    (hnonneg : 0 ≤ Integer.Combination.eval targetRows x rawCombination) : False := by
…
```
Mentions: OAI.MUB6.Certificate.Integer.Sparse.eval, OAI.MUB6.Certificate.MixedData.sourceRows, OAI.MUB6.Certificate.Integer.Combination.eval, OAI.MUB6.Certificate.MixedData.targetRows, OAI.MUB6.Certificate.MixedData.rawCombination
theorem OAI.MUB6.Certificate.MixedData.false_of_gram_interpretation line 24
Source documentation
A bridge to the exact, positively scaled six Gram forms discharges the nonnegativity premise without any numerical oracle.
```
theorem false_of_gram_interpretation (B : Fin 7 → Basis) (hB : IsMUBFamily B)
    (x : Fin 3237 → ℝ) (hx : ∀ i, |x i| ≤ 1) (hzero : x 0 = 1)
    (hsources : ∀ k, Integer.Sparse.eval (sourceRows k) x = 0)
    (hgram : Integer.Combination.eval targetRows x rawCombination =
      (denominator : ℝ) * GramNonnegative.sourceGram B) : False := by
…
```
Mentions: OAI.MUB6.Basis, OAI.MUB6.IsMUBFamily, OAI.MUB6.Certificate.Integer.Sparse.eval, OAI.MUB6.Certificate.MixedData.sourceRows, OAI.MUB6.Certificate.Integer.Combination.eval, OAI.MUB6.Certificate.MixedData.targetRows, OAI.MUB6.Certificate.MixedData.rawCombination, OAI.MUB6.Certificate.MixedData.denominator, OAI.MUB6.Certificate.GramNonnegative.sourceGram