diff --git a/.claude/settings.local.json b/.claude/settings.local.json
deleted file mode 100644
index 3a1f913..0000000
--- a/.claude/settings.local.json
+++ /dev/null
@@ -1,22 +0,0 @@
-{
-  "permissions": {
-    "allow": [
-      "Bash(lake build:*)",
-      "Bash(git add:*)",
-      "Bash(git commit -m \"$\\(cat <<''EOF''\nfeat: add generic SMT-LIB binary relations and min/max relations\n\nAdd FpEqRel, FpLtRel, FpGtRel, FpLeqRel, FpGeqRel, and FpIsNaN as generic\nbinary relations parameterized over embedding v : RoundableEmbed X R,\nfollowing the BTRW15 paper definitions.\n\nAdd FpMinRel and FpMaxRel as relations \\(rather than functions\\) to capture\nthe IEEE-754 underspecification for ±0 cases where either value is valid.\n\nCo-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>\nEOF\n\\)\")",
-      "Bash(lake exe fp-lean fpMaxRel)",
-      "Bash(./.lake/build/bin/fp-lean:*)",
-      "Bash(git branch:*)",
-      "Bash(git ls-tree:*)",
-      "Bash(echo:*)",
-      "Bash(git commit:*)",
-      "Bash(git push:*)",
-      "Bash(git checkout:*)",
-      "Bash(git pull:*)",
-      "Bash(gh run view:*)",
-      "WebSearch",
-      "WebFetch(domain:github.com)",
-      "WebFetch(domain:raw.githubusercontent.com)"
-    ]
-  }
-}
diff --git a/Fp/Basic.lean b/Fp/Basic.lean
index 0524b17..b5c7850 100644
--- a/Fp/Basic.lean
+++ b/Fp/Basic.lean
@@ -59,7 +59,6 @@ instance : Repr (PackedFloat exWidth sigWidth) where
   reprPrec x _prec :=
     f!"\{ sign := {if x.sign then "-" else "+"}, ex := {x.ex}, sig := {x.sig} }"
 
-
 /--
 A fixed point number with specified exponent offset.
 -/
@@ -395,7 +394,7 @@ the canonical NaN for `exWidth = 3` and `sigWidth = 4` is `0.111.1000`.
 def getNaN (exWidth sigWidth : Nat) : PackedFloat exWidth sigWidth where
   sign := false
   ex := BitVec.allOnes exWidth
-  sig := BitVec.ofNat sigWidth (2 ^ (sigWidth - 1))
+  sig := BitVec.intMin sigWidth
 
 @[simp]
 theorem sign_getNaN (exWidth sigWidth : Nat) :
@@ -407,7 +406,7 @@ theorem ex_getNaN (exWidth sigWidth : Nat) :
 
 @[simp]
 theorem sig_getNaN (exWidth sigWidth : Nat) :
-    (PackedFloat.getNaN exWidth sigWidth).sig = BitVec.ofNat sigWidth (2 ^ (sigWidth - 1)) := rfl
+    (PackedFloat.getNaN exWidth sigWidth).sig = BitVec.intMin sigWidth := rfl
 
 /--
 Returns the infinity value of the specified sign for the given floating point
@@ -810,16 +809,7 @@ theorem isNaN_getZero {e s : Nat} (sign : Bool) :
 theorem isNaN_getNaN {e s : Nat}  :
     (PackedFloat.getNaN e s).isNaN = true := by
   simp [getNaN, isNaN]
-  by_cases hs : s = 0
-  · simp [hs]
-  · simp [hs]
-    intros hcontra
-    have := BitVec.toNat_inj.mpr hcontra
-    simp at this
-    rw [Nat.mod_eq_of_lt] at this
-    · have : 0 < 2 ^ (s - 1) := by exact Nat.two_pow_pos (s - 1)
-      grind
-    · apply Nat.pow_lt_pow_of_lt <;> grind
+  grind
 
 /--
 Returns the `PackedFloat` representation for the given `BitVec`.
@@ -1091,6 +1081,7 @@ instance : LE ExtRat where
   le a b := le a b
 
 
+
 @[simp]
 theorem le_def {a b : ExtRat} : a.le b = (a ≤ b) := rfl
 
@@ -1403,6 +1394,26 @@ theorem mul_comm (x y : ExtRat) : x * y = y * x := by
 
 end InfinityBehaviour
 
