docs+annotate: Lambda cluster — inline AXIOM: comments + §(c)/§(d) proof-debt entries

Phase 2a of the standards#203 trusted-base reduction policy rollout
(follow-up to #58/#59 Coq triage). First cluster: `proofs/coq/lambda/`
and `proofs/lean4/LambdaCNO.lean`.

Coq (2 markers, both §(c) AXIOM per Phase 1 triage):
- `LambdaCNO.v:356` `y_not_cno` — inline `(* AXIOM: ... *)` added
- `LambdaCNO.v:376` `eta_equivalence` — inline `(* AXIOM: ... *)` added

Lean (3 markers — new Phase 2a triage):
- `LambdaCNO.lean:183` `subst_closed_term` → §(d) DEBT
  (provable by induction on `t`; INDEFINITE owner @hyperpolymath)
- `LambdaCNO.lean:232` `y_combinator_not_identity` → §(c) AXIOM
  (mirrors Coq `y_not_cno`; inline `-- AXIOM:` added)
- `LambdaCNO.lean:258` `eta_equivalence` → §(c) AXIOM
  (mirrors Coq `eta_equivalence`; inline `-- AXIOM:` added)

`docs/proof-debt.md` gains a Phase 2a triage section and a §(d) entry
for the Lean DEBT item. The two §(c) Lean entries are inline-annotated
per the policy contract (`-- AXIOM:` leading comment).

Verification: `bash standards/scripts/check-trusted-base.sh .` now
reports 0 Lambda errors (down from 5 of the original 129 markers).
The remaining 123 errors are the Quantum/Filesystem/Physics clusters,
scheduled for follow-up PRs.

Refs standards#203, absolute-zero#58, absolute-zero#59.

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

Author: hyperpolymath

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.

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.

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