docs+annotate: Lambda cluster — inline AXIOM: comments + Lean Phase 2a triage (#60)

## Summary

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

### Coq (2 markers, both §(c) AXIOM per #58 triage)
- `proofs/coq/lambda/LambdaCNO.v:356` `y_not_cno` — inline `(* AXIOM:
... *)` annotation added.
- `proofs/coq/lambda/LambdaCNO.v:376` `eta_equivalence` — inline `(*
AXIOM: ... *)` annotation added.

### Lean (3 markers — new Phase 2a triage)
| Line | Identifier | Disposition |
|-----:|------------|-------------|
| 183 | `subst_closed_term` | §(d) DEBT (provable; INDEFINITE) |
| 232 | `y_combinator_not_identity` | §(c) AXIOM (inline annotation
added) |
| 258 | `eta_equivalence` | §(c) AXIOM (inline annotation added) |

### docs/proof-debt.md
- New "Phase 2a triage — Lean Lambda cluster" section with per-marker
table.
- §(d) bucket gains the Lean `subst_closed_term` DEBT entry (owner +
INDEFINITE deadline).

## Verification

```
$ bash ../standards/scripts/check-trusted-base.sh .
[INFO] Found 129 soundness-relevant escape hatch(es).
[OK] proof-debt document(s) found: docs/proof-debt.md
[ERROR] 123/129 escape hatch(es) are undocumented.
```

**Lambda-specific errors: 0** (down from 5).
The remaining 123 errors are the Quantum / Filesystem / Physics
clusters, scheduled for follow-up PRs (Phase 2b/2c/2d).

## Test plan
- [x] check-trusted-base.sh reports 0 errors on Lambda lines.
- [x] All inline annotations precede Axiom / axiom within the script's
5-line lookback.
- [x] Lean §(d) DEBT entry has owner + deadline per standards#203
schema.
- [ ] Coq build still green (no semantic change — only added comments).
- [ ] Lean build still green (no semantic change — only added comments).

Refs standards#203, #58, #59.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

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