docs: substantive proof-debt.adoc per standards#203 (supersedes #37)

[hyperpolymath]

Summary

Replaces the thin index in #37 with a substantive classification under the standards#203 trusted-base reduction policy schema.

Corrects the marker count (#37 said "3 escape hatches"; actual is 1). Classifies the single hatch:

• (a) DISCHARGED: none
• (b) BUDGETED: none
• (c) NECESSARY AXIOM: proofs/BetLang.lean:392 substTop_preserves_typing — classical substitution lemma over de Bruijn substitution. Cited from Pierce TAPL Ch. 6 + Software Foundations Vol 2 + Programming Language Foundations in Agda. Promotion path documented per PR #27.
• (d) DEBT: none

The repo has zero sorry declarations. The author's in-file framing at BetLang.lean:387-391 already distinguishes this as an explicit axiom rather than a proof hole; the (c) classification formalises that disposition under the estate-wide policy schema.

Why supersede #37

PR #37's index says "3 escape hatches" (wrong — only 1 axiom), and defers all classification to a stub PROOF-NEEDS.md pointer without actually doing the work. This PR does the substantive classification per the policy schema.

After this PR merges, #37 should be closed as superseded.

Format choice

.adoc per estate-wide convention ("All docs must be .adoc except GitHub-required files" — standards CLAUDE.md). The policy itself allows .md or .adoc.

Test plan

• AsciiDoc renders on GitHub
• GPG-signed commit (key 4A03639C…2867091E, noreply email)
• Auto-merge SQUASH enabled
• CI baseline-rot (Test on Racket 8.11/8.12/current, Code Quality, governance/Workflow-security-linter, governance/Language-anti-pattern) is pre-existing on main — same failures present on #37 and on main's latest commit 6702d2d. Not introduced by this PR.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 55 issues detected

Severity	Count
🔴 Critical	9
🟠 High	18
🟡 Medium	28

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Merge artifact in root",
    "type": "stale",
    "file": "SPEC.core.scm.orig",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No permissions declaration -- add permissions: read-all",
    "type": "missing_permissions",
    "file": "comprehensive-quality.yml",
    "action": "add_permissions",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/main.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/probability.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/src/ternary.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/test/probability_test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/test/ternary_test.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/betlang/betlang/playground/examples/uncertainty.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "Atom creation from untrusted input may exhaust atom table (1 occurrences, CWE-400)",
    "type": "erlang_atom_from_untrusted",
    "file": "/home/runner/work/betlang/betlang/lsp/bet-lsp/build/packages/thoas/src/thoas_decode.erl",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence