From bb905dc207621780eec6d41a1aaa2af7d40e7652 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 27 May 2026 08:43:45 +0100 Subject: [PATCH] docs: substantive proof-debt.adoc per standards#203 (supersedes #37) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replaces the thin index in PR #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. Format: .adoc (matches estate-wide doc convention per estate CLAUDE.md "All docs must be .adoc except GitHub-required files"). --- docs/proof-debt.adoc | 84 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 84 insertions(+) create mode 100644 docs/proof-debt.adoc diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc new file mode 100644 index 0000000..4843859 --- /dev/null +++ b/docs/proof-debt.adoc @@ -0,0 +1,84 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += Proof debt +:policy: https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc +:tapl: TAPL (Pierce 2002) Chapter 6 +:discharge-pr: https://github.com/hyperpolymath/betlang/pull/27 + +Per link:{policy}[standards#203] (trusted-base reduction policy), every +soundness-relevant escape hatch in this repo is classified below as one +of: (a) DISCHARGED, (b) BUDGETED, (c) NECESSARY AXIOM, or (d) DEBT. + +Supersedes the thin index in +https://github.com/hyperpolymath/betlang/pull/37[betlang#37] (which +declared "3 escape hatches" — the actual count is 1). + +== Marker count + +1 soundness-relevant escape hatch in this repo: + +* `proofs/BetLang.lean:392` — `axiom substTop_preserves_typing` + +Zero `sorry` declarations. Zero `noncomputable` in soundness positions. + +== (a) Discharged + +No entries. + +== (b) Budgeted — tested with refutation budget + +No entries. + +== (c) NECESSARY AXIOM + +=== `proofs/BetLang.lean:392` — `axiom substTop_preserves_typing` + +[source,lean] +---- +axiom substTop_preserves_typing : + ∀ (Γ : Ctx) (S T : Ty) (body v : Expr), + HasType (S :: Γ) body T → HasType Γ v S → HasType Γ (substTop v body) T +---- + +* **Kind**: classical substitution lemma for typed lambda terms under + de Bruijn substitution. +* **Justification**: discharging requires the full shifting / + substitution calculus over de Bruijn indices, which would triple + the file size and is orthogonal to the BetLang-specific content of + this formalisation. The property is standard and well-known to + hold for this style of substitution. +* **Citation**: {tapl} ("Pure Simply Typed Lambda Calculus" — the + substitution lemma is the canonical preservation prerequisite). + Mechanised independently in many libraries: Software Foundations + Volume 2 § STLC, Programming Language Foundations in Agda § + Properties, Lean Mathlib's `Mathlib.Logic.Function.Iterate` + substitution machinery. +* **Used by**: `preservation` theorem at `proofs/BetLang.lean:398` + (invoked in the `appLam` case to thread typing across + beta-reduction). +* **Author's framing**: the in-file comment at + `proofs/BetLang.lean:387-391` is explicit that this is an axiom, + not a `sorry`: _"IMPORTANT: This is NOT sorry — it is an axiom. + The difference is that axioms are explicit assumptions in the + logical framework, whereas sorry is a proof hole."_ +* **Promotion path** (optional, not blocking): see + link:{discharge-pr}[betlang PR #27] body for a discharge recipe. + Promotion would move this entry to §(a) DISCHARGED and remove the + `axiom` declaration in favour of a proof using the Lean Mathlib + substitution lemmas. + +== (d) DEBT — actively to be closed + +No entries. (If the promotion path above is pursued, the §(c) entry +moves to §(a); it does not pass through §(d) because it has a +principled disposition today.) + +== Cross-references + +* link:{policy}[standards#203] — trusted-base reduction policy + (canonical estate-wide definition) +* `proofs/BetLang.lean` — the formal model where the axiom is + declared and used +* `docs/semantics.md` — language semantics overview +* link:{discharge-pr}[betlang PR #27] — discharge recipe (optional + promotion to §(a))