coherence pass 2: restore the one-button property, institutionalize audits

- check.sh: proofs memory default 6144 -> 8192 (ReduceSpec's norm_num
  step peaks above 6144; guard aborted gracefully — R3 was broken, S1
  held). Matches pasta's calibration.
- check.sh: dead-file gate now exempts Scalar* (delegated to
  check-scalar.sh); the gate had been un-passable since the scalar layer
  landed, masked by the memory failure.
- check.sh: axiom-audit phase routed through lean-guard (cgroup + flock;
  was raw lean -M), audit temp file moved into the workspace (lake env
  rejects /tmp inputs — the /tmp phase had never run green).
- check-scalar.sh: NEW Phase 3 kernel axiom audit — ScalarProofs.L_val
  must report exactly [propext, Classical.choice, Quot.sound].
- README: signature layer '⏳ planned' (was 'in progress' with nothing
  started); planned certificate names marked as such.

Validated: full check.sh + check-scalar.sh green end-to-end in the pass-2
sweep (see formal-verification-control/COHERENCE-PASS-2.md).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

README.md

@@ -27,8 +27,8 @@ in this repository.
 |-------|-------------|--------|-----------------------|
 | Field 𝔽_p          | `fieldImplementation`    | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
 | Group law (Edwards) | `edwardsImplementation`  | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
-| Scalar mod ℓ        | `scalarImplementation`   | 🔨 foundation | denotation + L=ℓ proven; add/sub/mul in progress |
-| Signature (EdDSA)   | `verifyEquation`          | ⏳ in progress | — |
+| Scalar mod ℓ        | `scalarImplementation` (planned; `L_val` proven)   | 🔨 foundation | denotation + L=ℓ proven; add/sub/mul in progress |
+| Signature (EdDSA)   | `verifyEquation` (planned)          | ⏳ planned | — |
 
 Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started.
 This table is updated only when `verification/check.sh` passes for the layer.

verification/check-scalar.sh

@@ -21,5 +21,21 @@ lake env bash -c "
   cd '$HERE'
   for m in ${PROOFS[*]}; do echo \"  · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done
 " || { echo FAIL; exit 1; }
+echo "=== Phase 3: axiom audit (kernel-level) ==="
+cd "$AENEAS_LEAN"
+lake env bash -c "
+  set -uo pipefail
+  export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\"
+  cd '$HERE'
+  AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean')
+  { echo 'import Proofs.ScalarDenote'; echo '#print axioms ScalarProofs.L_val'; } > \"\$AUD\"
+  OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
+  echo \"\$OUT\"
+  rm -f \"\$AUD\" \"\${AUD%.lean}.olean\"
+  echo \"\$OUT\" | grep -qF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || {
+    echo 'AXIOM AUDIT FAILED: L_val not clean'; exit 1; }
+" || { echo FAIL; exit 1; }
+echo "  L_val axiom-clean"
+
 echo ""
 echo "SCALAR FOUNDATION: gen compiles; denotation + group-order constant (L = ℓ) proven."

verification/check.sh

@@ -20,7 +20,7 @@ source ~/aeneas-toolchain/env.sh
 HERE="$(cd "$(dirname "$0")" && pwd)"
 AENEAS_LEAN="$AENEAS_HOME/backends/lean"
 TIMEOUT="${LEAN_TIMEOUT:-300}"
-export LEAN_MEM_MB="${LEAN_MEM_MB:-6144}"
+export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"  # 8192: ReduceSpec exceeds 6144 (coherence pass 2)
 CORES="${LEAN_MAX_CORES:-0-3}"
 
 # Layer manifests (extended as the pyramid grows; ORDER = import order).
@@ -110,6 +110,7 @@ lake env bash -c "
   for f in Proofs/*.lean; do
     b=\$(basename \"\$f\" .lean)
     [ \"\$b\" = AxiomCheck ] && continue
+    case \"\$b\" in Scalar*) continue;; esac  # scalar layer: checked by check-scalar.sh (coherence pass 2)
     case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f not in check manifest\"; exit 1;; esac
   done
 "
@@ -125,12 +126,12 @@ lake env bash -c "
   set -euo pipefail
   cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
   cd '$HERE'
-  AUD=\$(mktemp /tmp/audit-XXXX.lean)
+  AUD=\$(mktemp '$HERE/.audit-XXXX.lean')
   {
     for i in ${AUDIT_IMPORTS[*]}; do echo \"import \$i\"; done
     for c in ${CERTS[*]}; do echo \"#print axioms \$c\"; done
   } > \"\$AUD\"
-  OUT=\$(taskset -c $CORES timeout --kill-after=15 $TIMEOUT lean -M \${LEAN_MEM_MB:-4096} \"\$AUD\" 2>&1)
+  OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
   echo \"\$OUT\"
   rm -f \"\$AUD\"
   N_CLEAN=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: $EXPECTED\" || true)