docs(proof-debt): seed docs/proof-debt.md per standards#203 schema

[hyperpolymath]

Per-repo proof-debt triage for betlang, applying the estate-wide
Trusted-Base Reduction Policy that landed at
standards#203 and
was filled in by
standards#222.
The detection gate is scripts/check-trusted-base.sh
(standards#211).

What this PR does

1. Adds docs/proof-debt.md matching the schema-conformant per-repo
   form (the same shape as
   standards/docs/proof-debt.md@standards#213).
2. Enumerates the 1 real marker in proofs/BetLang.lean (the
   axiom substTop_preserves_typing at L392) under §(d) DEBT, with
   a full discharge recipe inlined from the body of
   PR #27.
3. Documents the 3 comment-skip false positives (lines 19, 387, 388)
   at the top of docs/proof-debt.md as a marker-count table.
4. Adds an inline -- AXIOM: substTop_preserves_typing — disposition §(d) DEBT ... annotation 5 lines preceding the axiom so the
   check-trusted-base.sh gate flips from naked-marker to documented.

Classification rationale

substTop_preserves_typing is §(d) DEBT, not §(c) NECESSARY AXIOM:

• It is the standard top-level substitution-preservation lemma (Pierce,
  TAPL Ch.9). It is constructively provable in Lean 4 by induction on
  the typing derivation, factored through a generalised
  substAt_preserves_typing plus three Ctx.insertAt lookup lemmas.
• It does not encode any metatheoretic assumption (no funExt, no
  choice, no UIP, no propositional truncation).
• It exists in the source only because a full de Bruijn substitution
  calculus would, per the inline doc-comment, "triple the file size" —
  a cost judgement (which §(d) DEBT captures) not a necessity
  judgement (which §(c) would capture).
• A partial implementation already lives on a local working branch
  (proofs/discharge-substTop-axiom-23, commit 8fa128d); the
  six-step discharge recipe is inlined verbatim in the new
  docs/proof-debt.md from the body of merged PR
  #27.
• Issue #23 was
  closed optimistically when PR WIP: discharge substTop_preserves_typing axiom (Refs #23) #27 merged the build-fix half of the
  work; the axiom itself remained in source. The new §(d) entry
  records "INDEFINITE" as the deadline pending re-open.

Verification

Locally:

$ bash /path/to/standards/scripts/check-trusted-base.sh .
[INFO] Found 3 soundness-relevant escape hatch(es).
[OK] proof-debt document(s) found: docs/proof-debt.md PROOF-NEEDS.md
[OK] All 3 escape hatch(es) are documented (inline annotation
     or entry in: docs/proof-debt.md PROOF-NEEDS.md).

(The "3" reflects the post-comment-skip count from the script's
is_comment_line heuristic: L19 is line-comment-skipped, L387 + L388
survive as continuation lines of a /-- ... -/ block, L392 is the
real declaration. All three are covered by docs/proof-debt.md's
path enumeration plus the inline AXIOM: annotation within 5 lines.)

References

• hyperpolymath/standards#203 — policy
• hyperpolymath/standards#211 — enforcement script
• hyperpolymath/standards#222 — fill-in pass (open, auto-merge armed)
• hyperpolymath/betlang#23 — tracking issue (closed; axiom still in source)
• hyperpolymath/betlang#27 — merged build-fix PR carrying the discharge recipe in its body

Test plan

• bash scripts/check-trusted-base.sh . exits 0 on this branch (verified locally)
• CI trusted-base job (when wired) reports [OK] on the merged main

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

🤖 Generated with Claude Code