proofs: discharge substTop_preserves_typing axiom (closes #23) (#40)

## Summary

Discharges the `axiom substTop_preserves_typing` introduced as a
placeholder in PR #27. The axiom is replaced by a fully-proved theorem
of the same signature. After this PR, the file's only axiom dependencies
are Lean 4 core (`propext`, `Classical.choice`, `Quot.sound`).

## What's in the proof (≈ +537 LoC in `proofs/BetLang.lean`)

Standard TAPL Ch. 6 / Ch. 9 de Bruijn machinery, adapted to BetLang's
signed-`Int` `shift` (which uses `Int.toNat` clamping):

- `Ctx.insertAt Γ k U := Γ.take k ++ U :: Γ.drop k` plus 3 lookup lemmas
(`_lt`, `_eq`, `_gt`, all needing `k ≤ Γ.length`) and 2 computational
lemmas.
- `shift_preserves_typing` — weakening for `shift 1 k`.
- `shift_down_shift_up` — cancellation `shift (-1) k (shift 1 k e) = e`,
unconditional (no clamping hazard because shift 1 always pushes vars ≥ k
strictly above the cutoff).
- `shift_one_comm_general : i ≤ j → shift 1 i (shift 1 j e) = shift 1
(j+1) (shift 1 i e)`. The recipe's `shift_one_comm` (cutoff 0 only)
doesn't admit a clean induction because lam/let recurse at `i = 1`;
generalised here, with the original as a one-line corollary.
- `substAt_preserves_typing` — combined subst-and-shift-down,
parameterised over the prefix length k. Proved by induction on the
expression (cleaner than induction on the typing derivation, per the PR
#27 recipe).
- `substTop_preserves_typing` — corollary at k = 0, restoring the exact
signature that `preservation` consumes.

Also includes one tag-along commit (`feat(security)`) that adds
`permissions: read-all` to `comprehensive-quality.yml` — an orphaned
local commit I restored from reflog mid-session.

## Test plan

- [x] `lean proofs/BetLang.lean` exits 0 (28 pre-existing/cosmetic
unused-variable warnings, no errors).
- [x] `grep -nE "\baxiom\b|\bsorry\b|\bAdmitted\b" proofs/BetLang.lean`
returns only one comment match at line 19 ("no sorry") — which is now
actually true.
- [x] No new axiom dependencies (verified by `#print axioms` chain
reaching only `propext`, `Classical.choice`, `Quot.sound`).
- [x] All call sites of `substTop_preserves_typing` in `preservation`
continue to typecheck unchanged.

Closes #23.

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

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/comprehensive-quality.yml

@@ -9,6 +9,8 @@ on:
   schedule:
     - cron: '0 5 * * 0'
 
+permissions: read-all
+
 jobs:
   # DEPENDABILITY - Stability and reliability
   dependability:

CHANGELOG.md

@@ -7,6 +7,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Changed
+- `proofs/BetLang.lean`: discharged `substTop_preserves_typing` axiom with a fully mechanised proof (`Ctx.insertAt` + lookup lemmas, weakening, shift cancellation/commutation, combined substitute-and-shift-down lemma). No `axiom` declarations remain in the file; the only axiom dependencies are Lean 4 core (`propext`, `Classical.choice`, `Quot.sound`). Closes #23.
+
 ### Added
 - RSR (Rhodium Standard Repository) compliance improvements
 - `.gitignore` for Racket projects