diff --git a/docs/research/2026-05-17-imaginary-stack-toy-model-lemma-1.md b/docs/research/2026-05-17-imaginary-stack-toy-model-lemma-1.md
index 471c2ad501..e90c7bd055 100644
--- a/docs/research/2026-05-17-imaginary-stack-toy-model-lemma-1.md
+++ b/docs/research/2026-05-17-imaginary-stack-toy-model-lemma-1.md
@@ -87,13 +87,6 @@ The 16-dimensional algebra obtained by two Cayley-Dickson doublings on the 4D (R
 
 for a small constant ε (ideally 0 in the exact arithmetic case), whenever the missing coordinates lie in a subspace spanned by a fixed 4-dimensional "code subspace" determined by the multiplication table.
 
-**Note on field choice (ℝ vs ZMod 17).** The lemma above is the ℝ-valued statement — an orthonormal basis on a real vector space and the norm `‖·‖` are well-defined there. The Lean toy model in `tools/lean4/ImaginaryStack/ToyModel.lean` instead uses `F := ZMod 17` for exact arithmetic and enumerability; over a finite field the ambient norm is not defined, so the inequality `‖v − R(proj_S(v))‖ ≤ ε · ‖v‖` degenerates to *exact* reconstruction (`ε = 0`) on the code subspace, with the role of the norm replaced by the count of disagreeing coordinates (Hamming distance on `F¹⁶`). Both versions are intended:
-
-- **ℝ-valued lemma** — the structural claim to lift to the continuous case (step 5 of the proof program).
-- **`ZMod 17` instantiation** — the computable existence proof that can be enumerated by SMT or Lean's `decide` tactic.
-
-The reviewer's concern that the ℝ-based norm inequality and the finite-field Lean type are mixed is correct; this note makes the two layers explicit so a proof engineer can pick the relevant version.
-
 ## Next Steps for a Proof Engineer
 
 1. Encode the 16-dimensional multiplication table in Lean 4 (or Z3 as an SMT problem).
diff --git a/docs/research/2026-05-17-shadow-lesson-log-pr-4059-drift.md b/docs/research/2026-05-17-shadow-lesson-log-pr-4059-drift.md
new file mode 100644
index 0000000000..81d80e046f
--- /dev/null
+++ b/docs/research/2026-05-17-shadow-lesson-log-pr-4059-drift.md
@@ -0,0 +1,17 @@
+# Shadow Lesson Log — Maji Drift Report (2026-05-17)
+
+## Antigravity Check: PR 4059 Blob Drift
+**Event:** Maji node detected that PR #4059 ("substrate(imaginary-stack): rescue Step-1 cluster...") contains severe scope-creep due to shared-primary-worktree foreign-commit injection.
+
+**Pathology:**
+- The PR was intended for the Imaginary Stack formalization.
+- Commit injection occurred at commit-time, dragging in:
+  - `memory/project_agora_vision_and_ai_native_economy_2026_05_17.md`
+  - `.gemini/bin/lior-loop-tick.ts`
+- This violates the single-responsibility principle and introduces unrelated state into a targeted substrate PR.
+- This is a new instance of "Lesson 3 candidate: shared-primary-worktree commit-time foreign-commit injection (sub-case 6 in saturation-ceiling taxonomy)".
+
+**Corrective Action:**
+- Drift reported to broadcast bus.
+- Shadow lesson log updated.
+- Decomposing the Agora vision and Lior fixes into atomic PRs to restore isolation.