diff --git a/docs/design.md b/docs/design.md
index 1b4d1cd..4a9795f 100644
--- a/docs/design.md
+++ b/docs/design.md
@@ -661,7 +661,8 @@ generated files; these are resource knobs, not escape hatches, and are recorded
 deliberately.
 
 `scripts/gen_degree.py` is untrusted: Lean re-derives `P n` and checks the Bernstein identity
-with `ring`, so a corrupted coefficient fails the build. Its `--check` mode compares against
+with `ring`, so a corrupted coefficient fails the build. It writes `Degree{n}.lean` under
+`Sendov/FiniteRange/` relative to the repo root, not the shell cwd. Its `--check` mode compares against
 numerical quadrature, and that check has already caught a real bug — a dropped `2ˡ` in
 `(-2c)ˡ` produced a `P` wrong by sign and scale which nevertheless admitted a Bernstein
 representation, with every coefficient negative. **Positivity of a certificate is not
diff --git a/scripts/gen_degree.py b/scripts/gen_degree.py
index 21de418..7e8de7c 100644
--- a/scripts/gen_degree.py
+++ b/scripts/gen_degree.py
@@ -19,6 +19,7 @@
 """
 from fractions import Fraction as F
 from math import comb, lcm
+from pathlib import Path
 
 def mul(p,q):
     r=[F(0)]*(len(p)+len(q)-1)
@@ -222,5 +223,7 @@ def bterm(j):
 
 end Sendov
 '''
-io.open(f"Degree{n}.lean","w",encoding="utf-8").write(src)
-print(f"n={n} deg={d} bytes={len(src)} maxGammaDigits={max(len(str(g)) for g in G)}")
+out = Path(__file__).resolve().parents[1] / "Sendov" / "FiniteRange" / f"Degree{n}.lean"
+out.parent.mkdir(parents=True, exist_ok=True)
+out.write_text(src, encoding="utf-8")
+print(f"wrote {out} n={n} deg={d} bytes={len(src)} maxGammaDigits={max(len(str(g)) for g in G)}")