+theorem le_refl (x : ExtRat) : x ≤ x := by
+  rw [← ExtRat.le_def]
+  unfold ExtRat.le
+  grind
+
+theorem le_trans {x y z : ExtRat} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
+  rw [← ExtRat.le_def] at hxy hyz ⊢
+  unfold ExtRat.le at hxy hyz ⊢
+  grind
+
+theorem le_antisymm {x y : ExtRat} (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
+  rw [← ExtRat.le_def] at hxy hyx
+  unfold ExtRat.le at hxy hyx
+  grind
+
+instance : Std.IsPartialOrder ExtRat where
+  le_refl := le_refl
+  le_trans := by grind [le_trans]
+  le_antisymm := by grind [le_antisymm]
+
 
 def isNaN (r : ExtRat) : Bool :=
   r = .NaN
@@ -1428,8 +1439,6 @@ def bias (e : Nat) : Nat :=
 
 namespace PackedFloat
 
-def mkNaN (sign := false) (sig := BitVec.intMin s) : PackedFloat e s :=
-  { sign, ex := BitVec.allOnes e, sig }
 
 def toExtDyadic (pf : PackedFloat e s) : ExtDyadic :=
   bif pf.isNaN then
@@ -1461,6 +1470,48 @@ theorem toExtDyadic_eq_Infinity_of_isInfinite (pf : PackedFloat e s) (hp : pf.is
 def toExtRat (pf : PackedFloat e s) : ExtRat :=
   pf.toExtDyadic.toExtRat
 
+
+/--
+'An Automatable Formal Semantics for IEEE-754 Floating-Point Arithmetic',
+definition from the model of floating point.
+-/
+def le (x y : PackedFloat e s) : Prop :=
+    (x.isNaN ∧ y.isNaN) ∨
+    (¬ x.isNaN ∧ ¬ y.isNaN ∧
+      ((x.sign = true ∧ y.sign = false) ∨ -- x negative, y positive.
+      (x.sign = false ∧ y.sign = false ∧ x.ex.toInt < y.ex.toInt) ∨ -- both +ve, x smaller ex.
+      (x.sign = false ∧ y.sign = false ∧ x.ex = y.ex ∧ x.sig.toNat ≤ y.sig.toNat) ∨ -- both +ve, x smaller sig.
+      (x.sign = true ∧ y.sign = true ∧ y.ex.toInt < x.ex.toInt) ∨ -- both -ve, y smaller ex.
+      (x.sign = true ∧ y.sign = true ∧ x.ex = y.ex ∧ y.sig.toNat ≤ x.sig.toNat))
+    )
+
+instance {x y : PackedFloat e s} : Decidable (le x y) := by
+  simp [le]; infer_instance
+
+instance : LE (PackedFloat exWidth sigWidth) where
+  le x y := le x y
+
+@[simp]
+theorem le_def (x y : PackedFloat e s) :
+  x.le y = (x ≤ y) := rfl
+
+@[simp]
+theorem minus_zero_le_plus_zero {e s} :
+    (PackedFloat.getZero e s true ≤ PackedFloat.getZero e s false) =
+    (e = 0 → s = 0 ∨ ¬s = 0) := by
+  simp [getZero, ← PackedFloat.le_def, PackedFloat.le, PackedFloat.isNaN]
+
+@[simp]
+theorem plus_zero_not_le_minus_zero :
+    (PackedFloat.getZero e s false ≤ PackedFloat.getZero e s true) =
+    (e = 0 ∧ s = 0) := by
+  simp [getZero, ← PackedFloat.le_def, PackedFloat.le, PackedFloat.isNaN]
+
+
+instance {x y : PackedFloat e s} : Decidable (x ≤ y) := by
+    simp only [← PackedFloat.le_def]
+    infer_instance
+
 def toExtRat' (pf : PackedFloat e s) : ExtRat :=
   bif pf.isNaN then
     .NaN
@@ -1474,6 +1525,8 @@ def toExtRat' (pf : PackedFloat e s) : ExtRat :=
     -- `-(bias e - 1)` is slightly different from SMT-LIB standard `1 - bias e` to allow `e = 1`.
     .Number (pf.sign.toSign * (0 + pf.sig.toNat / 2 ^ s) * 2 ^ (-(bias e - 1 : Nat) : Int))
 
+
+
 @[simp]
 theorem toExtRat'_eq_zero_of_isZero (pf : PackedFloat e s) (hp : pf.isZero) :
     pf.toExtRat' = .Number 0 := by
@@ -1562,14 +1615,25 @@ theorem toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm {pf : PackedFloat e s} (hp
   simp [toExtRat', hnan, hinf, hzero, toNumberRat]
   grind
 
-@[simp]
-theorem toExtRat'_mkInfinity (sign : Bool) (hs : 0 < s := by grind) :
+@[simp, grind! .]
+theorem toExtRat'_getInfinity (sign : Bool) (hs : 0 < s := by grind) :
     (PackedFloat.getInfinity e s sign).toExtRat' = .Infinity sign := by
   have : (PackedFloat.getInfinity e s sign).isInfinite = true := by
     grind
   simp [hs]
 
+@[simp, grind! .]
+theorem isNaN_mkNaN : (PackedFloat.getNaN e s).isNaN = true := by
+  simp [getNaN, isNaN]
+  grind
+
 @[simp]
+theorem toExtRat'_mkNaN :
+    (PackedFloat.getNaN e s).toExtRat' = .NaN := by
+  rw [toExtRat']
+  simp
+
+@[simp, grind! .]
 axiom toExtRat'_getZero (sign : Bool) (hs : 0 < s := by grind) :
     (PackedFloat.getZero e s sign).toExtRat' = .Number 0 -- := by
   -- have : (PackedFloat.getZero e s sign).isZero = true := by
@@ -1577,6 +1641,100 @@ axiom toExtRat'_getZero (sign : Bool) (hs : 0 < s := by grind) :
   -- simp [this]
     -- grind
 
+/--
+Case splitting on the different values a packed float
+can have: it can be nan, infinity, zero, or a nonzero normal/subnormal.+
+-/
+@[elab_as_elim]
+theorem classification {P : PackedFloat e s → Prop}
+    (x : PackedFloat e s)
+    (nanCase : ∀ (n : PackedFloat e s), n.isNaN → P n)
+    (infCase : ∀ sign, P (PackedFloat.getInfinity e s sign))
+    (zeroCase : ∀ sign, P (PackedFloat.getZero e s sign))
+    (numCase : ∀ (n : PackedFloat e s), n.isNormOrNonzeroSubnorm → P n) :
+    P x := by
+  have := x.classification_exhaustive
+  simp at this
+  by_cases h1 : x.isNaN
+  · grind
+  · by_cases h2 : x.isInfinite
+    · grind
+    · by_cases h3 : x.isZero
+      · grind
+      · by_cases h4 : x.isNonzeroSubnorm
+        · grind
+        · by_cases h5 : x.isNorm
+          · grind
+          · grind
+
+@[simp, grind .]
+theorem PackedFloat.le_refl (x : PackedFloat e s) : x ≤ x := by simp [← PackedFloat.le_def, PackedFloat.le]
+
+@[simp, grind .]
+theorem PackedFloat.le_NaN (x : PackedFloat e s) :
+    x ≤ PackedFloat.getNaN e s ↔ x.isNaN := by
+  by_cases hx : x.isNaN
+  · simp only [hx, iff_true]
+    simp only [← PackedFloat.le_def, PackedFloat.le, hx]
+    simp only [isNaN_mkNaN, and_self, not_true_eq_false, false_and, true_or]
+  · simp [hx]
+    simp only [← PackedFloat.le_def, PackedFloat.le]
+    simp [hx]
+
+@[simp, grind .]
+theorem PackedFloat.NaN_le (x : PackedFloat e s)
+    : PackedFloat.getNaN e s ≤ x ↔ x.isNaN := by
+  simp only [← PackedFloat.le_def, PackedFloat.le]
+  simp only [isNaN_getNaN]
+  by_cases hx : x.isNaN
+  · simp [hx]
+  · simp [hx]
+
+@[simp]
+theorem le_iff_toExtRat_le_toExtRat_of_not_isZero (x y : PackedFloat e s)
+  (hx : ¬ x.isZero) (hy : ¬ y.isZero) :
+  x ≤ y ↔ x.toExtRat ≤ y.toExtRat := sorry
+
+-- recall that -0 ≤ +0. So if x has sign = false, then y also needs sign = false
+@[simp]
+theorem le_iff_sign_eq_of_isZero (x y : PackedFloat e s)
+  (hx : x.isZero) (hy : y.isZero) : x ≤ y ↔ (x.sign = false → y.sign = false) := by
+  sorry
+
+attribute [grind .] BitVec.toNat_inj
+attribute [grind .] BitVec.toInt_inj
+
+theorem PackedFloat.le_antisymm_of_ne_NaN
+  {x y : PackedFloat e s}
+  (hxy : x ≤ y) (hyx : y ≤ x) (hx : ¬ x.isNaN) (hy : ¬ y.isNaN) :
+    x = y := by
+  simp only [← PackedFloat.le_def] at hxy hyx
+  simp only [PackedFloat.le] at hxy hyx
+  simp [hx] at hxy hyx
+  simp [hy] at hxy hyx
+  grind [PackedFloat]
+
+theorem PackedFloat.le_antisymm_iff {x y : PackedFloat e s}
+  (hxy : x ≤ y) (hyx : y ≤ x) :
+  (x.isNaN ∧ y.isNaN) ∨ (¬ x.isNaN ∧ ¬ y.isNaN ∧ x = y) := by
+  by_cases hx : x.isNaN
+  · sorry
+  · sorry
+
+theorem PackedFloat.le_trans
+    {x y z : PackedFloat e s} (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
+  sorry
+
+@[simp]
+theorem le_zero_iff_sign_eq_true {x : PackedFloat e s} :
+    (x ≤ PackedFloat.getZero e s true) ↔ (x.sign = true) := by
+  simp only [PackedFloat.getZero, ← PackedFloat.le_def, PackedFloat.le]
+  sorry
+
+@[simp]
+theorem zero_le_iff_sign_eq_false {x : PackedFloat e s} :
+  (PackedFloat.getZero e s false ≤ x) ↔ (x.sign = false) := by sorry
+
 
 end PackedFloat
 
diff --git a/Fp/SmtLibSemantics.lean b/Fp/SmtLibSemantics.lean
index 291053d..be68576 100644
--- a/Fp/SmtLibSemantics.lean
+++ b/Fp/SmtLibSemantics.lean
@@ -3,6 +3,7 @@ import Fp.Rounding
 import Fp.UnpackedRound
 import Fp.Utils
 import Lean
+import Fp.Theorems.Packing
 open Lean
 
 
@@ -102,7 +103,7 @@ structure RoundableLower (X : Type) (R : Type) where
   lower : R → X
 
 /-- The default embedding of packed floats into the extended rationals. -/
-instance  : RoundableEmbed (PackedFloat e s) ExtRat where
+instance embedPackedFloatExtRat (e s) : RoundableEmbed (PackedFloat e s) ExtRat where
   embed (x : PackedFloat e s) : ExtRat := x.toExtRat
 
 
@@ -114,6 +115,14 @@ structure RoundableAdjunction (X : Type) (R : Type) extends
   RoundableUpper X R
   where
 
+/--
+This is the main property of a lawful rounding adjunction, which states that the lower and upper approximants
+are correct with respect to the embedding. Specifically, `lower` computes the greatest lower bound and `upper` computes the least upper bound of the embedding of `X` into `R`.
+-/
+class LawfulRoundableAdjunction [LE X] [ExtendedNumber R] (adj : RoundableAdjunction X R) where
+  adjunctionLower : ∀ (r : R) (x : X), adj.embed x ≤ r ↔ x ≤ adj.lower r
+  adjunctionUpper : ∀ (r : R) (x : X), r ≤ adj.embed x ↔ adj.upper r ≤ x
+
 /-- Check if the given rational `r` is *strictly in* the lower half
 of the interval `(embed (lower r), embed (upper r))`. -/
 structure RoundableLowerHalf (X : Type) (R : Type) where
@@ -254,6 +263,27 @@ end Round
 def IsLawfulLower [ExtendedNumber R] [RE : RoundableEmbed X R] (r : R) (lower : X) : Prop :=
   RE.embed lower ≤ r ∧ (∀ (lower' : X), RE.embed lower' ≤ r → RE.embed lower' ≤ RE.embed lower)
 
+@[grind →]
+theorem IsLawfulLower.functional [ExtendedNumber R] [RE : RoundableEmbed X R] [Std.IsPartialOrder R] (r : R) (lower1 lower2 : X) :
+  IsLawfulLower r lower1 → IsLawfulLower r lower2 → RE.embed lower1 = RE.embed lower2 := by
+  intro hl1 hl2
+  cases hl1 with
+  | intro hle1 hglb1 =>
+    cases hl2 with
+    | intro hle2 hglb2 =>
+      have hle12 : RE.embed lower1 ≤ RE.embed lower2 := hglb2 lower1 hle1
+      have hle21 : RE.embed lower2 ≤ RE.embed lower1 := hglb1 lower2 hle2
+      grind
+
+-- theorem IsLawfulLower_always_exists {X R} [Inhabited X] [ExtendedNumber R] [RE : RoundableEmbed X R] (r : R) :
+--   ∃ (x : X), IsLawfulLower r x := by
+-- apply Classical.byContradiction
+-- intros h
+-- simp at h
+-- simp [IsLawfulLower] at h
+
+
+
 open Classical in
 noncomputable def smtLibLower [Inhabited X] [ExtendedNumber R] [RoundableEmbed X R] : RoundableLower X R where
   lower (r : R) : X :=
@@ -262,10 +292,41 @@ noncomputable def smtLibLower [Inhabited X] [ExtendedNumber R] [RoundableEmbed X
     else
       default
 
+@[grind .]
+theorem embed_smtLibLower_eq_of_IsLawfulLower [Inhabited X] [ExtendedNumber R] [instEmbed : RoundableEmbed X R] [Std.IsPartialOrder R]  (r : R) (lower : X) :
+  IsLawfulLower r lower → instEmbed.embed (smtLibLower.lower r) = instEmbed.embed lower := by
+  intro hl
+  simp [smtLibLower]
+  split
+  case isTrue h =>
+    obtain ⟨x, hlx⟩ := h
+    have : instEmbed.embed x = instEmbed.embed lower := by
+      apply IsLawfulLower.functional r x lower hlx hl
+    grind
+  case isFalse h =>
+    simp at h
+    grind
+
+
+
+-- TODO: need to know that IsLawfulLower is functional.
+
 /-- 'upper' is a valid least upper bound for 'r'. -/
 def IsLawfulUpper [ExtendedNumber R] [RE : RoundableEmbed X R] (r : R) (upper : X) : Prop :=
   r ≤ RE.embed upper ∧ (∀ (upper' : X), r ≤ RE.embed upper' → RE.embed upper ≤ RE.embed upper')
 
+@[grind →]
+theorem IsLawfulUpper.functional [ExtendedNumber R] [RE : RoundableEmbed X R] [Std.IsPartialOrder R] (r : R) (upper1 upper2 : X) :
+  IsLawfulUpper r upper1 → IsLawfulUpper r upper2 → RE.embed upper1 = RE.embed upper2 := by
+  intro hu1 hu2
+  cases hu1 with
+  | intro hle1 lub1 =>
+    cases hu2 with
+    | intro hle2 lub2 =>
+      have hle12 : RE.embed upper2 ≤ RE.embed upper1 := lub2 upper1 hle1
+      have hle21 : RE.embed upper1 ≤ RE.embed upper2 := lub1 upper2 hle2
+      grind
+
 open Classical in
 noncomputable def smtLibUpper {X R} [Inhabited X] [ExtendedNumber R] [RoundableEmbed X R] : RoundableUpper X R where
   upper (r : R) : X :=
@@ -283,26 +344,165 @@ for better computational properties.
 We will show later that the `vlower` and `vupper` defined this way agree
 with the galois adjunction expected.
 -/
-noncomputable def smtLibV [Inhabited X] [ExtendedNumber R] [RoundableEmbed X R] :
+noncomputable def smtLibV [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
     RoundableAdjunction X R where
   embed := RoundableEmbed.embed
   lower := smtLibLower.lower
   upper := smtLibUpper.upper
 
+/-- TODO: is this the right way to deal with this? -/
+theorem smtLiV.embed_toRoundableEmbed_eq [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
+  (smtLibV embed).embed = embed.embed := rfl
+
+/-- TODO: is this the right way to deal with this? -/
+@[simp, grind =]
+theorem smtLiV.lower_toRoundableEmbed_eq [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
+  (smtLibV embed).lower = smtLibLower.lower := rfl
+
+@[simp, grind =]
+theorem smtLiV.upper_toRoundableEmbed_eq [Inhabited X] [ExtendedNumber R] (embed : RoundableEmbed X R) :
+  (smtLibV embed).upper = smtLibUpper.upper := rfl
+
+@[simp, grind =] -- TODO: what should be the simp nf?
+theorem RoundableEmbed_embedPackedFloatExtRat_eq_smtLibV_embed:
+    RoundableEmbed.embed (self := embedPackedFloatExtRat e s) = PackedFloat.toExtRat := rfl
+
+
+@[simp, grind .]
+theorem toExtRat'_smtLibLower_eq_toExtRat'_of_IsLawfulLower (r : ExtRat) (lower : PackedFloat e s) :
+    IsLawfulLower r lower → (smtLibLower.lower r : PackedFloat e s).toExtRat' = PackedFloat.toExtRat' lower := by
+  intros h
+  have := embed_smtLibLower_eq_of_IsLawfulLower r lower h
+  simp at this
+  assumption
+
+-- theorem isNaN_lower_eq
+
+@[simp, grind .]
+theorem IsLawfulLower_mkInfinity (hs : 0 < s) {sign : Bool} : IsLawfulLower (ExtRat.Infinity sign) (PackedFloat.getInfinity e s sign) := by
+  constructor
+  · simp
+    -- grind
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+  · intros lower hle
+    simp at hle
+    simp
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+
+@[simp, grind .]
+theorem IsLawfulUpper_mkInfinity (hs : 0 < s) {sign : Bool} : IsLawfulUpper (ExtRat.Infinity sign) (PackedFloat.getInfinity e s sign) := by
+  constructor
+  · simp
+    -- grind
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+  · intros upper hle
+    simp at hle
+    simp
+    rw [PackedFloat.toExtRat'_getInfinity]
+    grind
+
+@[simp, grind .]
+theorem IsLawfulLower_mkNaN : IsLawfulLower ExtRat.NaN (PackedFloat.mkNaN : PackedFloat e s) := by
+  constructor
+  simp
+  intros lower hLtNaN
+  simp at hLtNaN
+  simp [hLtNaN]
+
+@[simp, grind .]
+theorem IsLawfulUpper_mkNaN : IsLawfulUpper ExtRat.NaN (PackedFloat.mkNaN : PackedFloat e s) := by
+  constructor
+  simp
+  intros upper hNaNLe
+  simp at hNaNLe
+  simp [hNaNLe]
+
+@[simp, grind .]
+theorem IslawfulUpper_mkNumber (pf : PackedFloat e s): IsLawfulUpper pf.toExtRat' pf := by
+  constructor
+  · simp; grind
+  · simp
+
+@[simp, grind .]
+theorem IsLawfulLower_mkNumber (pf : PackedFloat e s) : IsLawfulLower pf.toExtRat' pf := by
+  constructor
+  · simp; grind
+  · simp
+
+@[simp]
+theorem isNaN_lower_NaN : (smtLibLower.lower ExtRat.NaN : PackedFloat e s).isNaN = true := sorry
+
+-- TODO: show that toExtRat is injective everywhere away from zero.
+
+/-- Lower returns the input at all points except zero. -/
+theorem lower_eq_of_ne_zero {r : ExtRat} {lower : PackedFloat e s}
+  (h : r = lower.toExtRat) (hr : r ≠ 0) :
+  (smtLibLower.lower r : PackedFloat e s) = lower := by sorry
+
+
+theorem lower_eq_plus_zero :
+  (smtLibLower.lower (0 : ExtRat) : PackedFloat e s) = PackedFloat.getZero e s false := sorry
+
+theorem upper_eq_minus_zero :
+  (smtLibLower.lower (0 : ExtRat) : PackedFloat e s) = PackedFloat.getZero e s true := sorry
+
+/-- Upper returns the input at all points except zero. -/
+theorem upper_eq_of_ne_zero {r : ExtRat} {upper : PackedFloat e s} (h : r = upper.toExtRat) (hr : r ≠ 0) :
+  (smtLibUpper.upper r : PackedFloat e s) = upper := by sorry
+
+ theorem lower_le (r : ExtRat) :
+  ((smtLibLower.lower r) : PackedFloat e s).toExtRat ≤ r := sorry
+
+theorem le_upper (r : ExtRat) :
+  r ≤ ((smtLibUpper.upper r) : PackedFloat e s).toExtRat := sorry
+
+instance (he : 0 < e) (hs : 0 < s) : LawfulRoundableAdjunction (smtLibV (embedPackedFloatExtRat e s)) where
+  adjunctionLower := by
+    intros r p
+    simp [instExtendedRat, ← PackedFloat.le_def,
+      PackedFloat.toExtRat_eq_toExtRat']
+    rw [PackedFloat.toExtRat']
+    induction p using PackedFloat.classification
+    case nanCase n hn =>
+      simp [hn]
+      constructor
+      · intros hr
+        simp at hr
+        -- TODO: extract this out into a separate boi.
+        subst hr
+        -- apply PackedFloat.toExtRat'_eq_NaN_of_isNaN (smtLibLower.lower ExtRat.NaN)
+        sorry
+      · sorry
+    case zeroCase sign =>
+      simp [he, show (e = 0) = False by grind, show (s = 0) = False by grind]
+      constructor
+      · intros h
+        sorry
+      · intros h
+        simp at h
+        sorry
+
+    case infCase sign => sorry
+    case numCase n hnum => sorry
+  adjunctionUpper := sorry
+
 @[simp]
 theorem smtLibV_embed_eq [Inhabited X]
-  [ExtendedNumber R] [RoundableEmbed X R]
-    : (smtLibV (X := X) (R := R)).embed = RoundableEmbed.embed := rfl
+  [ExtendedNumber R] (embed : RoundableEmbed X R)
+    : (smtLibV embed).embed = RoundableEmbed.embed := rfl
 
 @[simp]
 theorem smtLibV_lower_eq [Inhabited X]
-  [ExtendedNumber R] [RoundableEmbed X R]
-    : (smtLibV (X := X) (R := R)).lower = smtLibLower.lower := rfl
+  [ExtendedNumber R] (embed : RoundableEmbed X R)
+    : (smtLibV embed).lower = smtLibLower.lower := rfl
 
 @[simp]
 theorem smtLibV_upper_eq [Inhabited X]
-  [ExtendedNumber R] [RoundableEmbed X R]
-    : (smtLibV (X := X) (R := R)).upper = smtLibUpper.upper := rfl
+  [ExtendedNumber R] (embed : RoundableEmbed X R)
+    : (smtLibV embed).upper = smtLibUpper.upper := rfl
 
 /--
 The SMT-Lib definition of the rounding methods for any choice of rounding adjunction 'v'.
diff --git a/Fp/Theorems/SmtLibSemanticsQ.lean b/Fp/Theorems/SmtLibSemanticsQ.lean
index be8648b..db8fd6f 100644
--- a/Fp/Theorems/SmtLibSemanticsQ.lean
+++ b/Fp/Theorems/SmtLibSemanticsQ.lean
@@ -14,7 +14,9 @@ into a packed float of 'eout, sout' according to the SMT-Lib semantics.
 Our proofs will be against this definition.
 -/
 noncomputable abbrev smtLibRoundMethodQ (eout sout : Nat) : SmtLibSemantics.RoundMethod (PackedFloat eout sout) ExtRat :=
-  SmtLibSemantics.smtLibRoundMethod eout sout (R := ExtRat) (SmtLibSemantics.smtLibV) (SmtLibSemantics.smtLibV)
+  SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))
 
 end SmtLibSemanticsQ
 
diff --git a/Fp/Theorems/UnpackedRound.lean b/Fp/Theorems/UnpackedRound.lean
index 721f1f5..262984e 100644
--- a/Fp/Theorems/UnpackedRound.lean
+++ b/Fp/Theorems/UnpackedRound.lean
@@ -6,12 +6,14 @@ import Fp.Theorems.Packing
 
 
 namespace Fp
+open SmtLibSemantics
 
 @[simp]
 theorem roundQ_eq (eout sout : Nat) (rm : RoundingMode) (sign : Bool) (r : ExtRat):
     (Fp.SmtLibSemanticsQ.smtLibRoundMethodQ eout sout).round rm sign r =
     (SmtLibSemantics.smtLibRoundMethod eout sout
-      SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round rm sign
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).round rm sign
     r := rfl
 
 set_option warn.sorry false in
@@ -26,32 +28,42 @@ theorem upper_NaN_eq_PackedFloat_mkNaN :
 
 @[simp]
 theorem roundRNA_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRNA sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRNA sign
     (ExtRat.NaN) = PackedFloat.mkNaN := by
   simp [SmtLibSemantics.RoundMethod.roundRNA]
 
 @[simp]
 theorem roundRNE_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRNE sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRNE sign
     (ExtRat.NaN) = PackedFloat.mkNaN := by
   simp [SmtLibSemantics.RoundMethod.roundRNE]
 
 @[simp]
 theorem roundRTP_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRTP sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRTP sign
     (ExtRat.NaN) = PackedFloat.mkNaN := by
   simp [SmtLibSemantics.RoundMethod.roundRTP]
 
 @[simp]
 theorem roundRTN_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRTN sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRTN sign
     (ExtRat.NaN) = PackedFloat.mkNaN := by
   simp [SmtLibSemantics.RoundMethod.roundRTN]
   rcases sign <;> simp
 
 @[simp]
 theorem rountRTZ_mkNaN (eout sout : Nat) (sign : Bool) :
-  (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).roundRTZ sign
+  (SmtLibSemantics.smtLibRoundMethod eout sout
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+    (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).roundRTZ sign
     (ExtRat.NaN) = PackedFloat.mkNaN := by
   simp [SmtLibSemantics.RoundMethod.roundRTZ]
   rcases sign <;> simp
@@ -59,7 +71,9 @@ theorem rountRTZ_mkNaN (eout sout : Nat) (sign : Bool) :
 
 @[simp]
 theorem round_eq_mkNaN_of_NaN {sign} {eout sout : Nat} {rm : RoundingMode} :
-    (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round
+    (SmtLibSemantics.smtLibRoundMethod eout sout
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))).round
         rm sign ExtRat.NaN = PackedFloat.mkNaN := by
   rcases rm
   · simp
@@ -71,14 +85,34 @@ theorem round_eq_mkNaN_of_NaN {sign} {eout sout : Nat} {rm : RoundingMode} :
 set_option warn.sorry false in
 @[simp]
 theorem round_eq_mkZero_of_mkZero {zeroSign : Bool} {eout sout : Nat} {rm : RoundingMode} :
-    (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round
+    (SmtLibSemantics.smtLibRoundMethod eout sout
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))
+    ).round
         rm zeroSign (ExtRat.Number 0) = PackedFloat.getZero eout sout zeroSign := by
   rcases rm <;> sorry
 
+/--
+'uf' approximtes 'r' upto rounding.
+-/
+structure ApproximatesUptoRounding (uf : UnpackedFloat ein sin) (er : ExtRat) (eout sout : Nat) : Prop where
+  /-- we have at least 2 bits more, of guard and sticky. -/
+  hSigGe : sin + 2 ≥ sout
+  /-- we have at least as much exponent range. -/
+  hExpGe : ein ≥ eout -- we have at least as much exponent range
+  /-- rational values have (sout + 1) bits of precision. -/
+  hApproxUptoGuard : ∀ (r : Rat), .Number r = er → (uf.toRat - r).abs < (2 : Rat) ^ (-(sout + 1 : Int))
+  /-- the sticky bit is zero iff the number truncated upto the guard bit equals -/
+  hStickyBitCorrect : ∀ (r : Rat), .Number r = er → ((uf.sig.extractMsb' (sout + 1) (sin - (sout + 1)) ≠ 0) = decide (r = uf.toRat))
+
 set_option warn.sorry false in
-theorem roundQ_Number_eq_round (er : ExtRat) (uf : UnpackedFloat ein sin)
-    (hruf : ExtRat.Number uf.toRat = er) :
-    (SmtLibSemantics.smtLibRoundMethod eout sout SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round rm sign
+theorem roundQ_Number_eq_round
+    (er : ExtRat) (uf : UnpackedFloat ein sin)
+    (hruf : ApproximatesUptoRounding uf er eout sout) (rm : RoundingMode) (sign : Bool) :
+    (SmtLibSemantics.smtLibRoundMethod eout sout
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout sout))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat eout (sout + 1)))
+    ).round rm sign
       er =
       (UnpackedFloat.round uf rm).pack := by sorry
 
@@ -97,42 +131,35 @@ theorem roundQ_Number_eq_round (er : ExtRat) (uf : UnpackedFloat ein sin)
 
 @[simp]
 theorem roundQ_eq_round_of_Infinity {zeroSign infSign : Bool} {e s : Nat} {rm : RoundingMode} :
-    (SmtLibSemantics.smtLibRoundMethod e s SmtLibSemantics.smtLibV SmtLibSemantics.smtLibV).round rm zeroSign
+    (SmtLibSemantics.smtLibRoundMethod e s
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat e s))
+      (SmtLibSemantics.smtLibV (SmtLibSemantics.embedPackedFloatExtRat e (s + 1)))
+    ).round rm zeroSign
       (ExtRat.Infinity infSign) =
       PackedFloat.getInfinity e s infSign := by sorry
 
-/--
-Case splitting on the different values a packed float
-can have: it can be nan, infinity, zero, or a nonzero normal/subnormal.+
--/
-@[elab_as_elim]
-theorem PackedFloat.kindCasesNaNInfZeroNum {P : PackedFloat e s → Prop}
-    (x : PackedFloat e s)
-    (nanCase : ∀ (n : PackedFloat e s), n.isNaN → P n)
-    (infCase : ∀ sign, P (PackedFloat.getInfinity e s sign))
-    (zeroCase : ∀ sign, P (PackedFloat.getZero e s sign))
-    (numCase : ∀ (n : PackedFloat e s), n.isNormOrNonzeroSubnorm → P n) :
-    P x := by
-  have := x.classification_exhaustive
-  simp at this
-  by_cases h1 : x.isNaN
-  · grind
-  · by_cases h2 : x.isInfinite
-    · grind
-    · by_cases h3 : x.isZero
-      · grind
-      · by_cases h4 : x.isNonzeroSubnorm
-        · grind
-        · by_cases h5 : x.isNorm
-          · grind
-          · grind
 
 @[grind <=]
 theorem PackedFloat.eq_of_unpack_eq_unpack_of_isInfinity {x y : PackedFloat e s}
     (hs : 0 < s) (he : 0 < e)
     (hx : x.isInfinite) (hy : y.isInfinite) (h : x.unpack = y.unpack) :
     x = y := by
-  cases x using PackedFloat.kindCasesNaNInfZeroNum <;> try grind
+  cases x using PackedFloat.classification <;> try grind
+
+/--
+Purely arithmetic fact that needs to be proven,
+which should just be to show that the fixed point computation equals the
+rational multiplication.
+Actually, this is too strong, the theorem statemtnt should be able to state
+something weaker, that only upto (s+1) bits agree,
+and that the sticky bit is computed correctly.
+-/
+theorem ApproximatesUptoRounding_mul_mul
+  (a b : PackedFloat ein sin)
+  (ha : a.isNormOrNonzeroSubnorm = true)
+  (hb : b.isNormOrNonzeroSubnorm = true) :
+  ApproximatesUptoRounding (a.unpackNormOrNonzeroSubnorm.mul b.unpackNormOrNonzeroSubnorm)
+  (ExtRat.Number a.toNumberRat * ExtRat.Number b.toNumberRat) ein sin := sorry
 
 set_option warn.sorry false in
 /--
@@ -144,7 +171,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
     rm a b = PackedFloat.mul rm a b := by
   simp [SmtLibSemantics.SmtLibFunctions.mul]
   rw [PackedFloat.mul, EUnpackedFloat.mul]
-  cases a using PackedFloat.kindCasesNaNInfZeroNum
+  cases a using PackedFloat.classification
   case nanCase hnan =>
     simp [hnan]
     rw [round_eq_mkNaN_of_NaN]
@@ -153,7 +180,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
     rw [← ExtRat.mul_def]
     unfold ExtRat.mul
     simp
-    cases b using PackedFloat.kindCasesNaNInfZeroNum
+    cases b using PackedFloat.classification
     case nanCase hb =>
       simp [hb]
       -- | why does this not apply automatically?
@@ -184,7 +211,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
       sorry
   case zeroCase sign =>
     simp [he]
-    cases b using PackedFloat.kindCasesNaNInfZeroNum
+    cases b using PackedFloat.classification
     case nanCase hb =>
       simp [hb]
       rw [round_eq_mkNaN_of_NaN]
@@ -211,7 +238,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
     rw [PackedFloat.unpack_eq_mkNumber_of_isNormOrNonzeroSubnorm ha]
     rw [PackedFloat.toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm ha]
     -- interesting case, when a is a number.
-    cases b using PackedFloat.kindCasesNaNInfZeroNum
+    cases b using PackedFloat.classification
     case nanCase hb =>
       simp [hb]
       rw [round_eq_mkNaN_of_NaN]
@@ -237,10 +264,7 @@ theorem mul_eq_mul {ein sin : Nat} (hsin : 0 < sin) (he : 0 < ein)
       simp [this]
       have : ¬ b.isZero := by grind
       simp [this]
-      rw [roundQ_Number_eq_round]
       rw [PackedFloat.toExtRat'_eq_Number_of_isNormOrNonzeroSubnorm hb]
-      simp only [ExtRat.number_mul_number_eq, ExtRat.Number.injEq]
-      -- Purely arithmetic statement.
-      -- ⊢ (a.unpackNormOrNonzeroSubnorm.mul b.unpackNormOrNonzeroSubnorm).toRat = a.toNumberRat * b.toNumberRat
-      sorry
+      apply roundQ_Number_eq_round
+      apply ApproximatesUptoRounding_mul_mul <;> assumption
 end Fp
diff --git a/fp-real-theory/FpRealTheory/Smtlib.lean b/fp-real-theory/FpRealTheory/Smtlib.lean
index 647e90c..d6374db 100644
--- a/fp-real-theory/FpRealTheory/Smtlib.lean
+++ b/fp-real-theory/FpRealTheory/Smtlib.lean
@@ -149,7 +149,7 @@ noncomputable instance : ExtendedNumber ExtReal where
    isNaN r := r = .NaN
    smtLibEq r1 r2 := r1.eq r2
 
-instance : RoundableEmbed (PackedFloat e s) ExtReal where
+instance embedPackedFloatExtReal (e s : Nat) : RoundableEmbed (PackedFloat e s) ExtReal where
    embed := fun pf =>
       match pf.toExtRat with
       | .NaN => .NaN
@@ -159,7 +159,9 @@ instance : RoundableEmbed (PackedFloat e s) ExtReal where
 end ExtReal
 
 noncomputable def smtLibRealRounder : RoundMethod (PackedFloat e s) ExtReal :=
-   smtLibRoundMethod e s smtLibV smtLibV
+   smtLibRoundMethod e s
+      (smtLibV (ExtReal.embedPackedFloatExtReal e s))
+      (smtLibV (ExtReal.embedPackedFloatExtReal e (s + 1)))
 
 namespace RealSemantics
 open Classical