diff --git a/SSA.lean b/SSA.lean
index 4323deb1d..3ab665533 100644
--- a/SSA.lean
+++ b/SSA.lean
@@ -8,6 +8,7 @@ import SSA.Core.Framework
 
 -- Eventually, all projects must be imported.
 import SSA.Projects.InstCombine.Alive
+import SSA.Projects.FullyHomomorphicEncryption
 import SSA.Projects.Tensor1D.Tensor1D
 import SSA.Projects.Tensor2D.Tensor2D
 import SSA.Projects.Holor.Holor
diff --git a/SSA/Projects/FullyHomomorphicEncryption.lean b/SSA/Projects/FullyHomomorphicEncryption.lean
new file mode 100644
index 000000000..22ca1cd7b
--- /dev/null
+++ b/SSA/Projects/FullyHomomorphicEncryption.lean
@@ -0,0 +1,2 @@
+import SSA.Projects.FullyHomomorphicEncryption.Basic
+import SSA.Projects.FullyHomomorphicEncryption.Statements
\ No newline at end of file
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
index bef519c67..fb1ddcf37 100644
--- a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
+++ b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
@@ -13,16 +13,21 @@ https://eprint.iacr.org/2012/144
 import Mathlib.RingTheory.Polynomial.Quotient
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.Ideal.QuotientOperations
-import Mathlib.Data.Zmod.Basic
-import SSA.Experimental.IntrinsicAsymptotics
+import Mathlib.Data.ZMod.Defs
+import Mathlib.Data.ZMod.Basic
+import Mathlib.Algebra.MonoidAlgebra.Basic
+import Mathlib.Data.Finset.Sort
+import Mathlib.Data.List.ToFinsupp
+import Mathlib.Data.Polynomial.RingDivision
+import SSA.Core.Framework
 
 open Polynomial -- for R[X] notation
 
 /-
-We assume tat `q > 1` is a natural number (not necessarily a prime) and `n` is a natural number.
+We assume that `q > 1` is a natural number (not necessarily a prime) and `n` is a natural number.
 We will use these to build `ℤ/qℤ[X]/(X^(2^n) + 1)`
 -/
-variable (q t : Nat) [Fact (q > 1)] (n : Nat)
+variable (q t : Nat) [ hqgt1 : Fact (q > 1)] (n : Nat)
 
 -- Can we make this computable?
 -- see: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Way.20to.20recover.20computability.3F/near/322382109
@@ -30,11 +35,11 @@ variable (q t : Nat) [Fact (q > 1)] (n : Nat)
 
 -- Question: Can we make something like d := 2^n work as a macro?
 --
-theorem WithBot.npow_coe_eq_npow (n : Nat) (x : ℕ) : (WithBot.some x : WithBot ℕ) ^ n = WithBot.some (x ^ n) := by
+theorem WithBot.coe_pow (n : Nat) (x : ℕ) : (WithBot.some x : WithBot ℕ) ^ n = WithBot.some (x ^ n) := by
   induction n with
     | zero => simp
     | succ n ih =>
-        rw [pow_succ'', ih, ← WithBot.coe_mul]
+        rw [pow_succ, ih, ← WithBot.coe_mul]
         rw [← WithBot.some_eq_coe, WithBot.some]
         apply Option.some_inj.2
         rw [Nat.pow_succ]
@@ -43,6 +48,48 @@ theorem WithBot.npow_coe_eq_npow (n : Nat) (x : ℕ) : (WithBot.some x : WithBot
 
 noncomputable def f : (ZMod q)[X] := X^(2^n) + 1
 
+-- theorem zmodq_eq_finq : ZMod q = Fin q := by
+--   have h : q > 1 := hqgt1.elim
+--   unfold ZMod
+--   cases q
+--   · exfalso
+--     apply Nat.not_lt_zero 1
+--     exact h
+--   · simp [Fin]
+--   done
+
+def ZMod.toInt (x : ZMod q) : Int := ZMod.cast x
+def ZMod.toFin (x : ZMod q) : Fin q := ZMod.cast x
+
+@[simp]
+theorem ZMod.toInt_inj {x y : ZMod q} : x.toInt = y.toInt ↔ x = y := by
+  constructor
+  · intro h
+    simp [toInt] at h
+    apply ZMod.val_injective
+    rw[ZMod.cast_eq_val] at h
+    rw[ZMod.cast_eq_val] at h
+    norm_cast at h
+  · intro h
+    rw [h]
+
+def ZMod.toInt_zero_iff_zero (x : ZMod q) : x = 0 ↔ x.toInt = 0 := by
+  constructor
+  · intro h
+    rw [h]
+    simp [toInt]
+  · intro h
+    have h0 : ZMod.toInt q 0 = (0 : Int) := by simp [ZMod.toInt]
+    rw [← h0] at h
+    apply (ZMod.toInt_inj q).1
+    assumption
+
+instance : Nontrivial (ZMod q) where
+  exists_pair_ne := by
+    exists 0
+    exists 1
+    norm_num
+
 /-- Charaterizing `f`: `f` has degree `2^n` -/
 theorem f_deg_eq : (f q n).degree = 2^n := by
   simp [f]
@@ -59,7 +106,7 @@ theorem f_deg_eq : (f q n).degree = 2^n := by
   have h2 : @OfNat.ofNat (WithBot ℕ) 2 instOfNat = @WithBot.some ℕ 2 := by
     simp [OfNat.ofNat]
   have h2n : @HPow.hPow (WithBot ℕ) ℕ (WithBot ℕ) instHPow 2 n = @WithBot.some ℕ (@HPow.hPow ℕ ℕ ℕ instHPow 2 n) := by
-    rw [h2, WithBot.npow_coe_eq_npow]
+    rw [h2, WithBot.coe_pow]
   rw [h0, h2n]
   exact h'
   done
@@ -81,22 +128,43 @@ abbrev R := (ZMod q)[X] ⧸ (Ideal.span {f q n})
 -- Coefficients of `a : R' q n` are `a\_i : Zmod q`.
 -- TODO: get this from mathlib
 
-/-- Canonical epimorphism `ZMod q[X] ->*+ R q n` -/
+/-- Canonical epimorphism / quotient map: `ZMod q[X] ->*+ R q n` -/
 abbrev R.fromPoly {q n : Nat} : (ZMod q)[X] →+* R q n := Ideal.Quotient.mk (Ideal.span {f q n})
 
-noncomputable abbrev R.zero {q n : Nat} : R q n := R.fromPoly 0
-noncomputable abbrev R.one {q n : Nat} : R q n := R.fromPoly 1
+/-- fromPoly, the canonical epi from `ZMod q[X] →*+ R q n` is surjective -/
+theorem R.surjective_fromPoly (q n : ℕ) : Function.Surjective (R.fromPoly (q := q) (n := n)) := by
+  simp[R.fromPoly]
+  apply Ideal.Quotient.mk_surjective
+
+private noncomputable def R.representative' : R q n → (ZMod q)[X] := Function.surjInv (R.surjective_fromPoly q n)
 
-noncomputable instance {q n : Nat} : Zero (R q n) := ⟨R.zero⟩
-noncomputable instance {q n : Nat} : One (R q n) := ⟨R.one⟩
+theorem R.injective_representative' (q n : ℕ) : Function.Injective (R.representative' (q := q) (n := n)) := by
+  simp[R.representative']
+  apply Function.injective_surjInv
+
+/-- A concrete version that shows that mapping into the ideal back from the representative produces the representative'
+  NOTE: Lean times out if I use the abbreviation `R.fromPoly` for unclear reasons! -/
+theorem R.fromPoly_representatitive' (a : R q n) : R.fromPoly (R.representative' q n a) = ↑ a := by
+  simp[R.fromPoly, R.representative']
+  apply Function.surjInv_eq
+
+theorem R.fromPoly_representatitive'_toFun (a : R q n) : (R.fromPoly (q := q) (n := n)).toFun (R.representative' q n a) = ↑a := by
+  apply Function.surjInv_eq
 
