diff --git a/verification/Proofs/EdDouble.lean b/verification/Proofs/EdDouble.lean
index 7f0a426..09142c9 100644
--- a/verification/Proofs/EdDouble.lean
+++ b/verification/Proofs/EdDouble.lean
@@ -215,6 +215,7 @@ theorem proj_double_spec (p : ProjPoint) (hp : ProjValid p) :
   let* ⟨ YY, YY_post1, YY_post2 ⟩ ← square_spec' by edis
   -- ZZ2 ← square2 p.Z          ⟪ZZ2⟫ = 2·(⟪p.Z⟫·⟪p.Z⟫),  Bnd 2⁵³
   let* ⟨ ZZ2, ZZ2_post1, ZZ2_post2 ⟩ ← square2_spec' by edis
+  -- v4.1.2 ORDER (differs from the v4.1.3/risc0 body — same ops, reordered):
   -- X_plus_Y ← p.X + p.Y       (unreduced add of two reduced values, Bnd 2⁵³)
   let* ⟨ XpY, XpY_post1, XpY_post2 ⟩ ← add_spec'' by edis
   -- X_plus_Y_sq ← square X_plus_Y
diff --git a/verification/lean-guard b/verification/lean-guard
index 256ef42..10a0af3 100755
--- a/verification/lean-guard
+++ b/verification/lean-guard
@@ -106,7 +106,7 @@ if systemd-run --user --scope -p MemoryMax=10M --quiet -- /bin/true 2>/dev/null;
     # --scope runs the command as a child of THIS shell (env inherited),
     # merely placing it in a fresh cgroup with the hard caps below.
     systemd-run --user --scope --quiet \
-        -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M -p LimitCORE=0 \
+        -p MemoryMax="${CGROUP_MB}M" -p MemorySwapMax=256M \
         -- taskset -c "$CORES" \
            timeout --signal=TERM --kill-after=15 "$TIMEOUT_SEC" \
            lean -M "$MEM_MB" -o "$OLEAN_FILE" "$LEAN_FILE" "$@"