ci(proofs): add weekly schedule so the proof gate re-checks main

The Proofs Gate is path-filtered: the `changes` job skips the heavy
type-check unless a PR/push touches src/abi/**, cartridges/**/abi, etc.
A break already in main (merged before this gate existed, or via a path
the filter ignores) is therefore never re-detected — every off-path PR's
typecheck job is skipped and reports success to the required check.

Add a weekly `schedule` trigger. On a schedule event the detect step
leaves run=true (its default), so the full core + every-cartridge Idris2
type-check runs unconditionally against main and catches proof drift.

Motivated by a duplicate `allTake` definition that sat in
src/abi/Boj/SafetyLemmas.idr on main with a green gate (fixed separately).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/proofs.yml

@@ -22,6 +22,17 @@ on:
   pull_request:
     branches: [main]
   workflow_dispatch:
+  # Weekly baseline re-verification of main. The `changes` path-filter below
+  # skips the heavy type-check on PRs/pushes that don't touch src/abi/** (so an
+  # off-path PR isn't blocked and doesn't pay for a 45-min Idris2 build). The
+  # side effect is that a proof break ALREADY living in main — merged before
+  # this gate existed, or via a path the filter ignores — is otherwise never
+  # re-detected. On a `schedule` event the detect step leaves run=true (its
+  # default), so the full core + every-cartridge type-check runs unconditionally
+  # and catches such drift. (This is exactly how a duplicate `allTake` in
+  # SafetyLemmas.idr sat in main with a green gate — see PR fixing it.)
+  schedule:
+    - cron: '17 6 * * 1'   # Mondays 06:17 UTC
 
 permissions:
   contents: read