-private noncomputable def R.representative' : R q n → (ZMod q)[X] := Function.surjInv Ideal.Quotient.mk_surjective
 /--
 The representative of `a : R q n` is the (unique) polynomial `p : ZMod q[X]` of degree `< 2^n`
  such that `R.fromPoly p = a`.
 -/
 noncomputable def R.representative : R q n → (ZMod q)[X] := fun x => R.representative' q n x %ₘ (f q n)
 
+@[simp]
+theorem R.fromPoly_kernel_eq_zero (x : (ZMod q)[X]) : R.fromPoly (n := n) (f q n * x) = 0 := by
+   unfold fromPoly
+   apply Ideal.Quotient.eq_zero_iff_mem.2
+   rw [Ideal.mem_span_singleton]
+   simp [Dvd.dvd]
+   use x
+
 /--
 `R.representative` is in fact a representative of the equivalence class.
 -/
@@ -106,24 +174,17 @@ theorem R.fromPoly_representative : forall a : R q n, (R.fromPoly (n:=n) (R.repr
  simp [R.representative]
  rw [Polynomial.modByMonic_eq_sub_mul_div _ (f_monic q n)]
  rw [RingHom.map_sub (R.fromPoly (q := q) (n:=n)) _ _]
- have hker : forall x, fromPoly (f q n * x) = 0 := by
-   intro x
-   unfold fromPoly
-   apply Ideal.Quotient.eq_zero_iff_mem.2
-   rw [Ideal.mem_span_singleton]
-   simp [Dvd.dvd]
-   use x
- rw [hker _]
+ rw [R.fromPoly_kernel_eq_zero]
  simp
  apply Function.surjInv_eq
 
 
 /--
-Characterization theorem for any potential representative.
+Characterization theorem for any potential representative (in terms of ideals).
 For an  `a : (ZMod q)[X]`, the representative of its equivalence class
 is just `a + i` for some `i ∈ (Ideal.span {f q n})`.
 -/
-theorem R.fromPoly_rep'_eq : forall a : (ZMod q)[X], ∃ i ∈ Ideal.span {f q n}, (R.fromPoly (n:=n) a).representative' = a + i := by
+theorem R.fromPoly_rep'_eq_ideal : forall a : (ZMod q)[X], ∃ i ∈ Ideal.span {f q n}, (R.fromPoly (n:=n) a).representative' = a + i := by
   intro a
   exists (R.fromPoly (n:=n) a).representative' - a
   constructor
@@ -131,22 +192,176 @@ theorem R.fromPoly_rep'_eq : forall a : (ZMod q)[X], ∃ i ∈ Ideal.span {f q n
     simp [R.representative', Function.surjInv_eq]
   · ring
   done
+/--
+Characterization theorem for any potential representative (in terms of elements).
+For an  `a : (ZMod q)[X]`, the representative of its equivalence class
+is a concrete element of the form `a + k * (f q n)` for some `k ∈ (ZMod q)[X]`.
+-/
+theorem R.exists_representative_fromPoly_eq_mul_add (a : (ZMod q)[X]) : ∃ (k : (ZMod q)[X]), (R.fromPoly (n:=n) a).representative' = k * (f q n) + a := by
+  have H : ∃ i ∈ Ideal.span {f q n}, (R.fromPoly (n:=n) a).representative' = a + i := by
+    apply R.fromPoly_rep'_eq_ideal
+  obtain ⟨i, iInIdeal, ih⟩ := H
+  have fqn_div_i : (f q n) ∣ i  := by
+    rw[← Ideal.mem_span_singleton]
+    assumption
+  have i_multiple_fqn : ∃ (k : (ZMod q)[X]), i = k * (f q n) := by
+    apply dvd_iff_exists_eq_mul_left.mp
+    assumption
+  obtain ⟨k, hk⟩ := i_multiple_fqn
+  exists k
+  subst hk
+  rw[ih]
+  ring_nf
+
+/-- A theorem similar to `R.fromPoly_rep'_eq_element` but uses `fromPoly.toFun` to be more deterministic,
+  as the `toFun` sometimes sneaks in due to coercions. -/
+theorem R.representatitive'_toFun_fromPoly_eq_element (a : (ZMod q)[X]) : ∃ (k : (ZMod q)[X]),
+  R.representative' q n ((R.fromPoly (q := q) (n := n)).toFun a) = a + k * (f q n) := by
+  have H : ∃ (k : (ZMod q)[X]), (R.fromPoly (n:=n) a).representative' = k * (f q n) + a := by apply
+    R.exists_representative_fromPoly_eq_mul_add;
+  obtain ⟨k, hk⟩ := H
+  exists k
+  ring_nf at hk ⊢
+  rw[← hk]
+  norm_cast
+
+/-- The representative of 0 wil live in the ideal of {f q n}. To show that such an element is a multiple of {f q n}, use `Ideal.mem_span_singleton'`-/
+theorem R.representative'_zero_ideal : R.representative' q n 0 ∈ Ideal.span {f q n} := by
+  have H : ∃ i ∈ Ideal.span {f q n}, (R.fromPoly (n:=n) 0).representative' = 0 + i := by apply R.fromPoly_rep'_eq_ideal (a := 0)
+  obtain ⟨i, hi, hi'⟩ := H
+  simp[fromPoly] at hi'
+  rw[hi']
+  assumption
+
+/-- The representatiatve of 0 is a multiple of `f q n`. -/
+theorem R.representative'_zero_elem : ∃ (k : (ZMod q)[X]), R.representative' q n 0 = k * (f q n) := by
+  have H : ∃ k : (ZMod q)[X], (R.fromPoly (n:=n) 0).representative' = k * (f q n) + 0 := by apply R.exists_representative_fromPoly_eq_mul_add (a := 0)
+  obtain ⟨k, hk⟩ := H
+  simp[fromPoly] at hk
+  rw[hk]
+  exists k
+
+/-- Representative of (0 : R) is (0 : Z/qZ[X]) -/
+theorem R.representative_zero : R.representative q n 0 = 0 := by
+  simp[R.representative]
+  obtain ⟨k, hk⟩ := R.representative'_zero_elem q n
+  rw[hk]
+  rw[dvd_iff_modByMonic_eq_zero]
+  simp
+  exact (f_monic q n)
 
 /--
 Characterization theorem for the representative.
 Taking the representative of the equivalence class of a polynomial  `a : (ZMod q)[X]` is
 the same as taking the remainder of `a` modulo `f q n`.
 -/
+theorem R.representative_fromPoly_toFun : forall a : (ZMod q)[X], ((R.fromPoly (n:=n) (q := q)).toFun a).representative = a %ₘ (f q n) := by
+  intro a
+  simp [R.representative]
+  have ⟨i,⟨hiI,hi_eq⟩⟩ := R.fromPoly_rep'_eq_ideal q n a
+  simp[FunLike.coe] at hi_eq
+  rw [hi_eq]
+  apply Polynomial.modByMonic_eq_of_dvd_sub (f_monic q n)
+  ring_nf
+  apply Ideal.mem_span_singleton.1 hiI
+  done
+
 theorem R.representative_fromPoly : forall a : (ZMod q)[X], (R.fromPoly (n:=n) a).representative = a %ₘ (f q n) := by
   intro a
   simp [R.representative]
-  have ⟨i,⟨hiI,hi_eq⟩⟩ := R.fromPoly_rep'_eq q n a
+  have ⟨i,⟨hiI,hi_eq⟩⟩ := R.fromPoly_rep'_eq_ideal q n a
   rw [hi_eq]
   apply Polynomial.modByMonic_eq_of_dvd_sub (f_monic q n)
   ring_nf
   apply Ideal.mem_span_singleton.1 hiI
   done
 
+/-- Representative is an additive homomorphism -/
+@[simp]
+theorem R.representative_add [Fact (q > 1)](a b : R q n) : (a + b).representative = a.representative + b.representative := by
+  have ⟨a', ha'⟩ := R.surjective_fromPoly q n a
+  have ⟨b', hb'⟩ := R.surjective_fromPoly q n b
+  have ⟨ab', hab'⟩ := R.surjective_fromPoly q n (a + b)
+  rw[← hab']
+  subst ha'
+  subst hb'
+  rw[← map_add] at hab'
+  rw[hab']
+  repeat rw[R.representative_fromPoly]
+  rw[Polynomial.add_modByMonic]
+
+/-- pushing and pulling negation through mod -/
+theorem neg_modByMonic (p mod : (ZMod q)[X]) : (-p) %ₘ mod = - (p %ₘ mod) := by
+    have H : -p = (-1 : ZMod q) • p := by norm_num
+    have H' : - (p %ₘ mod) = (-1 : ZMod q) • (p %ₘ mod) := by norm_num
+    rw[H, H']
+    apply smul_modByMonic (R := (ZMod q)) (c := -1) (p := p) (q := mod)
+
+/-- %ₘ is a subtraction homomorphism (obviously)-/
+@[simp]
+theorem sub_modByMonic (a b mod : (ZMod q)[X]) : (a - b) %ₘ mod = a %ₘ mod - b %ₘ mod := by
+  ring_nf
+  repeat rw[sub_eq_add_neg]
+  simp[Polynomial.add_modByMonic]
+  rw[neg_modByMonic]
+
+/-- Representative is an multiplicative homomorphism upto modulo -/
+@[simp]
+theorem R.representative_mul [Fact (q > 1)] (a b : R q n) : (a * b).representative = (a.representative * b.representative) %ₘ (f q n) := by
+  have ⟨a', ha'⟩ := R.surjective_fromPoly q n a
+  have ⟨b', hb'⟩ := R.surjective_fromPoly q n b
+  have ⟨ab', hab'⟩ := R.surjective_fromPoly q n (a * b)
+  rw[← hab']
+  subst ha'
+  subst hb'
+  rw[← map_mul] at hab'
+  rw[hab']
+  repeat rw[R.representative_fromPoly]
+  -- rw[modByMonic_eq_sub_mul_div (p := a' * b') (_hq := f_monic q n)]
+  rw[modByMonic_eq_sub_mul_div (p := a') (_hq := f_monic q n)]
+  rw[modByMonic_eq_sub_mul_div (p := b') (_hq := f_monic q n)]
+  ring_nf
+  repeat rw[Polynomial.add_modByMonic]
+  ring_nf
+  repeat rw[sub_modByMonic]
+
+  have H1 : (-(a' * f q n * (b' /ₘ f q n))) %ₘ f q n = 0 := by
+    rw[Polynomial.dvd_iff_modByMonic_eq_zero (hq := f_monic q n)]
+    rw[dvd_neg]
+    apply dvd_mul_of_dvd_left
+    apply dvd_mul_of_dvd_right
+    apply dvd_rfl
+  rw[H1]
+  have H2 : b' * f q n * (a' /ₘ f q n) %ₘ f q n = 0 := by
+    rw[Polynomial.dvd_iff_modByMonic_eq_zero (hq := f_monic q n)]
+    apply dvd_mul_of_dvd_left
+    apply dvd_mul_of_dvd_right
+    apply dvd_rfl
+  rw[H2]
+  have H3 : f q n ^ 2 * (b' /ₘ f q n) * (a' /ₘ f q n) %ₘ f q n = 0 := by
+    rw[Polynomial.dvd_iff_modByMonic_eq_zero (hq := f_monic q n)]
+    apply dvd_mul_of_dvd_left
+    apply dvd_mul_of_dvd_left
+    apply dvd_pow_self
+    simp
+  rw[H3]
+  ring
+
+/- characterize representative', very precisely, in terms of elements -/
+/-
+theorem R.representative'_iff (r : R q n) (p : (ZMod q)[X]) :
+  (∃ (k : (ZMod q)[X]), (R.representative' q n r) = (k * (f q n) + p)) ↔ (fromPoly (n := n) (q := q) p = r) := by
+  constructor
+-/
+
+/-- Another characterization of the representative: if the degree of x is less than that of (f q n),
+then we recover the same polynomial. -/
+@[simp]
+theorem R.representative_fromPoly_eq (x : (ZMod q)[X]) (DEGREE: x.degree < (f q n).degree) :
+   R.representative q n (R.fromPoly (n:=n) x) = x := by
+   simp[R.representative_fromPoly]
+   rw[modByMonic_eq_self_iff] <;> simp[DEGREE, f_monic]
+
 /--
 The representative of `a : R q n` is the (unique) reperesntative with degree `< 2^n`.
 -/
@@ -157,18 +372,45 @@ theorem R.rep_degree_lt_n : forall a : R q n, (R.representative q n a).degree <
   apply Polynomial.degree_modByMonic_lt
   exact f_monic q n
 
+/-- The representative `a : R q n` is the (unique) representative with degree less than degree of `f`. -/
+theorem R.representative_degree_lt_f_degree {q n : ℕ} [Fact (q > 1)] : forall a : R q n, (R.representative q n a).degree < (f q n).degree := by
+  rw[f_deg_eq (q := q)]
+  intros a
+  apply R.rep_degree_lt_n
+
+noncomputable def R.repLength {q n} (a : R q n) : Nat := match
+  Polynomial.degree a.representative with
+    | none => 0
+    | some d => d + 1
+
+theorem R.repLength_lt_n_plus_1 : forall a : R q n, a.repLength < 2^n + 1 := by
+  intro a
+  simp [R.repLength, representative]
+  have : Polynomial.degree ( R.representative' q n a %ₘ f q n) < 2^n := by
+    rw [← f_deg_eq q n]
+    apply (Polynomial.degree_modByMonic_lt)
+    apply f_monic
+  simp[LT.lt] at this
+  let ⟨val, VAL, VAL_EQN⟩ := this
+  rcases H : degree (R.representative' q n a %ₘ f q n) <;> simp[this]
+  case some val' =>
+    specialize (VAL_EQN _ H)
+    norm_cast at VAL
+    cases VAL
+    norm_cast at VAL_EQN
+
 /--
 This function gets the `i`th coefficient of the polynomial representative
 (with degree `< 2^n`) of an element `a : R q n`. Note that this is not
 invariant under the choice of representative.
 -/
-noncomputable def R.coeff (a : R q n) (i : Nat) : ZMod q :=
+noncomputable def R.coeff {q n} (a : R q n) (i : Nat) : ZMod q :=
   Polynomial.coeff a.representative i
 
 /--
 `R.monomial i c` is the equivalence class of the monomial `c * X^i` in `R q n`.
 -/
-noncomputable def R.monomial {q n : Nat} (i : Nat) (c : ZMod q) : R q n :=
+noncomputable def R.monomial {q n : Nat} (c : ZMod q) (i : Nat): R q n :=
   R.fromPoly (Polynomial.monomial i c)
 
 /--
@@ -182,70 +424,260 @@ noncomputable def R.slice {q n : Nat} (a : R q n) (startIdx endIdx : Nat) : R q
   let coeffIdxs := List.range (endIdx - startIdx)
   let coeffs := coeffIdxs.map (fun i => a.coeff (startIdx + i))
   let accum : R q n → (ZMod q × Nat) → R q n :=
-    fun poly (c,i) => poly + R.monomial (n:=n) i c
-  coeffs.zip coeffIdxs |>.foldl accum R.zero
+    fun poly (c,i) => poly + R.monomial (n:=n) c i
+  coeffs.zip coeffIdxs |>.foldl accum (0 : R q n)
+
+noncomputable def R.leadingTerm {q n} (a : R q n) : R q n :=
+  let deg? := Polynomial.degree a.representative
+  match deg? with
+    | .none => 0
+    | .some deg =>  R.monomial (a.coeff deg) deg
+
+noncomputable def R.fromTensor {q n} (coeffs : List Int) : R q n :=
+  coeffs.enum.foldl (init := 0) fun res (i,c) =>
+    res + R.monomial ↑c i
+
+/- `fromTensor (cs ++ [c])` equals `(fromTensor xs) + c X^n` -/
+theorem R.fromTensor_snoc (q n : ℕ) (c : ℤ) (cs : List ℤ) : R.fromTensor (q := q) (n := n) (cs ++ [c])
+  = (R.fromTensor (q := q) (n := n) cs) + R.monomial c cs.length := by
+    induction cs using List.reverseRecOn generalizing c
+    case H0 =>
+      simp[fromTensor]
+    case H1 xs x _hxs =>
+      simp[fromTensor]
+      repeat rw[List.enum_append]
+      repeat rw[List.foldl_append]
+      simp[List.enumFrom]
+
+/-- A definition of fromTensor that operates on Z/qZ[X], to provide a relationship between
+    R and Z/qZ[X] as the polynomial in R is built.
+-/
+noncomputable def R.fromTensor' (coeffs : List Int) : (ZMod q)[X] :=
+  coeffs.enum.foldl (init := 0) fun res (i,c) =>
+    res + (Polynomial.monomial i ↑c)
+
+theorem R.fromTensor_eq_fromTensor'_fromPoly_aux (coeffs : List Int) (rp : R q n) (p : (ZMod q)[X])
+  (H : R.fromPoly (q := q) (n := n) p = rp) :
+  ((List.enumFrom k coeffs).foldl (init := rp) fun res (i,c) =>
+    res + R.monomial ↑c i) =
+  R.fromPoly (q := q) (n := n)
+    ((List.enumFrom k coeffs).foldl (init := p) fun res (i,c) =>
+      res + (Polynomial.monomial i ↑c)) := by
+      induction coeffs generalizing p rp k
+      case nil =>
+        simp[List.enum, H]
+      case cons head tail tail_ih =>
+        simp[List.enum_cons]
+        specialize tail_ih (k := k + 1) (rp := (rp + monomial (↑head) k)) (p := (p + ↑(Polynomial.monomial k ↑head)))
+        apply tail_ih
+        simp[monomial, H]
+
+/-- fromTensor = R.fromPoly ∘ fromTensor'.
+This permits reasoning about fromTensor directly on the polynomial ring.
+-/
+theorem R.fromTensor_eq_fromTensor'_fromPoly {q n} : R.fromTensor (q := q) (n := n) coeffs =
+  R.fromPoly (q := q) (n := n) (R.fromTensor' q coeffs) := by
+    simp[fromTensor, fromTensor']
+    induction coeffs
+    . simp[List.enum]
+    . simp[List.enum_cons]
+      apply fromTensor_eq_fromTensor'_fromPoly_aux
+      simp[monomial]
+
+
+/-- an equivalent implementation of `fromTensor` that uses `Finsupp` to enable reasoning about values using mathlib's notions of
+  support, coefficients, etc. -/
+noncomputable def R.fromTensorFinsupp (coeffs : List ℤ) : (ZMod q)[X] :=
+  Polynomial.ofFinsupp (List.toFinsupp (coeffs.map Int.cast))
+
+/-- concatenating into a `fromTensorFinsupp` is the same as adding a ⟨Finsupp.single⟩. -/
+theorem R.fromTensorFinsupp_concat_finsupp {q : ℕ} (c : ℤ) (cs : List ℤ) :
+    (R.fromTensorFinsupp (q := q) (cs ++ [c])) = (R.fromTensorFinsupp (q := q) cs) + ⟨Finsupp.single cs.length (Int.cast c : (ZMod q))⟩ := by
+    simp only[fromTensorFinsupp]
+    simp only[← Polynomial.ofFinsupp_add]
+    simp only[List.map_append, List.map]
+    simp only[List.toFinsupp_concat_eq_toFinsupp_add_single]
+    simp only[List.length_map]
+
+/-- concatenating into a `fromTensorFinsupp` is the same as adding a monomial. -/
+theorem R.fromTensorFinsupp_concat_monomial {q : ℕ} (c : ℤ) (cs : List ℤ) :
+    (R.fromTensorFinsupp (q := q) (cs ++ [c])) = (R.fromTensorFinsupp (q := q) cs) + (Polynomial.monomial cs.length (Int.cast c : (ZMod q))) := by
+    simp[fromTensorFinsupp]
+    rw[← Polynomial.ofFinsupp_single]
+    simp only[List.toFinsupp_concat_eq_toFinsupp_add_single]
+    simp only[← Polynomial.ofFinsupp_add]
+    rw[List.length_map]
+
+/-- show that `fromTensor` is the same as `fromPoly ∘ fromTensorFinsupp`. -/
+theorem R.fromTensor_eq_fromTensorFinsupp_fromPoly {q n} : R.fromTensor (q := q) (n := n) coeffs =
+  R.fromPoly (q := q) (n := n) (R.fromTensorFinsupp q coeffs) := by
+    simp[fromTensor, fromTensor']
+    induction coeffs  using List.reverseRecOn
+    case H0 => simp[List.enum, fromTensorFinsupp]
+    case H1 c cs hcs =>
+      simp[List.enum_append]
+      simp[R.fromTensorFinsupp_concat_monomial]
+      rw[hcs]
+      congr
+
+/-- `coeff (p % f) = coeff p` if the degree of `p` is less than the degree of `f`. -/
+theorem coeff_modByMonic_degree_lt_f {q n i : ℕ} [Fact (q > 1)] (p : (ZMod q)[X]) (DEGREE : p.degree < (f q n).degree) :
+  (p %ₘ f q n).coeff i = p.coeff i := by
+  have H := (modByMonic_eq_self_iff (hq := f_monic q n) (p := p)).mpr DEGREE
+  simp[H]
+
+/-- The coefficient of `fromPoly p` is the coefficient of `p` modulo `f q n`. -/
+@[simp]
+theorem R.coeff_fromPoly {q n : ℕ} [Fact (q > 1)] (p : (ZMod q)[X]) : R.coeff (R.fromPoly (q := q) (n := n) p) = Polynomial.coeff (p %ₘ (f q n)) := by
+  simp[R.coeff]
+  simp[FunLike.coe]
+  have H := R.representative_fromPoly_toFun (a := p) (n := n)
+  norm_cast at H ⊢
+
+
+/-- since `0` is the additive identity, getting from `(x :: xs)` at index `i` with -/
+theorem List.getD_snoc_zero (x : ℤ) (xs : List ℤ) :
+  (xs ++ [x]).getD i 0 = (xs.getD i 0) + (if i == xs.length then x else 0) := by sorry
+
+/-- The coefficient of `fromTensor` is the same as the values available in the tensor input. -/
+theorem R.coeff_fromTensor [hqgt1 : Fact (q > 1)] (tensor : List Int): (R.fromTensor (q := q) (n := n) tensor).coeff i = (tensor.getD i 0) := by
+  induction tensor using List.reverseRecOn
+  case H0 =>
+    simp[fromTensor, coeff, representative_zero]
+  case H1 cs c hcs =>
+    simp[fromTensor_snoc]
+    rw[fromTensor_eq_fromTensor'_fromPoly]
+    by_cases (i < cs.length)
+    case pos =>
+      rw[List.getD_eq_get (hn := by simp[List.append]; linarith)]
+      simp[fromTensor_eq_fromTensor'_fromPoly]
+      simp[coeff]
+      ring_nf
+      simp only[FunLike.coe]
+      rw[representative_fromPoly_toFun (n := n) (a := fromTensor' q cs)]
+      sorry
+    case neg =>
+      by_cases (i = cs.length)
+      case pos =>
+        subst h
+        sorry
+      case neg =>
+        have hi : i > cs.length := by
+          obtain H := Nat.lt_trichotomy i cs.length
+          cases H
+          . linarith
+          . case inr H =>
+              cases H
+              . contradiction
+              . linarith
+        rw[List.getD_eq_default (hn := by simp[List.length_append]; linarith)]
+        sorry
+
+theorem R.representative_fromTensor_eq_fromTensor' (tensor : List ℤ) : R.representative q n (R.fromTensor tensor) = R.representative' q n (R.fromTensor' q tensor)  %ₘ (f q n) := by
+  simp [R.representative]
+  rw[fromTensor_eq_fromTensor'_fromPoly];
+
+/--
+Converts an element of `R` into a tensor (modeled as a `List Int`)
+with the representatives of the coefficients of the representative.
+The length of the list is the degree of the representative + 1.
+-/
+noncomputable def R.toTensor {q n} [Fact (q > 1)] (a : R q n) : List Int :=
+  List.range a.repLength |>.map fun i =>
+        a.coeff i |>.toInt
+
+/--
+Converts an element of `R` into a tensor (modeled as a `List Int`)
+with the representatives of the coefficients of the representative.
+The length of the list is the degree of the generator polynomial `f` + 1.
+-/
+noncomputable def R.toTensor' {q n} [Fact (q > 1)] (a : R q n) : List Int :=
+  let t := a.toTensor
+  t ++ List.replicate (2^n - t.length + 1) 0
+
+def trimTensor (tensor : List Int) : List Int
+  := tensor.reverse.dropWhile (· = 0) |>.reverse
 
 /--
 We define the base type of the representation, which encodes both natural numbers
 and elements in the ring `R q n` (which in FHE are sometimes called 'polynomials'
  in allusion to `R.representative`).
+
+ In this context, `Tensor is a 1-D tensor, which we model here as a list of integers.
 -/
-inductive Ty
-  | nat : Ty
-  | poly (q : Nat) (n : Nat) : Ty
+inductive Ty (q : Nat) (n : Nat) [Fact (q > 1)]
+  | index : Ty q n
+  | integer : Ty q n
+  | tensor : Ty q n
+  | polynomialLike : Ty q n
   deriving DecidableEq
 
-instance : Inhabited Ty := ⟨Ty.nat⟩
-instance : Goedel Ty where
+instance : Inhabited (Ty q n) := ⟨Ty.index⟩
+instance : Goedel (Ty q n) where
 toType := fun
-  | .nat => Nat
-  | .poly q n => (R q n)
+  | .index => Nat
+  | .integer => Int
+  | .tensor => List Int
+  | .polynomialLike => (R q n)
+
 
 /--
 The operation type of the `Poly` dialect. Operations are parametrized by the
 two parameters `p` and `n` that characterize the ring `R q n`.
+We parametrize the entire type by these since it makes no sense to mix operations in different rings.
 -/
-inductive Op
-| add (q : Nat) (n : Nat) : Op
-| sub (q : Nat) (n : Nat) : Op
-| mul (q : Nat) (n : Nat) : Op
-| mul_constant (q : Nat) (n : Nat) (c : R q n) : Op
-| get_coeff (q : Nat) (n : Nat) : Op
-| extract_slice (q : Nat) (n : Nat) : Op
---deriving DecidableEq --, Repr
+inductive Op (q : Nat) (n : Nat) [Fact (q > 1)]
+  | add : Op q n-- Addition in `R q n`
+  | sub : Op q n-- Substraction in `R q n`
+  | mul : Op q n-- Multiplication in `R q n`
+  | mul_constant : Op q n-- Multiplication by a constant of the base ring (we assume this to be a `.integer` and take its representative)
+  | leading_term : Op q n-- Leading term of representative
+  | monomial : Op q n-- create a monomial
+  | monomial_mul : Op q n-- multiply by(monic) monomial
+  | from_tensor : Op q n-- interpret values as coefficients of a representative
+  | to_tensor : Op q n-- give back coefficients from `R.representative`
+  | const (c : R q n) : Op q n
 
 open Goedel (toType)
 
 
 @[simp, reducible]
-def Op.sig : Op  → List Ty
-| Op.add q n => [Ty.poly q n, Ty.poly q n]
-| Op.sub q n => [Ty.poly q n, Ty.poly q n]
-| Op.mul q n => [Ty.poly q n, Ty.poly q n]
-| Op.mul_constant q n _ => [Ty.poly q n]
-| Op.get_coeff q n => [Ty.poly q n, Ty.nat]
-| Op.extract_slice q n => [Ty.poly q n, Ty.nat, Ty.nat]
+def Op.sig : Op  q n → List (Ty q n)
+| Op.add => [Ty.polynomialLike, Ty.polynomialLike]
+| Op.sub => [Ty.polynomialLike, Ty.polynomialLike]
+| Op.mul => [Ty.polynomialLike, Ty.polynomialLike]
+| Op.mul_constant => [Ty.polynomialLike, Ty.integer]
+| Op.leading_term => [Ty.polynomialLike]
+| Op.monomial => [Ty.integer, Ty.index]
+| Op.monomial_mul => [Ty.polynomialLike, Ty.index]
+| Op.from_tensor => [Ty.tensor]
+| Op.to_tensor => [Ty.polynomialLike]
+| Op.const _ => []
+
+@[simp, reducible]
+def Op.outTy : Op q n → Ty q n
+| Op.add | Op.sub | Op.mul | Op.mul_constant | Op.leading_term | Op.monomial
+| Op.monomial_mul | Op.from_tensor | Op.const _  => Ty.polynomialLike
+| Op.to_tensor => Ty.tensor
 
 @[simp, reducible]
-def Op.outTy : Op → Ty
-| Op.add q n => Ty.poly q n
-| Op.sub q n => Ty.poly q n
-| Op.mul q n => Ty.poly q n
-| Op.mul_constant q n _ => Ty.poly q n
-| Op.get_coeff _ _ => Ty.nat
-| Op.extract_slice q n => Ty.poly q n
+def Op.signature : Op q n → Signature (Ty q n) :=
+  fun o => {sig := Op.sig q n o, outTy := Op.outTy q n o, regSig := []}
 
-instance : OpSignature Op Ty := ⟨Op.sig, Op.outTy⟩
+instance : OpSignature (Op q n) (Ty q n) := ⟨Op.signature q n⟩
 
-variable (a b : R q n)
 @[simp]
-noncomputable def Op.denote (o : Op)
+noncomputable def Op.denote (o : Op q n)
    (arg : HVector toType (OpSignature.sig o))
    : (toType <| OpSignature.outTy o) :=
     match o with
-    | Op.add q n => (fun args : R q n × R q n => args.1 + args.2) arg.toPair
-    | Op.sub q n => (fun args : R q n × R q n => args.1 - args.2) arg.toPair
-    | Op.mul q n => (fun args : R q n × R q n => args.1 * args.2) arg.toPair
-    | Op.mul_constant q n c => (fun arg : R q n => arg * c) arg.toSingle
-    | Op.get_coeff q n => (fun args : R q n × Nat => args.1.coeff args.2 |>.val) arg.toPair
-    | Op.extract_slice _ _ => (fun (a,i,c) => R.slice a i c) arg.toTriple
\ No newline at end of file
+    | Op.add => (fun args : R q n × R q n => args.1 + args.2) arg.toPair
+    | Op.sub => (fun args : R q n × R q n => args.1 - args.2) arg.toPair
+    | Op.mul => (fun args : R q n × R q n => args.1 * args.2) arg.toPair
+    | Op.mul_constant => (fun args : R q n × Int => args.1 * ↑(args.2)) arg.toPair
+    | Op.leading_term => R.leadingTerm arg.toSingle
+    | Op.monomial => (fun args => R.monomial ↑(args.1) args.2) arg.toPair
+    | Op.monomial_mul => (fun args : R q n × Nat => args.1 * R.monomial 1 args.2) arg.toPair
+    | Op.from_tensor => R.fromTensor arg.toSingle
+    | Op.to_tensor => R.toTensor' arg.toSingle
+    | Op.const c => c
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
new file mode 100644
index 000000000..05d65dd03
--- /dev/null
+++ b/SSA/Projects/FullyHomomorphicEncryption/Rewrites.lean
@@ -0,0 +1,43 @@
+import SSA.Projects.FullyHomomorphicEncryption.Basic
+import SSA.Projects.FullyHomomorphicEncryption.Statements
+import SSA.Projects.MLIRSyntax.EDSL
+
+theorem dialect_mul_comm :
+[mlir_icom| {
+^bb0(%A : P, %B : P):
+  %v1 = "poly.mul" (%A,%B) : (P, P) -> (P)
+  "poly.return" (%v1) : (P) -> ()
+}] = 
+[mlir_icom| {
+^bb0(%A : P, %B : P):
+  %v1 = "poly.mul" (%A,%B) : (P, P) -> (P)
+  "poly.return" (%v1) : (P) -> ()
+}]=  := by
+  simp_mlir
+  apply poly_mul_comm
+
+theorem dialect_add_comm : a + b = b + a := by
+  ring
+
+theorem dialect_f_eq_zero : (f q n) = (0 : R q n) := by
+  apply Ideal.Quotient.eq_zero_iff_mem.2
+  rw [Ideal.mem_span_singleton]
+
+theorem dialect_mul_f_eq_zero : a * (f q n) = 0 := by
+  rw [dialect_f_eq_zero]; ring
+
+theorem dialect_mul_one_eq : 1 * a = a := by
+  ring
+
+theorem dialect_add_f_eq : a + (f q n) = a := by
+  rw [← dialect_mul_one_eq q n (f q n), dialect_mul_f_eq_zero _ _ 1]; ring
+
+theorem dialect_add_zero_eq : a + 0 = a := by
+  ring
+
+
+
+
+
+
+
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Statements.lean b/SSA/Projects/FullyHomomorphicEncryption/Statements.lean
new file mode 100644
index 000000000..894acd758
--- /dev/null
+++ b/SSA/Projects/FullyHomomorphicEncryption/Statements.lean
@@ -0,0 +1,293 @@
+import SSA.Projects.FullyHomomorphicEncryption.Basic
+import Std.Data.List.Lemmas
+import Mathlib.Data.List.Basic
+
+-- variable {q t : Nat} [ hqgt1 : Fact (q > 1)] {n : Nat}
+-- variable (a b : R q n)
+
+namespace Poly
+
+theorem mul_comm (a b : R q n) : a * b = b * a := by
+  ring
+
+theorem add_comm (a b : R q n) : a + b = b + a := by
+  ring
+
+@[simp]
+theorem f_eq_zero : (f q n) = (0 : R q n) := by
+  apply Ideal.Quotient.eq_zero_iff_mem.2
+  rw [Ideal.mem_span_singleton]
+
+theorem mul_f_eq_zero (a : R q n): a * (f q n) = 0 := by
+  rw [f_eq_zero]; ring
+
+theorem mul_one_eq (a : R q n) : 1 * a = a := by
+  ring
+
+theorem add_f_eq (a : R q n) : a + (f q n) = a := by
+  rw[f_eq_zero]
+  ring
+
+theorem add_zero_eq : a + 0 = a := by
+  ring
+
+theorem eq_iff_rep_eq [Fact (q > 1)] (a b : R q n) : a.representative = b.representative ↔ a = b := by
+  constructor
+  · intros hRep
+    have hFromPolyRep : R.fromPoly (q := q) (n := n) a.representative = R.fromPoly (q := q) (n := n) b.representative := by
+      rw [hRep]
+    rw [R.fromPoly_representative, R.fromPoly_representative] at hFromPolyRep
+    assumption
+  · intro h; rw [h]
+
+open Polynomial in
+theorem from_poly_zero : R.fromPoly (0 : (ZMod q)[X]) (n := n) = (0 : R q n) := by
+  have hzero : f q n * 0 = 0 := by simp
+  rw [← hzero]
+  apply R.fromPoly_kernel_eq_zero
+
+theorem rep_zero [Fact (q > 1)]: R.representative q n 0 = 0 := by
+  rw [← from_poly_zero, R.representative_fromPoly]; simp
+
+
+open Polynomial in
+theorem monomial_mul_mul (x y : Nat) : (R.monomial 1 y) * (R.monomial 1 x) = R.monomial 1 (x + y) (q := q) (n := n) := by
+  unfold R.monomial
+  rw [← map_mul, monomial_mul_monomial, Nat.add_comm]
+  simp
+
+end Poly
+
+theorem R.toTensor_length [hqgt1 : Fact (q > 1)] (a : R q n) : a.toTensor.length = a.repLength := by
+  unfold R.toTensor
+  unfold R.repLength
+  cases Polynomial.degree a.representative <;> simp
+
+
+theorem R.toTensor_getD [hqgt1 : Fact (q > 1)] (a : R q n) (i : Nat) : a.toTensor.getD i 0 = (a.coeff i).toInt := by
+  simp [R.toTensor, R.coeff]
+  have hLength : (List.map (fun i => ZMod.toInt q (Polynomial.coeff (R.representative q n a) i)) (List.range (R.repLength a))).length = repLength a := by
+    simp
+  by_cases (i < R.repLength a)
+  case pos =>
+    rw [← hLength] at h; rw [List.getD_eq_get _ _ h, List.get_map, List.get_range]
+    done
+  case neg =>
+    rw [Nat.not_lt] at h
+    rw [List.getD_eq_default _, Polynomial.coeff_eq_zero_of_degree_lt]
+    simp[ZMod.toInt]
+    unfold R.repLength at h
+    cases hDeg : Polynomial.degree (R.representative q n a)
+    · apply WithBot.bot_lt_coe
+    . simp[hDeg] at h
+      apply WithBot.some_lt_some.2
+      linarith
+    . rw[← hLength] at h
+      linarith
+
+theorem R.toTensor_getD' [hqgt1 : Fact (q > 1)] (a : R q n) (i : Nat) : ↑(a.toTensor.getD i 0) = a.coeff i := by
+  rw [R.toTensor_getD]
+  simp [ZMod.toInt]
+
+theorem R.monomial_zero_c_eq_zero : R.monomial (q := q) (n := n) 0 c = 0 := by
+  unfold R.monomial
+  rw [Polynomial.monomial_zero_right]
+  simp
+
+theorem R.fromTensor_eq_concat_zero (tensor : List Int) :
+  R.fromTensor (q := q) (n := n) tensor = R.fromTensor (q := q) (n := n) (tensor ++ [0]) := by
+  unfold R.fromTensor
+  simp
+  rw [List.enum_append, List.enumFrom_singleton, List.foldl_concat]
+  simp [R.monomial_zero_c_eq_zero]
+
+
+theorem R.fromTensor_eq_concat_zeroes (tensor : List Int) (k : Nat) :
+   R.fromTensor (q := q) (n := n) (tensor ++ List.replicate k 0) = R.fromTensor (q := q) (n := n) tensor := by
+  induction k generalizing tensor with
+   | zero => simp
+   | succ k ih =>
+       simp [ih]
+       have H : tensor ++ (0 :: List.replicate k 0) = (tensor ++ [0]) ++ List.replicate k 0 :=
+        List.append_cons ..
+       rw[H]
+       rw [ih (tensor ++ [0])]
+       rw[← R.fromTensor_eq_concat_zero]
+
+@[simp]
+theorem R.trimTensor_append_zero_eq (tensor : List Int) :  trimTensor (tensor ++ [0]) = trimTensor tensor := by
+  simp [trimTensor]
+  rw [List.dropWhile]
+  simp
+
+@[simp]
+theorem R.trimTensor_append_zeroes_eq (tensor : List Int) (n : Nat) :  trimTensor (tensor ++ List.replicate n 0) = trimTensor tensor := by
+  induction n with
+  | zero => simp
+  | succ n ih =>
+     rw [List.replicate_succ', ← List.append_assoc, R.trimTensor_append_zero_eq,ih]
+
+theorem R.trimTensor_append_not_zero (tensor : List Int) (x : Int) (hX : x ≠ 0) :
+  trimTensor (tensor ++ [x]) = tensor ++ [x] := by
+  simp [trimTensor]; rw [List.dropWhile]
+  simp [hX]
+
+theorem R.trimTensor_eq_append_zeros (tensor : List Int) : ∃ (n : Nat),
+tensor = trimTensor tensor ++ List.replicate n 0 := by
+induction tensor using List.reverseRecOn with
+   | H0 => exists 0
+   | H1 xs x ih =>
+     have ⟨n,hxs⟩ := ih
+     by_cases (x = 0)
+     · exists (n + 1)
+       rw [h]
+       simp
+       rw [← List.replicate_succ, List.replicate_succ', ← List.append_assoc, ← hxs]
+     · exists 0
+       rw [R.trimTensor_append_not_zero _ _ h] ; simp
+
+theorem R.trimTensor_getD_0 (tensor: List Int) :
+  tensor.getD i 0 = (trimTensor tensor).getD i 0 := by
+  have ⟨n, H⟩ := trimTensor_eq_append_zeros tensor
+  conv =>
+    lhs
+    rw[H]
+  by_cases INBOUNDS:(i < List.length (trimTensor tensor))
+  . rw[List.getD_append (h := INBOUNDS)]
+  . have OUT_OF_BOUNDS : List.length (trimTensor tensor) ≤ i := by linarith
+    rw[List.getD_eq_default (hn := OUT_OF_BOUNDS)]
+    rw[List.getD_append_right (h := OUT_OF_BOUNDS)]
+    rw[List.getD_replicate_default_eq]
+
+theorem R.trimTensor_trimTensor (tensor : List Int) :
+  trimTensor (trimTensor tensor) = trimTensor tensor := by
+  induction tensor using List.reverseRecOn with
+    | H0 => simp
+    | H1 xs x ih =>
+       by_cases (x = 0)
+       · rw [h, R.trimTensor_append_zero_eq,ih]
+       · rw [trimTensor_append_not_zero _ _ h, trimTensor_append_not_zero _ _ h]
+
+theorem R.fromTensor_eq_fromTensor_trimTensor (tensor : List Int) :
+   R.fromTensor (q := q) (n := n) (trimTensor tensor) = R.fromTensor (q := q) (n := n) tensor := by
+  have ⟨n,hn⟩ := R.trimTensor_eq_append_zeros tensor
+  conv =>
+    rhs
+    rw [hn]
+  simp[R.fromTensor_eq_concat_zeroes]
+
+theorem R.trimTensor_toTensor'_eq_trimTensor_toTensor [hqgt1 : Fact (q > 1)] (a : R q n) :
+  trimTensor a.toTensor' = trimTensor a.toTensor := by
+  apply R.trimTensor_append_zeroes_eq
+
+namespace Poly
+
+theorem eq_iff_coeff_eq [hqgt1 : Fact (q > 1)] (a b : R q n) : a = b ↔ Polynomial.coeff a.representative = Polynomial.coeff b.representative := by
+  constructor
+  .  intro h; rw [h]
+  ·  intro h
+     apply (eq_iff_rep_eq _ _).1
+     apply Polynomial.coeff_inj.1
+     exact h
+
+theorem toTensor_length_eq_rep_length [hqgt1 : Fact (q > 1)] (a : R q n) :
+  a.toTensor.length = a.repLength := by
+  simp [R.repLength, R.toTensor]
+
+-- Surely this doesn't need to be this annoying
+theorem toTensor_length_eq_f_deg_plus_1 [hqgt1 : Fact (q > 1)] (a : R q n) :
+  a.toTensor'.length = 2^n + 1 := by
+  rw [R.toTensor', List.length_append, toTensor_length_eq_rep_length, List.length_replicate]
+  have h : R.repLength a ≤ 2^n  := Nat.le_of_lt_succ (R.repLength_lt_n_plus_1 q n a)
+  calc
+       R.repLength a + (2 ^ n - R.repLength a + 1)
+     = R.repLength a + (Nat.succ (2 ^ n) - R.repLength a) := by rw [Nat.add_comm _ 1, ← Nat.add_sub_assoc h, Nat.add_comm 1 (2^n)]
+   _ = 2^n + 1 := by rw [Nat.add_sub_cancel' (Nat.le_succ_of_le h)]
+
+
+theorem toTensor_trimTensor_eq_toTensor [hqgt1 : Fact (q > 1)] (a : R q n) :
+  trimTensor a.toTensor = a.toTensor := by
+  unfold R.toTensor
+  cases h : Polynomial.degree a.representative with
+  | none => simp [h, R.repLength]
+  | some n  =>
+    simp [R.repLength, h]
+    rw [List.range_succ, List.map_append]
+    simp
+    have hNe := Polynomial.coeff_ne_zero_of_eq_degree h
+    simp [R.coeff, hNe]
+    have hNe': ZMod.toInt q (Polynomial.coeff (a.representative) n) ≠ 0 := by
+      intro contra
+      have contra' := (ZMod.toInt_zero_iff_zero _ _).2 contra
+      contradiction
+    apply R.trimTensor_append_not_zero  _ _ hNe'
+
+theorem R.trim_toTensor'_eq_toTensor [hqgt1 : Fact (q > 1)] (a : R q n) :
+  trimTensor a.toTensor' = a.toTensor := by
+  rw [R.trimTensor_toTensor'_eq_trimTensor_toTensor, toTensor_trimTensor_eq_toTensor]
+
+
+theorem toTensor_fromTensor [hqgt1 : Fact (q > 1)] (tensor : List Int) (i : Nat):
+  (R.fromTensor tensor (q:=q) (n :=n)).toTensor.getD i 0 = (tensor.getD i 0) % q := by
+  simp[R.toTensor_getD]
+
+  simp[ZMod.toInt];
+  simp[R.coeff_fromTensor]
+  norm_cast
+  simp[Int.cast, ZMod.cast]
+  cases q;
+  case zero =>
+    exfalso
+    simp at hqgt1
+    exact (Fact.elim hqgt1)
+  case succ q' =>
+    simp
+    simp[ZMod.cast]
+    norm_cast
+    simp[IntCast.intCast]
+    norm_cast
+    ring_nf
+    rw[ZMod.cast_eq_val]
+    rw[ZMod.val_int_cast]
+    ring_nf
+
+theorem toTensor_fromTensor_trimTensor_eq_trimTensor [hqgt1 : Fact (q > 1)] (a : R q n) (tensor : List Int) {l : Nat}:
+  Polynomial.degree a.representative = .some l → tensor.length < l →
+  (R.fromTensor (trimTensor tensor) (q:=q) (n :=n)).toTensor = trimTensor tensor := by
+  intros hDeg hLen
+  simp [R.fromTensor, R.toTensor]
+  sorry
+
+theorem toTensor_fromTensor_eq_trimTensor [hqgt1 : Fact (q > 1)] (a : R q n) (tensor : List Int) {l : Nat}:
+  Polynomial.degree a.representative = .some l → tensor.length < l →
+  (R.fromTensor tensor (q:=q) (n :=n)).toTensor = trimTensor tensor := by
+  intros hDeg hLen
+  --simp [R.fromTensor, R.toTensor]
+  have ⟨n,hTrim⟩ := R.trimTensor_eq_append_zeros tensor
+  rw [hTrim,R.trimTensor_append_zeroes_eq, R.fromTensor_eq_concat_zeroes, R.trimTensor_trimTensor]
+  apply toTensor_fromTensor_trimTensor_eq_trimTensor _ _ hDeg hLen
+
+theorem fromTensor_toTensor [hqgt1 : Fact (q > 1)] (a : R q n) : R.fromTensor a.toTensor = a := by
+  cases h : Polynomial.degree (R.representative q n a) with
+    | none =>
+        have h' :=  Polynomial.degree_eq_bot.1 h
+        rw [← rep_zero] at h'
+        have h'':= (eq_iff_rep_eq _ _).1 h'
+        simp [R.fromTensor, R.toTensor, R.repLength]; rw [h, h'']
+        simp
+    | some deg =>
+        apply (eq_iff_coeff_eq _ _).2
+        have hCoeff := R.toTensor_getD' (q := q) (n := n)
+        unfold R.coeff at hCoeff
+        apply funext
+        intro i
+        rw [← hCoeff, ← hCoeff]
+        rw [toTensor_fromTensor]
+        rw[← ZMod.coe_int_cast]
+        norm_cast
+
+theorem fromTensor_toTensor' [hqgt1 : Fact (q > 1)] (a : R q n) : R.fromTensor a.toTensor' = a := by
+  rw [← R.fromTensor_eq_fromTensor_trimTensor, R.trim_toTensor'_eq_toTensor]
+  apply fromTensor_toTensor
+
+end Poly
diff --git a/lake-manifest.json b/lake-manifest.json
index 502a4a1f8..f017ded0a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -25,14 +25,6 @@
     "name": "partax",
     "inputRev?": "master",
     "inherited": false}},
-  {"git":
-   {"url": "https://github.com/leanprover/doc-gen4",
-    "subDir?": null,
-    "rev": "8bccb92b531248af1b6692d65486e8640c8bcd10",
-    "opts": {},
-    "name": "«doc-gen4»",
-    "inputRev?": "8bccb92b531248af1b6692d65486e8640c8bcd10",
-    "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
@@ -64,29 +56,5 @@
     "opts": {},
     "name": "proofwidgets",
     "inputRev?": "v0.0.19",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/xubaiw/CMark.lean",
-    "subDir?": null,
-    "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-    "opts": {},
-    "name": "CMark",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-    "subDir?": null,
-    "rev": "f09250282cea3ed8c010f430264d9e8e50d7bc32",
-    "opts": {},
-    "name": "«lean4-unicode-basic»",
-    "inputRev?": "main",
-    "inherited": true}},
-  {"git":
-   {"url": "https://github.com/hargonix/LeanInk",
-    "subDir?": null,
-    "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
-    "opts": {},
-    "name": "leanInk",
-    "inputRev?": "doc-gen",
     "inherited": true}}],
  "name": "SSA"}