diff --git a/docs/proof-debt.md b/docs/proof-debt.md
index b1394f0..c032314 100644
--- a/docs/proof-debt.md
+++ b/docs/proof-debt.md
@@ -31,6 +31,20 @@ Out of scope for Phase 1 (still in §(d) pending future triage):
 52 Lean 4 `axiom` declarations and the 7 Idris2 postulates tracked by
 [#27](https://github.com/hyperpolymath/absolute-zero/issues/27).
 
+## Phase 2a triage — Lean Lambda cluster (2026-05-27)
+
+Per-cluster Lean triage rolling out 2026-05-27 in cluster-sized PRs.
+First cluster: `proofs/lean4/LambdaCNO.lean` (3 axioms).
+
+| Line | Identifier | Disposition | Justification |
+|-----:|------------|-------------|---------------|
+| 183  | `subst_closed_term`        | §(d) DEBT   | Standard metatheoretic property of lambda calculus; provable by induction on `t` once the substitution-on-closed-terms lemma is mechanised. |
+| 232  | `y_combinator_not_identity` | §(c) AXIOM | Non-termination claim about Y combinator; requires step-indexed semantics or coinduction (same justification as Coq `y_not_cno`). |
+| 258  | `eta_equivalence`           | §(c) AXIOM | η-equivalence is not derivable under β-only reduction (same justification as Coq `eta_equivalence` at LambdaCNO.v:376). |
+
+The two §(c) entries are annotated inline with `-- AXIOM:` leading
+comments. The §(d) entry below has an owner + deadline.
+
 ## (a) DISCHARGE backlog (Coq, 17)
 
 Provable propositions currently stated as `Axiom`. Enumerated in
@@ -52,12 +66,33 @@ Full enumeration in [`docs/proof-debt-triage.md`](./proof-debt-triage.md).
 
 ## (d) DEBT — actively to be closed
 
-After Phase 1, the §(d) bucket contains only the 52 Lean axioms and
-7 Idris2 postulates that have not yet been triaged. Coq markers are
+After Phase 1, the §(d) bucket contains only the Lean axioms and 7
+Idris2 postulates that have not yet been triaged. Coq markers are
 no longer in §(d).
 
+### Lean — provable, awaiting proof
+
+- `proofs/lean4/LambdaCNO.lean:183` — `subst_closed_term`
+  - **Owner**: @hyperpolymath
+  - **Plan**: discharge by induction on `t : LambdaTerm`; closed-term
+    invariant carries through `LVar`, `LAbs`, `LApp` cases. Sibling to
+    Coq's `subst` lemmas in `proofs/coq/lambda/LambdaCNO.v`.
+  - **Deadline**: INDEFINITE (no proof-PR scheduled yet — provable;
+    awaits Lean-side discharge push).
+
+### Lean — pending triage
+
+49 Lean axioms remain to be triaged (FilesystemCNO 21, QuantumCNO 14,
+StatMech 14). Triage planned in cluster-sized PRs through
+2026-06 — see this file's status block at the bottom.
+
+### Idris2 — pending triage
+
+7 Idris2 postulates in `src/abi/Layout.idr`. Tracked by
+[#27](https://github.com/hyperpolymath/absolute-zero/issues/27).
+
 ```
-(no Coq markers in §(d) post Phase 1; see triage doc for §a/§b/§c.)
+(Coq markers no longer in §(d) post Phase 1; see triage doc for §a/§b/§c.)
 ```
 
 > If `129` > 30, the list above shows the first 30 only.
diff --git a/proofs/coq/lambda/LambdaCNO.v b/proofs/coq/lambda/LambdaCNO.v
index 655f3a1..c931a52 100644
--- a/proofs/coq/lambda/LambdaCNO.v
+++ b/proofs/coq/lambda/LambdaCNO.v
@@ -353,6 +353,10 @@ Definition y_combinator : LambdaTerm :=
 
     This is a fundamental result in lambda calculus and is safely axiomatized.
 *)
+(* AXIOM: y_not_cno; non-termination claim about the Y combinator —
+   requires step-indexed semantics or coinduction to discharge within
+   the working logic. §(c) NECESSARY AXIOM per docs/proof-debt.md
+   (triage: docs/proof-debt-triage.md row LambdaCNO.v:356). *)
 Axiom y_not_cno : ~ is_lambda_CNO y_combinator.
 
 (** ** Practical Examples *)
@@ -373,6 +377,10 @@ Definition snd : LambdaTerm :=
 (** ** Eta Equivalence *)
 
 (** Eta reduction: (λx. f x) ≡ f *)
+(* AXIOM: eta_equivalence; η-equivalence is not derivable under β-only
+   reduction — requires an extra reduction rule or extensional equality.
+   §(c) NECESSARY AXIOM per docs/proof-debt.md (triage:
+   docs/proof-debt-triage.md row LambdaCNO.v:376). *)
 Axiom eta_equivalence :
   forall f : LambdaTerm,
     beta_reduce_star (LAbs (LApp f (LVar 0))) f.
diff --git a/proofs/lean4/LambdaCNO.lean b/proofs/lean4/LambdaCNO.lean
index a5f7d32..066c61e 100644
--- a/proofs/lean4/LambdaCNO.lean
+++ b/proofs/lean4/LambdaCNO.lean
@@ -229,6 +229,9 @@ def y_combinator : LambdaTerm :=
 
 /-- Y is NOT a CNO because it doesn't act as identity.
     Y f reduces to f (Y f), not back to f. -/
+-- AXIOM: y_combinator_not_identity; non-termination claim about the Y combinator —
+--   requires step-indexed semantics or coinduction to discharge.
+--   §(c) NECESSARY AXIOM per docs/proof-debt.md (Lean Lambda triage 2026-05-27).
 axiom y_combinator_not_identity :
   ¬ BetaReduceStar (LApp y_combinator lambda_id) lambda_id
 
@@ -255,6 +258,9 @@ example : BetaReduceStar (LApp church_zero church_zero) (LAbs (LVar 0)) := by
 /-! ## Eta Equivalence -/
 
 /-- Eta reduction: (λx. f x) ≡ f -/
+-- AXIOM: eta_equivalence; η-equivalence is not derivable under β-only reduction —
+--   requires an extra reduction rule or extensional equality.
+--   §(c) NECESSARY AXIOM per docs/proof-debt.md (Lean Lambda triage 2026-05-27).
 axiom eta_equivalence (f : LambdaTerm) :
   BetaReduceStar (LAbs (LApp f (LVar 0))) f