diff --git a/PhD.lean b/PhD.lean
index 4e56ad9..c60e64d 100644
--- a/PhD.lean
+++ b/PhD.lean
@@ -1 +1 @@
-import PhD.Example
+import PhD.RPS.def
diff --git a/PhD/Example.lean b/PhD/Example.lean
deleted file mode 100644
index 5dd5b12..0000000
--- a/PhD/Example.lean
+++ /dev/null
@@ -1,4 +0,0 @@
-import Mathlib
-
-def foo (a b : ℚ) : a + b = b + a := by
-  ring
diff --git a/PhD/RPS/def.lean b/PhD/RPS/def.lean
new file mode 100644
index 0000000..4ea9dfa
--- /dev/null
+++ b/PhD/RPS/def.lean
@@ -0,0 +1,181 @@
+/-
+Copyright (c) 2025 William Coram. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: William Coram
+-/
+
+import Mathlib.Algebra.Group.NatPowAssoc
+import Mathlib.Analysis.Normed.Group.Ultra
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.RingTheory.PowerSeries.Basic
+
+/-!
+# Restricted power series
+
+We say a powerseries over a normed ring `R` is restricted for a parameter `c` if
+`‖coeff R i f‖ * c^i → 0`.
+
+## Main results
+
+- `IsGroup`: for a normed ring `R` the set of restricted power series forms an additive group.
+- `IsRing`: if `R` is a normed ring with the ultrametric property then the set of restricted
+  power series forms a ring.
+
+-/
+
+namespace PowerSeries
+
+open PowerSeries Filter
+open scoped Topology
+
+/-- A power series over `R` is restricted of paramerter `c` if we have the following limit. -/
+def IsRestricted (R : Type*) [NormedRing R] (f : PowerSeries R) (c : ℝ) :=
+  Tendsto (fun (i : ℕ) => (norm (coeff R i f)) * c^i) atTop (𝓝 0)
+
+namespace Restricted
+
+variable (R : Type*) [NormedRing R] (c : ℝ)
+
+lemma Equiv_cToAbs (f : PowerSeries R) : IsRestricted R f c ↔ IsRestricted R f |c| := by
+  simp_rw [IsRestricted, NormedAddCommGroup.tendsto_atTop, sub_zero, norm_mul, norm_norm, norm_pow,
+    Real.norm_eq_abs, abs_abs]
+
+/-- The set of restricted power series over `R` for a parameter `c`. -/
+def SetOf : Set (PowerSeries R) :=
+  {f : PowerSeries R | IsRestricted R f c}
+
+lemma zero : IsRestricted R 0 c := by
+  simp_rw [IsRestricted, map_zero, norm_zero, zero_mul, tendsto_const_nhds_iff]
+
+lemma one : IsRestricted R 1 c := by
+  simp_rw [IsRestricted, coeff_one, NormedAddCommGroup.tendsto_atTop, sub_zero, norm_mul, norm_norm,
+    norm_pow, Real.norm_eq_abs]
+  intro ε hε
+  refine ⟨1, fun n hn => ?_ ⟩
+  simpa only [Nat.ne_zero_of_lt hn, ↓reduceIte, norm_zero, zero_mul] using hε
+
+lemma add {f g : PowerSeries R} (hf : IsRestricted R f c) (hg : IsRestricted R g c) :
+    IsRestricted R (f + g) c := by
+  simp only [IsRestricted, map_add, NormedAddCommGroup.tendsto_atTop] at hf hg ⊢
+  intro ε hε
+  obtain ⟨fN, hfN⟩ := hf (ε/2) (half_pos hε)
+  obtain ⟨gN, hgN⟩ := hg (ε/2) (half_pos hε)
+  simp only [sub_zero, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at hfN hgN
+  refine ⟨max fN gN, fun n hn => ?_ ⟩
+  simp only [sub_zero, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm]
+  exact lt_of_le_of_lt  (by simpa only [right_distrib] using (mul_le_mul_of_nonneg_right
+    (norm_add_le (coeff R n f) (coeff R n g)) (pow_nonneg (abs_nonneg c) n)))
+    (by simpa only [add_halves] using (add_lt_add (hfN n (le_of_max_le_left hn))
+    (hgN n (le_of_max_le_right hn))))
+
+lemma neg {f : PowerSeries R} (hf : IsRestricted R f c) : IsRestricted R (-f) c := by
+  simpa only [IsRestricted, map_neg, norm_neg] using hf
+
+/-- The set of restricted power series over `R` for a parameter `c` forms an additive subgroup of
+    power series over `R`. -/
+def addsubgroup : AddSubgroup (PowerSeries R) where
+  carrier := (SetOf R c)
+  zero_mem' := zero R c
+  add_mem' := add R c
+  neg_mem' := neg R c
+
+/-- The restricted power series over a normed ring `R` for a parameter `c ∈ ℝ` forms an additive
+    group. -/
+instance IsGroup : AddGroup (SetOf R c) :=
+  AddSubgroup.toAddGroup (addsubgroup R c)
+
+/-- The set of `‖coeff R i f‖ * c^i` for a given power series `f` and parameter `c`. -/
+def convergenceSet (f : PowerSeries R) : Set ℝ :=
+  {‖coeff R i f‖ * c^i | i : ℕ}
+
+lemma BddAbove {f : PowerSeries R} (hf : IsRestricted R f c) : BddAbove (convergenceSet R c f) := by
+  simp_rw [IsRestricted, NormedAddCommGroup.tendsto_atTop] at hf
+  obtain ⟨N, hf⟩ := by simpa only [zero_lt_one, sub_zero, norm_mul, norm_norm, norm_pow,
+    Real.norm_eq_abs, forall_const, abs_norm] using (hf 1)
+  simp_rw [bddAbove_def, convergenceSet]
+  use max 1 (Finset.max' (Finset.image (fun i => ‖coeff R i f‖ * c^i) (Finset.range (N+1)))
+    (by simp only [Finset.image_nonempty, Finset.nonempty_range_iff, ne_eq,
+    AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false,
+    not_false_eq_true]))
+  simp only [Set.mem_setOf_eq, le_sup_iff, forall_exists_index, forall_apply_eq_imp_iff]
+  intro i
+  rcases (Nat.le_total i N) with h | h
+  · right
+    apply Finset.le_max'
+    simp only [Finset.mem_image, Finset.mem_range]
+    exact ⟨i, by exact Order.lt_add_one_iff.mpr h, rfl⟩
+  · exact Or.inl (le_of_lt (lt_of_le_of_lt (mul_le_mul_of_nonneg_left
+      (by simpa only [abs_pow] using le_abs_self (c ^ i)) (norm_nonneg _)) (hf i h)))
+
+lemma BddAbove_nneg {f : PowerSeries R} (hf : IsRestricted R f c) :
+     ∃ A, A > 0 ∧ ∀ i, ‖coeff R i f‖ * c^i ≤ A := by
+  obtain ⟨n, hn⟩ := by simpa only [bddAbove_def] using (BddAbove R c hf)
+  simp_rw [convergenceSet, Set.mem_setOf_eq, forall_exists_index, forall_apply_eq_imp_iff] at hn
+  rcases (eq_zero_or_neZero n) with h | h
+  · refine ⟨n + 1, ⟨by simp_rw [h, zero_add, gt_iff_lt, zero_lt_one], fun i => le_trans (hn i)
+    (by simp_rw [h, zero_add, zero_le_one])⟩⟩
+  · exact ⟨|n|, by simpa only [gt_iff_lt, abs_pos] using Ne.symm (NeZero.ne' n),
+    fun i => le_trans (hn i) (le_abs_self n)⟩
+
+variable [IsUltrametricDist R]
+
+open IsUltrametricDist
+
+lemma mul {f g : PowerSeries R} (hf : IsRestricted R f c) (hg : IsRestricted R g c) :
+    IsRestricted R (f * g) c := by
+  simp_rw [IsRestricted] at hf hg ⊢
+  obtain ⟨a, ha, fBound1⟩ := BddAbove_nneg R |c| ((Equiv_cToAbs R c f).mp hf)
+  obtain ⟨b, hb, gBound1⟩ := BddAbove_nneg R |c| ((Equiv_cToAbs R c g).mp hg)
+  rw [NormedAddCommGroup.tendsto_atTop] at hf hg ⊢
+  intro ε hε
+  simp only [sub_zero, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at hf hg ⊢
+  simp_rw [PowerSeries.coeff_mul]
+  obtain ⟨Nf, fBound2⟩ := (hf (ε/ (max a b))) (div_pos hε (lt_sup_of_lt_left ha))
+  obtain ⟨Ng, gBound2⟩ := (hg (ε/ (max a b))) (div_pos hε (lt_sup_of_lt_left ha))
+  refine ⟨2 * max Nf Ng,  fun n hn => ?_⟩
+  obtain ⟨i, hi, ultrametric⟩ := exists_norm_finset_sum_le (Finset.antidiagonal n)
+    (fun a => (coeff R a.1) f * (coeff R a.2) g)
+  have hi := by simpa only [Finset.mem_antidiagonal] using hi (⟨(0,n), by simp only
+    [Finset.mem_antidiagonal, zero_add]⟩)
+  have InterimBound1 := mul_le_mul_of_nonneg_right ultrametric (pow_nonneg (abs_nonneg c) n)
+  have InterimBound2 := mul_le_mul_of_nonneg_right
+    (NormedRing.norm_mul_le ((coeff R i.1) f) ((coeff R i.2) g)) (pow_nonneg (abs_nonneg c) n)
+  have : ‖(coeff R i.1) f‖ * ‖(coeff R i.2) g‖ * |c|^n =
+      ‖(coeff R i.1) f‖ * |c|^i.1 * (‖(coeff R i.2) g‖ * |c|^i.2) := by
+    ring_nf
+    simp_rw [mul_assoc, ← npow_add, hi]
+  simp only [this] at InterimBound2
+  have : i.1 ≥ max Nf Ng ∨ i.2 ≥ max Nf Ng := by
+    omega
+  rcases this with this | this
+  · have FinalBound := mul_lt_mul_of_lt_of_le_of_nonneg_of_pos ((fBound2 i.1)
+      (le_of_max_le_left this)) (gBound1 i.2) (Left.mul_nonneg (norm_nonneg ((coeff R i.1) f))
+      (pow_nonneg (abs_nonneg c) i.1)) hb
+    exact lt_of_lt_of_le (lt_of_le_of_lt (le_trans InterimBound1 InterimBound2) FinalBound)
+      (by simpa only [div_mul_comm] using ((mul_le_iff_le_one_left hε).mpr
+      ((div_le_one₀ (lt_sup_of_lt_left ha)).mpr (le_max_right a b))))
+  · have FinalBound := mul_lt_mul_of_le_of_lt_of_nonneg_of_pos (fBound1 i.1) ((gBound2 i.2)
+      (le_of_max_le_right this)) (Left.mul_nonneg (norm_nonneg ((coeff R i.2) g))
+      (pow_nonneg (abs_nonneg c) i.2)) ha
+    exact lt_of_lt_of_le (lt_of_le_of_lt (le_trans InterimBound1 InterimBound2) FinalBound)
+      (by simpa only [mul_div_left_comm] using ((mul_le_iff_le_one_right hε).mpr
+      ((div_le_one₀ (lt_sup_of_lt_left ha)).mpr (le_max_left a b))))
+
+/-- The set of restricted power series over `R` for a parameter `c` are a subring of power series
+    over `R`. -/
+def subring : Subring (PowerSeries R) where
+  carrier := SetOf R c
+  zero_mem' := zero R c
+  add_mem' := add R c
+  neg_mem' := neg R c
+  one_mem' := one R c
+  mul_mem' := mul R c
+
+/-- The restricted power series over a normed ring `R` with the ultrametric property forms a
+    ring. -/
+noncomputable
+instance IsRing : Ring (SetOf R c) :=
+    Subring.toRing (subring R c)
+
+end Restricted
+end PowerSeries
diff --git a/README.md b/README.md
index 08f426d..1327c41 100644
--- a/README.md
+++ b/README.md
@@ -1,198 +1,3 @@
-# Lean 4 Project Template
+Ongoing PhD project to formalise quaternionic modular forms and results on the slopes of compact Hecke operator.
 
-[![License: Apache 2.0](https://img.shields.io/badge/License-Apache_2.0-lightblue.svg)](https://opensource.org/licenses/Apache-2.0)
-[![Zulip : Topic](https://img.shields.io/badge/Zulip-Topic-%237E57C2.svg?logo=zulip&logoColor=white)](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Tutorial.3A.20Getting.20Started.20with.20Blueprint-Driven.20Projects)
-[![YouTube : Tutorial](https://img.shields.io/badge/YouTube-Tutorial-%23FF0000.svg?logo=youtube&logoColor=white)](https://youtu.be/KyuyTsLgkMY)
-
-This repository contains a template for blueprint-driven formalization projects in Lean 4.
-
-## Install Lean 4
-
-Ensure that you have a functioning Lean 4 installation. If you do not, please follow
-the [Lean installation guide](https://leanprover-community.github.io/get_started.html).
-
-## Use this Template
-
-To create a new repository using this template, ensure you are on the correct repository page
-([LeanProject](https://github.com/pitmonticone/LeanProject)) and then follow these steps:
-
-1. Click the **Use this template** button located at the top right of the repository page.
-2. Click the **Create a new repository** button.
-3. Select the account or organization where you want to create it, choose a name for the new
-repository, and click the **Create repository** button.
-
-## Clone this Repository
-
-To clone this repository to your local machine, please refer to the relevant section of the
-GitHub documentation [here](https://docs.github.com/en/repositories/creating-and-managing-repositories/cloning-a-repository).
-
-## Customize this Template
-
-To tailor this template to your specific project, follow these steps:
-
-1. If you don't have a Python environment, you can install one by following the instructions in the
-[Python installation guide](https://www.python.org/downloads/).
-1. Verify your Python installation by running:
-    ```bash
-    python3 --version
-    ```
-1. Verify your Pip installation by running:
-    ```bash
-    pip3 --version
-    ```
-1. Ensure your terminal is in the project directory by running the following command:
-    ```bash
-    cd path/to/your/project
-    ```
-1.	Execute the customization script by running:
-    ```bash
-    scripts/customize_template.py NewProject
-    ```
-    where `NewProject` must be replaced by the name of your project.
-
-The script [`customize_template.py`](scripts/customize_template.py) will automatically rename the
-project folder and update the necessary files and configurations to match the new project name.
-
-## Configure GitHub Pages
-
-To set up GitHub Pages for your repository, follow these steps:
-
-1. Go to the **Settings** tab of your repository.
-2. In the left sidebar, click on the **Pages** section.
-3. In the **Source** dropdown, select `GitHub Actions`.
-
-## Repository Layout
-
-The template repository is organized as follows (listing the main folders and files):
-
-- [`.github`](.github) contains GitHub-specific configuration files and workflows.
-    - [`workflows`](.github/workflows) contains GitHub Actions workflow files.
-        - [`build-project.yml`](.github/workflows/build-project.yml) defines the workflow for building
-        the Lean project on pushes, pull requests, and manual triggers. This is a minimalistic build
-        workflow which is not necessary if you decide to generate a blueprint (see instructions below)
-        and can be manually disabled by clicking on the **Actions** tab, selecting **Build Project**
-        in the left sidebar, then clicking the horizontal triple dots (⋯) on the right,
-        and choosing **Disable workflow**.
-        - [`create-release.yml`](.github/workflows/create-release.yml): defines the workflow for creating a new Git tag and GitHub release when the `lean-toolchain` file is updated in the `main` branch. Ensure the following settings are configured under **Settings > Actions > General > Workflow permissions**: "Read and write permissions" and "Allow GitHub Actions to create and approve pull requests".
-        - [`update.yml`](.github/workflows/update.yml) is the dependency
-        update workflow to be triggered manually by default. [It's not documented yet, but it will be soon.]
-    - [`dependabot.yml`](.github/dependabot.yml) is the configuration file to automate CI dependency updates.
-- [`.vscode`](.vscode) contains Visual Studio Code configuration files
-    - [`extensions.json`](.vscode/extensions.json) recommends VS Code extensions for the project.
-    - [`settings.json`](.vscode/settings.json) defines the project-specific settings for VS Code.
-- [`Project`](Project) should contain the Lean code files.
-    - [`Mathlib`](Project/Mathlib) should contain `.lean` files with declarations missing from the
-    current version of Mathlib.
-    - [`Example.lean`](Project/Example.lean) is a sample Lean file.
-- [`scripts`](scripts) contains scripts to update Mathlib ensuring that the latest version is
-fetched and integrated into the development environment.
-- [`.gitignore`](.gitignore) specifies files and folders to be ignored by Git.
-and environment.
-- [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md) should contain the code of conduct for the project.
-- [`CONTRIBUTING.md`](CONTRIBUTING.md) should provide the guidelines for contributing to the
-project.
-- [`lakefile.toml`](lakefile.toml) is the configuration file for the Lake build system used in
-Lean projects.
-- [`lean-toolchain`](lean-toolchain) specifies the Lean version and toolchain used for the project.
-
-## Blueprint
-
-### 0. Selected Collaborative Projects
-
-- [Fermat's Last Theorem for Exponent 3](https://pitmonticone.github.io/FLT3/) by Riccardo Brasca et al.
-- [Polynomial Freiman-Ruzsa Conjecture](https://github.com/teorth/pfr) by Terence Tao et al.
-- [Fermat's Last Theorem](https://imperialcollegelondon.github.io/FLT/) by Kevin Buzzard et al.
-- [Carleson Operators on Doubling Metric Measure Spaces](http://florisvandoorn.com/carleson/) by Floris van Doorn et al.
-- [Bonn Collaborative Formalization Seminar Series in Analysis](https://github.com/fpvandoorn/BonnAnalysis) by Floris van Doorn et al.
-- [Prime Number Theorem and More](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd) by Alex Kontorovich et al.
-- [Infinity Cosmos](https://github.com/emilyriehl/infinity-cosmos) by Emily Riehl et al.
-- [Analytic Number Theory Exponent Database](https://github.com/teorth/expdb) by Terence Tao et al.
-- [Groupoid Model of Homotopy Type Theory](https://github.com/sinhp/GroupoidModelofHoTTinLean4) by Sina Hazratpour et al.
-- [Equational Theories](https://github.com/teorth/equational_theories) by Terence Tao et al.
-
-For more examples of completed and ongoing Lean projects and libraries, please
-see the [Lean Reservoir](https://reservoir.lean-lang.org).
-
-### 1. Install Dependencies
-
-To install the necessary dependencies, follow the instructions in the
-[PyGraphViz installation guide](https://pygraphviz.github.io/documentation/stable/install.html).
-
-### 2. Install LeanBlueprint Package
-
-Assuming you have a properly configured Python environment, install LeanBlueprint by running:
-
-```bash
-pip install leanblueprint
-```
-
-If you have an existing installation of LeanBlueprint, you can upgrade to the latest version by
-running:
-
-```bash
-pip install -U leanblueprint
-```
-
-### 3. Configure Blueprint
-
-To set up the blueprint for your project, run:
-
-```bash
-leanblueprint new
-```
-
-Then, follow the prompts and answer the questions as you like, except for a few specific
-questions which should be answered as indicated below to ensure compatibility with this template.
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Proceed with blueprint creation? [y/n]
-```
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Modify lakefile and lake-manifest to allow checking declarations exist? [y/n] (y)
-```
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Modify lakefile and lake-manifest to allow building the documentation? [y/n] (y):
-```
-
-If you want to generate a Jekyll-based home page for the project, respond
-affirmatively with `y` to the following prompt:
-
-```console
-Do you want to create a home page for the project, with links to the blueprint, the API documentation and the repository? [y/n]:
-```
-
-Respond affirmatively with `y` to the following prompt:
-
-```console
-Configure continuous integration to compile blueprint? [y/n] (y):
-```
-
-For more details about the LeanBlueprint package and its commands, please refer to its
-[documentation](https://github.com/PatrickMassot/leanblueprint/tree/master#starting-a-blueprint).
-
-After configuring the blueprint, please wait for the GitHub Action workflow to finish.
-You can keep track of the progress in the **Actions** tab of your repository.
-
-## Selected Projects Using this Template
-
-If you have used this template to create your own Lean project and would like to share it with the community, please consider opening a [PR](https://github.com/pitmonticone/LeanProject/pulls) to add your project to this list:
-
-- [Infinity Cosmos](https://github.com/emilyriehl/infinity-cosmos) by Emily Riehl et al.
-- [Analytic Number Theory Exponent Database](https://github.com/teorth/expdb) by Terence Tao et al.
-- [Equational Theories](https://github.com/teorth/equational_theories) by Terence Tao et al.
-- [Groupoid Model of Homotopy Type Theory](https://github.com/sinhp/GroupoidModelofHoTTinLean4) by Sina Hazratpour et al.
-- [Soundness of FRI](https://github.com/BoltonBailey/FRISoundness) by Bolton Bailey et al.
-- [Weil's Converse Theorem](https://github.com/CBirkbeck/WeilConverse) by Chris Birkbeck et al.
-- [Proofs from THE BOOK](https://github.com/mo271/FormalBook) by Moritz Firsching et al.
-- [Automata Theory](https://github.com/shetzl/autth) by Stefan Hetzl et al.
-- [Dirichlet Nonvanishing](https://github.com/CBirkbeck/DirichletNonvanishing) by Chris Birkbeck et al.
-- [Seymour's Decomposition Theorem](https://github.com/Ivan-Sergeyev/seymour) by Ivan Sergeyev et al.
-- [Spectral Theorem](https://github.com/oliver-butterley/SpectralThm) by Oliver Butterley and Yoh Tanimoto.
+More information and progress can be found in the [blueprint](https://williamcoram.github.io/PhD/blueprint/sect0001.html).
diff --git a/blueprint/src/chapter/GaussNorm.tex b/blueprint/src/chapter/GaussNorm.tex
new file mode 100644
index 0000000..339a4d7
--- /dev/null
+++ b/blueprint/src/chapter/GaussNorm.tex
@@ -0,0 +1,19 @@
+\chapter{Gauss Norm}
+
+Thus far we have shown restricted power series over a non-archimedean normed ring $R$ for a
+parameter $c$ forms a ring. Let us denote this ring by $\mathcal{F}$. Next, let us consider the
+following function $| \cdot |_c :  \mathcal{F} \to \R$ with $f = \sum a_n x^n$
+\[
+    |f|_c = \sup_{i \in \N} |a_n|c^n
+\]
+
+\begin{lemma}
+  The pair $(\mathcal{F}, | \cdot |_c)$ is a non-archimedean normed ring.
+\end{lemma}
+
+Moreover, if we restrict ourselves to polynomials we can strenghten this.
+
+\begin{lemma}
+  The pair $(R[x], | \cdot |_c)$ is a non-archimedean valued ring. That is, $| \cdot |_c$ is an
+  absolute value.
+\end{lemma}
diff --git a/blueprint/src/chapter/Intro.tex b/blueprint/src/chapter/Intro.tex
index 16f94dd..ae3b21d 100644
--- a/blueprint/src/chapter/Intro.tex
+++ b/blueprint/src/chapter/Intro.tex
@@ -1,7 +1,39 @@
 \chapter{Introduction}
 
-This page consists of the outline for my PhD project. Ultimately, the goal is to formalise results
-on $p$-adic modular forms - however there will be a lot of foundational work required to get to this
-point.
+Jacquet-Langlands suggests that certain classical modular forms should be related to modular forms
+on quaternion algebras. This is because classical modular forms can be viewed as automorphic forms
+for $M_2 (\Q)$; which is also a quaternion algebra. Compared to the analytic defintion of classical
+modular forms, for definite quaternion algebras, the definition of quaternionic modular forms is
+much nicer to work with - specifically, being of a concrete combinatorial nature. Thus, to study
+(some) classical modular forms, it may be easier to study quaternionic modular forms.
 
-Right now the goal is to formalise Daniel Jacobs thesis "slopes of compact Hecke operators".
+In this project the aim is to define such quaternionic modular forms over definite quaternion
+algebras and then prove some results surrounding them in Lean. Specifcally, we aim to formalise
+Daniel Jacobs' thesis "slopes of compact Hecke operators", which says that $p$-adic valuations of the
+eigenvalues of certain Hecke operators over quaternionic modular forms are in arithmetic
+progression.
+
+\subsection{What is being formalised?}
+
+In attempting to formalise Daniel Jacobs' theis paper we need to first build up foundation material
+before we can start working on his paper. This includes:
+
+\begin{enumerate}
+  \item restricted power series;
+  \item the Gauss norm; and
+  \item Newton polygons.
+\end{enumerate}
+
+Each of these can be found in its own chapter of the blueprint. Where we introduce the topic and
+state what we need in Lean. This is by no means the entirity of the field, but should be sufficient
+for what we need.
+
+After what we are dubbing the foundational material, we need to start working on results on
+quaternionic modular forms. This includes:
+\begin{enumerate}
+  \item their definition;
+  \item a result on their finite dimensionality (Fujisaki's lemma); and
+  \item their Hecke operators.
+\end{enumerate}
+
+Finally, with this we can hopefully start formalising the results from Jacobs' thesis.
diff --git a/blueprint/src/chapter/NewtonPolygons.tex b/blueprint/src/chapter/NewtonPolygons.tex
index e834f07..a0f1733 100644
--- a/blueprint/src/chapter/NewtonPolygons.tex
+++ b/blueprint/src/chapter/NewtonPolygons.tex
@@ -3,7 +3,7 @@ \chapter{Newton Polygons}
 In this section we will determine a way to check for zeroes of a power series via constructing
 something called a Newton polygon. We will follow \cite[Section~7.4]{Gouvea} closely.
 
-\subsection{Polynomials}
+\section{Polynomials}
 
 Suppose $p$ is a prime number and consider $K = \Q_p$. We can generalise everything here to
 discretely valued fields, but for notation it is enough to consider $\Q_p$.
@@ -80,7 +80,7 @@ \subsection{Polynomials}
 Therefore, by computing the Newton polygon of a polynomial we can get information about the
 valuations of its roots.
 
-\subsection{Power series}
+\section{Power series}
 
 Thus far we have worked with Newton polygons of polynomials, however we will eventually want to
 know properties of roots of power series. Therefore, we would like to generalise all the work we
@@ -146,7 +146,7 @@ \subsection{Power series}
     in the closed ball of radius $p^m.$
 \end{corollary}
 
-\subsection{Weierstrass preparation theorem}
+\section{Weierstrass preparation theorem}
 
 This section will be dedicated to proving proposition~\ref{NP}.
 
diff --git a/blueprint/src/chapter/QMF.tex b/blueprint/src/chapter/QMF.tex
index 0e08e97..ecf3462 100644
--- a/blueprint/src/chapter/QMF.tex
+++ b/blueprint/src/chapter/QMF.tex
@@ -2,7 +2,8 @@ \chapter{Quaternionic Modular Forms}
 
 \section{Definition}
 
-We define quaternionic modular forms explicitely as the following space.
+We define quaternionic modular forms over definite quaternion algebras explicitely as the following
+space.
 
 \begin{definition}
   Let $\kappa : \mathbb{Z}_p^\times \to \mathcal{O}_p^\times$ be a locally analytic character.
diff --git a/blueprint/src/chapter/RPS.tex b/blueprint/src/chapter/RPS.tex
index 958b5ff..eae0337 100644
--- a/blueprint/src/chapter/RPS.tex
+++ b/blueprint/src/chapter/RPS.tex
@@ -1,6 +1,6 @@
 \chapter{Restricted Power Series}
 
-Recall formal power series over a set $K$ in one variable, written $K \llbracket x \rrbracket $, are
+Recall formal power series over a set $K$ in one variable, written $K [ \! [ x ] \! ] $, are
 infinite sums
 \[
 f(x) = \sum_{n=0}^\infty a_n x^n, \quad \forall i, \; a_i \in K.
@@ -16,15 +16,17 @@ \chapter{Restricted Power Series}
 refer to them as the ring of power series over $K$.
 
 We want to introduce a convergence property on the terms $a_n x^n$, to do this we need a norm.
+Towards this we recall the definition of a normed ring: we say a ring $R$ is a normed ring if we can
+equip it with a norm.
 
-\begin{definition}
-    We say a ring $R$ is a normed ring if we can equip it with a norm.
-\end{definition}
 
 We now restrict ourselves to normed rings $R$ and define a subset of power series with a convergence
 property.
 
 \begin{definition}
+    \label{PowerSeries.IsRestricted}
+    \lean{PowerSeries.IsRestricted}
+    \leanok
     Let $f$ be a power series over $R$ in one variable, write $f = \sum_{n=0}^\infty a_n x^n$, and
     let $c$ be a real number. We say $f$ is a restricted power series of parameter $c$ over $K$ if
     \[
@@ -41,8 +43,6 @@ \chapter{Restricted Power Series}
 of the norm on $K$, but a stronger bound than the triangle inequality is necessary for the
 multiplication to be closed. This can be seen by the following example:
 
-\begin{example}
-
 Let $f = \sum_{n=0}^\infty \frac{(-1)^n}{\sqrt{n+1}}x^n$ be a power series over $\mathbb{R}$
 equipped with the standard norm. Then it is trivial to see that $f$ is a restricted power series for
 the parameter 1. However, the product $f^2$ has coefficients
@@ -57,16 +57,28 @@ \chapter{Restricted Power Series}
 that is $f^2$ is not a restricted power series for parameter 1, and we see multiplication is not
 closed.
 
-\end{example}
-
 \begin{theorem}
+  \label{PowerSeries.Restricted.IsGroup}
+  \lean{PowerSeries.Restricted.IsGroup}
+  \leanok
   Restricted power series over a normed ring $R$ form an additive group.
 \end{theorem}
 
+\begin{proof}
+  \leanok
+\end{proof}
+
 \begin{theorem}
+  \label{PowerSeries.Restricted.IsRing}
+  \lean{PowerSeries.Restricted.IsRing}
+  \leanok
   Restricted power series over a non-archimedean normed ring $R$ form a ring.
 \end{theorem}
 
+\begin{proof}
+  \leanok
+\end{proof}
+
 We now suppose that $K$ is a non-archimedean complete field; that is a field equipped with a metric
 that is complete and whose metric has the non-archimedean property as defined earlier, like $\Q_p$.
 
diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex
index 13e94a6..055705d 100644
--- a/blueprint/src/content.tex
+++ b/blueprint/src/content.tex
@@ -1,6 +1,7 @@
 
 \input{chapter/Intro}
 \input{chapter/RPS}
+\input{chapter/GaussNorm}
 \input{chapter/NewtonPolygons}
 \input{chapter/Fujisaki}
 \input{chapter/QMF}