WIP: discharge substTop_preserves_typing axiom (Refs #23)

[hyperpolymath]

DRAFT — discharging the substTop_preserves_typing axiom (#23).

What landed (commit 1: ac6c44d)

origin/main (aa65b23) didn't build. lean proofs/BetLang.lean failed with 4 pre-existing errors that blocked any further proof work:

1. progress (L304) — induction ht failed with "index in target's type is not a variable" because HasType [] e T has the concrete [] index. Refactored with generalize hΓ : ([] : Ctx) = Γ at ht + subst hΓ in the branches that need the closed-context invariant (tVar, tApp, tIf, tSample, tDistBind). Used non-@ patterns where possible; tIf still needs @tIf Γ c t T e ... because Lean's auto-bound-implicit order is Γ, c, t, T, e (T appears in the type of t's premise, so it's bound before e).
2. lookup_extend_ge (L367) — broken omega + rw chain (IH over wrong index because induction Γ didn't generalize n). Deleted as unused — the substitution machinery to come will use a cleaner Ctx.insertAt-based formulation, so this had no caller and won't have one.
3. Two orphan /-- ... -/ doc-comments (L386-391, L393-399) not attached to any declaration. Replaced with a one-line pointer to the upcoming Section 8.5.

lean proofs/BetLang.lean now exits 0 with no errors (7 pre-existing unused-variable warnings in preservation remain, untouched).

What's NOT done yet

The actual discharge of substTop_preserves_typing. The axiom is still in place at L420. Attempted to write Section 8.5 in this session but hit a budget wall — the proof structure requires careful TAPL Ch. 9-style infrastructure, and several attempts at the foundational lookup_ctxInsertAt_lt lemma revealed that the natural statement needs an additional k ≤ Γ.length hypothesis (otherwise it's false at empty Γ with k > 0). The deeper friction is Int.toNat (↑n + amount) reasoning at the Expr.var case of shift, especially for amount = -1 (the shift-down in substTop is only sound when no free var 0 survives — needs an auxiliary tracking lemma).

Recipe for the next session

1. ctxInsertAt (non-dot-notation — Ctx := List Ty is an abbrev so Γ.insertAt resolves to List.insertAt which doesn't exist): def ctxInsertAt (Γ : Ctx) (k : Nat) (U : Ty) : Ctx := Γ.take k ++ U :: Γ.drop k.
2. Three lookup lemmas, all needing k ≤ Γ.length:
   • lookup_ctxInsertAt_lt: n < k → Ctx.lookup (ctxInsertAt Γ k U) n = Ctx.lookup Γ n
   • lookup_ctxInsertAt_eq: Ctx.lookup (ctxInsertAt Γ k U) k = some U
   • lookup_ctxInsertAt_gt: n > k → Ctx.lookup (ctxInsertAt Γ k U) n = Ctx.lookup Γ (n - 1)
3. shift_preserves_typing (weakening, amount = 1 only): HasType Γ e T → ∀ k U, k ≤ Γ.length → HasType (ctxInsertAt Γ k U) (shift 1 k e) T. Induction on HasType; binder cases (tLam, tLet) bump k by 1 and recurse. Variable case needs Int.toNat (↑n + 1) = n + 1.
4. subst_preserves_typing (generalised): HasType (ctxInsertAt Γ k S) e T → HasType Γ v S → HasType (ctxInsertAt Γ k S) (subst k (shift (k+1 : Int) 0 v) e) T. Induction on e. Binder cases recurse with k+1 after pulling in the extra shift 1 0.
5. "No surviving var k" tracking lemma: after subst k v e, define a predicate freeVarNotIn k e and prove it holds. Then prove shift_down preserves typing when this predicate holds.
6. Headline: substTop_preserves_typing Γ S T body v hb hv := ... combining the chain. Then delete axiom substTop_preserves_typing at L420 (was 420, may be a few lines off after commit 1). Verify preservation still typechecks.

Estimated ~300-400 LoC remaining. Standard TAPL Ch. 9 mechanisation, but the Int.toNat clamping in BetLang's shift (signed amount) adds non-trivial arithmetic friction at every var case.

Closes #23 once the discharge is complete and the axiom is deleted.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 56 issues detected

Severity	Count
🔴 Critical	9
🟠 High	18
🟡 Medium	29

⚠️ 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": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "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"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence