fix(ci): make the secret scanner and the Lean proof gate actually run (#129)

Two workflows in this repo are rejected by Actions **at parse time**,
before a runner is allocated. Neither has ever produced a result. Two
independent faults, one per file.

## 1. `secret-scanner.yml` — `jobs:` was empty

The job key `scan:` sat at **column 0** — a sibling of `jobs:`, not a
child:

```yaml
jobs:
scan:            # <-- column 0
    permissions:
      ...
```

So `jobs:` parsed as `null` and Actions refused the file.

This is **valid YAML but invalid Actions**, which is why linting never
caught it — a `yaml.safe_load` sweep over all 22 workflows here passes
this file happily. Only Actions' own schema rejects it.

**Consequence:** the job-level `permissions:` block added in #124 is
attached to a top-level key Actions ignores. That fix has been inert,
and **gitleaks has never executed in this repository.** The diagnosis in
#124 was right and the reusable SHA pin is correct and untouched — the
fix simply never took effect.

Fix: indent `scan:` by two spaces. The child keys were already at 4, so
the block nests correctly.

## 2. `lean-proofs.yml` — unquoted `": "` in three step names

Parse error at line 60, column 63: `mapping values are not allowed
here`. An unquoted YAML scalar cannot contain `": "`, and three `-
name:` values do:

```
(§7.1 not-regular: DFA + pigeonhole)
(§7.3 CFL closure: union/concat/star)
(§7.3 non-closure: pumping foundation)
```

Fix: quote all three.

**This one inverts the usual failure mode.** `lean-proofs.yml` is an
*honest* gate — it installs the pinned Lean toolchain and runs `lean
<file>` with no `|| true`, and was written specifically to stop the
bit-rot recorded in `docs/proofs/verification/AUDIT.md`. It is not a
fake gate that passes when it shouldn't. It is a **real gate that has
never run.**

The proofs behind it are green, verified locally before this PR:

| | prover | result |
|---|---|---|
| 6 × `.lean` | Lean 4.30.0 (per `lean-toolchain`) | all PASS |
| 3 × `.v` | Coq 8.20.1 | all PASS |

Trust base is clean: **zero `sorry`, `Admitted`, `axiom` or
`Parameter`.** So nothing had rotted — the guard was simply switched
off.

## Verification

All 22 workflow files now pass a structural check mirroring what Actions
requires: parses as a mapping, has a trigger, and `jobs` is a non-empty
mapping in which every job has `steps` or `uses`.

Expect this PR itself to demonstrate the fix: `lean-proofs` triggers on
changes to `.github/workflows/lean-proofs.yml`, so it should run here
for the first time. **`Secret Scanner` will also run for the first time
— expect findings that need triage rather than a clean pass.**

## Recognising this class

Both faults share one signature, worth knowing:

- the run is listed by **file path** instead of workflow name
- `gh run view --log-failed` returns **"log not found"**
- `gh pr checks` shows **nothing at all** — a parse-rejected workflow
creates no check run

Only `gh run list --json conclusion` reveals them.

Estate note: the col-0 `jobs:` fault is **not** widespread. A scan of
all 13,330 workflow files across `hyper-repos`/`meta-repos`/`repos`
found it in exactly two — this repo and
`voyage-enterprise-decision-system`, byte-identical in shape. That one
is being fixed in the same pass.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/lean-proofs.yml

@@ -57,19 +57,19 @@ jobs:
           lean docs/proofs/verification/WokeGrammarStructure.lean
           echo "✅ WokeGrammarStructure.lean verified"
 
-      - name: Verify WokeGrammarRegular.lean (§7.1 not-regular: DFA + pigeonhole)
+      - name: "Verify WokeGrammarRegular.lean (§7.1 not-regular: DFA + pigeonhole)"
         run: |
           set -euo pipefail
           lean docs/proofs/verification/WokeGrammarRegular.lean
           echo "✅ WokeGrammarRegular.lean verified"
 
-      - name: Verify WokeGrammarCFL.lean (§7.3 CFL closure: union/concat/star)
+      - name: "Verify WokeGrammarCFL.lean (§7.3 CFL closure: union/concat/star)"
         run: |
           set -euo pipefail
           lean docs/proofs/verification/WokeGrammarCFL.lean
           echo "✅ WokeGrammarCFL.lean verified"
 
-      - name: Verify WokeGrammarPumping.lean (§7.3 non-closure: pumping foundation)
+      - name: "Verify WokeGrammarPumping.lean (§7.3 non-closure: pumping foundation)"
         run: |
           set -euo pipefail
           lean docs/proofs/verification/WokeGrammarPumping.lean

.github/workflows/secret-scanner.yml

@@ -10,7 +10,7 @@ concurrency:
 permissions:
   contents: read
 jobs:
-scan:
+  scan:
     # The reusable's gitleaks job requests pull-requests: write (PR summary
     # comment) and actions: read (workflow-run metadata) at job level; the
     # caller must grant at least that or the run startup-fails.