diff --git a/lean/Spa/Language/Semantics.lean b/lean/Spa/Language/Semantics.lean
index 2fa1234..0eedc50 100644
--- a/lean/Spa/Language/Semantics.lean
+++ b/lean/Spa/Language/Semantics.lean
@@ -2,12 +2,27 @@ import Spa.Language.Base
 import Spa.Lattice
 import Spa.Interp
 
+/-!
+
+# Operational Semantics
+
+This file contains the operational semantics for the object language defined in
+`Spa.Language.Base`. Right now, all values in the language are integers.
+The semantics are big-step, and lead to a fully constructed proof tree
+containing the derivation connecting the initial and final states.
+All pretty standard.
+
+-/
+
 namespace Spa
 
+/-- A value in the object language. Currently, the only possible case is
+    an integer. -/
 inductive Value where
   | int (z : ℤ)
   deriving DecidableEq
 
+/-- An environment mapping variables to their values. -/
 def Env : Type := List (String × Value)
 
 inductive Env.Mem : String × Value → Env → Prop
@@ -15,6 +30,8 @@ inductive Env.Mem : String × Value → Env → Prop
   | there (s s' : String) (v v' : Value) (ρ : Env) :
       ¬(s = s') → Env.Mem (s, v) ρ → Env.Mem (s, v) ((s', v') :: ρ)
 
+/-- Inference rules for evaluating an expression (`Spa.Expr`) in a given
+    environment. Pretty standard big-step expression evaluation. -/
 inductive EvalExpr : Env → Expr → Value → Prop
   | num (ρ : Env) (n : ℕ) : EvalExpr ρ (.num n) (.int n)
   | var (ρ : Env) (x : String) (v : Value) :
@@ -26,17 +43,24 @@ inductive EvalExpr : Env → Expr → Value → Prop
       EvalExpr ρ e₁ (.int z₁) → EvalExpr ρ e₂ (.int z₂) →
       EvalExpr ρ (.sub e₁ e₂) (.int (z₁ - z₂))
 
+/-- Inference rules for evaluating a basic statement (`Spa.BasicStmt`) in
+    a given environment, potentially changing the environment.
+    Pretty standard big-step evaluation. -/
 inductive EvalBasicStmt : Env → BasicStmt → Env → Prop
   | noop (ρ : Env) : EvalBasicStmt ρ .noop ρ
   | assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
       EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)
 
+/-- Inference rules for evaluating a sequence of basic statements. -/
 inductive EvalBasicStmts : Env → List BasicStmt → Env → Prop
   | nil {ρ : Env} : EvalBasicStmts ρ [] ρ
   | cons {ρ₁ ρ₂ ρ₃ : Env} {bs : BasicStmt} {bss : List BasicStmt} :
       EvalBasicStmt ρ₁ bs ρ₂ → EvalBasicStmts ρ₂ bss ρ₃ →
       EvalBasicStmts ρ₁ (bs :: bss) ρ₃
 
+/-- Inference rules for evaluating statements (`Spa.Stmt`) in a given
+    environment, potentially changing the environment.
+    Pretty standard big-step evaluation. -/
 inductive EvalStmt : Env → Stmt → Env → Prop
   | basic (ρ₁ ρ₂ : Env) (bs : BasicStmt) :
       EvalBasicStmt ρ₁ bs ρ₂ → EvalStmt ρ₁ (.basic bs) ρ₂
@@ -57,6 +81,15 @@ inductive EvalStmt : Env → Stmt → Env → Prop
       EvalExpr ρ e (.int 0) →
       EvalStmt ρ (.whileLoop e s) ρ
 
+/-- For the purpose of static analysis, lattices we define describe program
+    state, or better yet, they describe _values_ in the program.
+    This class should be provided by each analysis' lattice (see also `Spa/Analysis/Forward.lean`)
+    to describe what each lattice value means in terms of the language.
+
+    In addition to providing the interpretation (`Spa.Interp`), the lattice
+    combinators `⊔` and `⊓` must respect disjunction and conjunction respectively.
+    This is because possible paths through a control flow graph (`Spa/Language/Graphs.lean`),
+    are tied to lattice operations used by the analysis engine. -/
 class LatticeInterpretation (L : Type*) [Lattice L] extends Interp L (Value → Prop) where
   interp_sup : ∀ {l₁ l₂ : L} (v : Value),
     interp l₁ v ∨ interp l₂ v → interp (l₁ ⊔ l₂) v
diff --git a/lean/Spa/Lattice/Prod.lean b/lean/Spa/Lattice/Prod.lean
index ca382fd..0898163 100644
--- a/lean/Spa/Lattice/Prod.lean
+++ b/lean/Spa/Lattice/Prod.lean
@@ -1,11 +1,46 @@
 import Spa.Lattice
 
+/-!
+
+# Product Lattice
+
+This file provides a proof that, in addition to being a lattice,
+the product of two types $\alpha \times \beta$ forms a `Spa.FiniteHeightLattice`
+if both $\alpha$ and $\beta$ have a finite height.
+
+The proof proceeds by "unzipping" a chain:
+
+$$
+(a_1, b_1) < (a_1, b_2) < \ldots < (a_n, b_m)
+$$
+
+In which, at each step, either an $\alpha$ or $\beta$ element
+might ratchet up, into two chains:
+
+$$
+\begin{aligned}
+a_1 < \ldots < a_n \\
+b_1 < \ldots < b_m
+\end{aligned}
+$$
+
+Because at least one of the two "unzipped" chains grows with
+each element of the product chain, the full chain length
+can't exceed the sum of the two components. By the definition
+of finite height, these two chains are bounded, and therefore,
+the product chain is bounded too.
+
+-/
+
 namespace Spa
 
 section Unzip
 
 variable {α β : Type*} [PartialOrder α] [PartialOrder β]
 
+/-- The unzipping lemma: any chain (`LTSeries`) of product
+    elements can be decomposed into chains of components,
+    whose lengths bound the chain. -/
 lemma LTSeries.exists_unzip (c : LTSeries (α × β)) :
     ∃ (c₁ : LTSeries α) (c₂ : LTSeries β),
       c₁.head = c.head.1 ∧ c₁.last = c.last.1 ∧
@@ -60,6 +95,9 @@ section FixedHeight
 
 variable {α β : Type*}
 
+/-- The longest possible chain is one in which only one of the components grows
+    at a time, making the maximum height of $\alpha \times \beta$ be
+    $\text{height}_\alpha + \text{height}_\beta$. -/
 instance prod [A : FiniteHeightLattice α] [B : FiniteHeightLattice β] :
     FiniteHeightLattice (α × β) where
   toLattice := inferInstance
diff --git a/lean/Spa/Lattice/Unit.lean b/lean/Spa/Lattice/Unit.lean
index f63c415..2e20475 100644
--- a/lean/Spa/Lattice/Unit.lean
+++ b/lean/Spa/Lattice/Unit.lean
@@ -1,7 +1,18 @@
 import Spa.Lattice
 
+/-!
+
+# Unit Lattice
+
+This file provides a proof that in addition to being a lattice,
+`PUnit` is a `Spa.FiniteHeightLattice`. This is fairly trivial result,
+but the unit is used as a placeholder in various contexts (e.g.,
+as a base case for the iterated product `Spa/Lattice/IterProd.lean`). -/
+
 namespace Spa
 
+/-- Since a singleton type's preorder has no nonempty `<` chains,
+    they are vacuously bounded by any minimum height. -/
 lemma boundedChains_of_subsingleton (α : Type*) [Preorder α] [Subsingleton α]
     (n : ℕ) : BoundedChains α n := fun c => by
   by_contra hc