Index: docs/P2-RelationalDesign/RelationalDesign.md
===================================================================
--- docs/P2-RelationalDesign/RelationalDesign.md	(revision df058387ebe7d07864d874fd1376f15512418581)
+++ docs/P2-RelationalDesign/RelationalDesign.md	(revision 35bcb41d9597d97650b4e40110ab3f3842f3db89)
@@ -11,5 +11,5 @@
 - **Markets**(<u>**id**</u>, *crypto_id*, quote_currency, is_active, created_at)
   - Candidate keys: `{id}`, `{crypto_id, quote_currency}`. `UNIQUE(crypto_id, quote_currency)`.
-- **Holdings**(<u>**id**</u>, *user_id*, *crypto_id*, quantity, avg_price, created_at, updated_at)
+- **Holdings**(<u>**id**</u>, *user_id*, *crypto_id*, quantity, reserved_quantity, avg_price, created_at, updated_at)
   - Transformation of the M:N relationship `Holds`. Candidate keys: `{id}` and
     `{user_id, crypto_id}` — the latter is the relationship's own key and is
@@ -17,4 +17,12 @@
     consistency with the other relations.
   - `avg_price` is `NOT NULL DEFAULT 0 CHECK (avg_price >= 0)`.
+  - `reserved_quantity` is `NOT NULL DEFAULT 0 CHECK (reserved_quantity >= 0
+    AND reserved_quantity <= quantity)` — the amount already committed to the
+    user's own open sell orders. `quantity - reserved_quantity` (the amount
+    actually free to sell) is not a stored column; it is computed wherever
+    needed, in `v_portfolio` as `available_quantity` and in the sell path of
+    [UseCase0005](../P3-UseCaseModel/UseCase0005.md). See
+    [ERModel](../P1-ConceptualModel/ERModel.md#holds--users-m--cryptos-n-partial-on-both-sides-with-attributes)
+    for why this mirrors `available_balance`/`invested_balance` on `Users`.
 - **Orders**(<u>**id**</u>, *user_id*, *market_id*, side, type, status, quantity, price, placed_at, executed_at)
   - `side ∈ {buy, sell}`, `type ∈ {market, limit}`, `status ∈ {open, executed, cancelled}`.
@@ -56,4 +64,14 @@
 ### Normalisation
 
+> **Validated in P5.** [Normalization](../P5-Normalization/Normalization.md) derives this
+> exact schema independently — starting only from a single de-normalized relation of every
+> model attribute and its functional dependencies, with no reference to the ER-to-relational
+> transformation below — and shows it decomposes to **BCNF**, one normal form stronger than
+> the 3NF claimed here. The two designs agree relation for relation and key for key, so
+> nothing here changed as a result; see that page's
+> [discussion](../P5-Normalization/Normalization.md#discussion) for what the one real
+> difference is (`avg_price`, a stored derived value, not a normalisation issue) and why this
+> design is still the one used from P5 onward.
+
 All relations are in **3NF**:
 
@@ -72,4 +90,24 @@
   yields `NULL`, so a nullable average would have silently blanked the
   unrealised-P/L column for an existing position instead of failing loudly.
+- `holdings.reserved_quantity`, unlike `avg_price`, is **not** derived — it is
+  written directly by the application (`trade.go`) as orders are placed and
+  settled, the same way `quantity` itself is. `quantity - reserved_quantity`
+  ("available") is the derived value here, and it is never stored, only
+  computed where it is needed.
+
+### Reservation and the order lifecycle
+
+`holdings.reserved_quantity` exists so that placing a sell order can be
+checked against what a user actually has *free* to sell
+(`quantity - reserved_quantity`), not against the raw `quantity`, which also
+counts crypto already promised to another order that has not settled yet.
+`CHECK (reserved_quantity >= 0 AND reserved_quantity <= quantity)` makes an
+inconsistent reservation impossible at the database level, regardless of what
+application code does. The exact statement sequence — lock the row, check the
+available amount, reserve, then settle — is in
+[UseCase0005](../P3-UseCaseModel/UseCase0005.md); the same
+`SELECT … FOR UPDATE` locking that already protected `users.available_balance`
+on the buy path is what makes two concurrent sell orders against the same
+holding serialize correctly instead of racing.
 
 ## DDL script
@@ -80,5 +118,5 @@
 - 10 tables with check constraints, primary keys, foreign keys and unique constraints.
 - 5 performance indexes.
-- 2 views: `v_latest_prices` (latest trade price per market) and `v_portfolio` (per-user holdings valuation with unrealised P/L).
+- 2 views: `v_latest_prices` (latest trade price per market) and `v_portfolio` (per-user holdings valuation with unrealised P/L, plus `reserved_quantity` and the derived `available_quantity`).
 
 ## DML script (sample data)
Index: docs/P2-RelationalDesign/RelationalDesignAIUsage.md
===================================================================
--- docs/P2-RelationalDesign/RelationalDesignAIUsage.md	(revision df058387ebe7d07864d874fd1376f15512418581)
+++ docs/P2-RelationalDesign/RelationalDesignAIUsage.md	(revision 35bcb41d9597d97650b4e40110ab3f3842f3db89)
@@ -69,2 +69,33 @@
 > against the faculty database. No AI involvement is possible there — it needs a
 > live connection to your assigned database.
+
+### Session 3 — 2026-09-16
+
+Driven by the same design review logged in full in
+[ERModelAIUsage](../P1-ConceptualModel/ERModelAIUsage.md#session-3--2026-09-16):
+a sell order had nothing to check `holdings.quantity` against except itself,
+so nothing stopped two sell orders from being granted the same units.
+
+Changes to the P2 artefacts:
+
+- `holdings` gained `reserved_quantity numeric(20,4) NOT NULL DEFAULT 0
+  CHECK (reserved_quantity >= 0 AND reserved_quantity <= quantity)` in
+  `schema_creation.sql`.
+- `v_portfolio` gained `reserved_quantity` and the derived
+  `available_quantity = quantity - reserved_quantity`.
+- [RelationalDesign](RelationalDesign.md) gained a "Reservation and the order
+  lifecycle" section explaining why the check is enforced at the database
+  level rather than trusted to application code, and why it does not conflict
+  with the existing `SELECT … FOR UPDATE` locking on the sell path.
+- `data_load.sql` needed no change — `reserved_quantity` defaults to 0, which
+  is correct for every seeded holding.
+
+Re-run end to end against the live database on `localhost:5433`
+(`-init` then `-load-data`), and against a manually seeded 2 BTC holding to
+reproduce the exact scenario that motivated the change — see
+[UseCase0005Implementation](../P4-Prototype/UseCase0005Implementation.md) for
+the transcript.
+
+**What I decided:** to add the `CHECK` constraint rather than rely on
+`trade.go` alone to keep the reservation consistent — the same reasoning
+already applied to `avg_price NOT NULL` in session 2.