Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Paper256.cone_not_spectrahedral line 17
theorem OAI.Paper256.main_result line 25
Source documentation
An explicit degree-20 hyperbolic polynomial in a 23-dimensional real space whose closed hyperbolicity cone is not spectrahedral.
Distinct definitions of this name: ComparatorChallenges/HyperbolicCones.lean:67 (same statement text; different proof or body). Qualify references as OAI.Paper256.main_result@path.
```
theorem main_result :
    Module.finrank ℝ Ambient = 23 ∧
    polynomial.IsHomogeneous 20 ∧
    polynomial.totalDegree = 20 ∧
    MvPolynomial.eval (coordinates basePoint) polynomial = 1 ∧
    (∀ (x : Ambient) (z : ℂ), (linePolynomial x).aeval z = 0 → z.im = 0) ∧
    ∀ (N : ℕ) (_hN : 0 < N) (L : Ambient →ₗ[ℝ] Sym N),
      cone ≠ {x | (L x : Mat N ℝ).PosSemidef} := by
…
```
Mentions: OAI.Paper256.Ambient, OAI.Paper256.coordinates, OAI.Paper256.basePoint, OAI.Paper256.polynomial, OAI.Paper256.linePolynomial, OAI.Paper256.Sym, OAI.Paper256.cone, OAI.Paper256.Mat