From eff17a6252ced4dc3bebd6e431d14b145a34ddfb Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 29 Sep 2025 04:52:51 -0700
Subject: [PATCH] notes

---
 src/math/lp/nla_stellensatz.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/nla_stellensatz.cpp b/src/math/lp/nla_stellensatz.cpp
index 682e5b38c..c7af96f3e 100644
--- a/src/math/lp/nla_stellensatz.cpp
+++ b/src/math/lp/nla_stellensatz.cpp
@@ -49,11 +49,13 @@ Currently missed lemma:
 (46) - j5 + j23 + j27 >= 0
 (44) j4 - j7 - j25 >= 0
 
-j4 - j7 - j27 >= 1
+j4 - j7 - j27 >= 1       (from (51) + (46))
 j4 - j5 - j7 + j23 >= 1  (from (46))
-j4 - j5 + j23 >= 2
-j4 - j5 + j11 >= 2
-j4 - j5 >= 3
+j4 - j5 + j23 >= 2       (from (12))
+j4 - j5 + j11 >= 2       (from (38))
+j4j4 - j4j5 + j4j11 >= 2j4  (multiply by j4)
+j4j11 >= 2j4             (subtract 10 multiplied by j4)
+..
 ..
 
   */