η extension of MECH-1 (PROOF-STATUS OPEN row "ET-1..3 (η)") — deferred; campaign design ready to launch

[hyperpolymath]

Deferred by owner decision 2026-07-27 ("skip this bit and record it as an issue for now"). A proof campaign was fully designed and briefly launched (wf_e91ac441-9b8), then stopped before any attempt produced output — nothing to salvage, nothing lost. This issue is the resume point.

The goal

Close PROOF-STATUS's OPEN row "ET-1..3 (η): η-laws / η-long normal forms extension of MECH-1" — βη-decidability for the L1 kinded calculus, extending the closed β-fragment ET-2 (PR #24/#27).

Design-critical facts (verified against main @ 859395a)

• Current Nf.ne : Var Γ k → Sp Γ k j → Nf Γ j admits neutrals at any kind — the landed forms are β-normal, NOT η-long. The extension needs a new η-long discipline: ne restricted to .star, so every arrow-kinded normal form is a lam.
• DefEq = refl/symm/trans/beta/arrowCong/lamCong/appCong — no η rule. Spines are left-nested; arrow is the base-kinded object arrow, distinct from the kind arrow.
• ET-2's modules (SubstLemmas/Soundness/Completeness/Decidable) are the toolbox: cast toolkit (swp/remSwap + by subst h; rfl push lemmas), sum-measure for subst/subst, hand-rolled mutual DecidableEq pattern.

The 8 goals (purely additive; new Systemet/L1/Eta* modules)

1. η-long NfE/SpE (ne at .star only) + weakening
2. Total η-long normalizer nfE — either K–A-native hereditary substitution on η-long forms (MSFP 2010 is natively η-long) or η-expansion-by-kind-recursion over the existing β-nf with transfer lemmas
3. DefEqE = DefEq + η rule, plus the embedding DefEq t u → DefEqE t u
4. Stability nfE_emb 5. Soundness DefEqE t (embNfE (nfE t)) 6. Completeness 7. defEqE_iff_nfE + decEqNfE + decDefEqE
5. Anti-vacuity sanity example: arrow-kinded neutral f — η-equality derivable, nfE identifies f with its expansion, β-nf distinguishes them

Resume handle

Campaign script (4 independent attempts + seeded round 2 + apply-and-gate + 2 adversarial reviewers, hardcoded paths, full gotcha bank in the briefing):
~/.claude/projects/-home-hyperpolymath-developer/f9a6bee1-.../workflows/scripts/l1-eta-campaign-wf_e91ac441-9b8.js
Relaunch: Workflow({scriptPath, resumeFromRunId: "wf_e91ac441-9b8"}) — needs a Fable/high-capability session and a spend ceiling that tolerates ~4–6 max-effort proof agents. Campaign clone was at $CLAUDE_JOB_DIR/tmp/systemet-eta (branch proofs/l1-eta-extension, baseline green); recreate with a fresh clone of main if gone.

Estimated shape: comparable to the ET-2 campaign (which two of four attempts fully closed).

[hyperpolymath]

Campaign run 2 (2026-07-28): spend-limited, but half the work is salvaged and landed

All four Fable attempts died on the monthly spend limit (0/4 reported; 271k tokens, ~41 min). One attempt had written six modules before dying — five build green and are now on proofs/l1-eta-extension, draft PR #34, axiom-audited [propext, Quot.sound].

Landed (goals 1, 3, and the DecidableEq half of 7)

• EtaNormal — η-long NfE/SpE with ne : Var Γ k → SpE Γ k .star → NfE Γ .star (neutrals at base kind only) + spEKindLe
• EtaConversion — DefEqE with a real η rule DefEqE t (.lam (.app (wkTy .vz t) (.var .vz))), plus proven defEq_to_defEqE
• EtaSubstLemmas (26 theorems), EtaHsub, EtaDecEq

The precise obstruction (goal 2 — the normalizer)

EtaExpand.lean is excluded: it stubbed two cases of adjWkv with the non-existent identifier sorryAx_placeholder. The lemma being fought:

theorem adjWkv {Γ : Ctx} {b j : Kind} {X : Var Γ b} {H : Var (rem X) b}
    (a : Adj X H) (w : Var (rem (swp X H)) j) :
    castV (adjCtx a) (wkv (swp X H) w)
      = castV (congrArg rem (wkv_swp X H))
          (wkv (swp (wkv X H) (swp X H))
            (castV (remSwap (wkv X H) (swp X H)).symm w))

— the there/vz and there/vs cases, i.e. weakening-exchange across an adjacent variable pair (Adj), transported along wkv_swp. A resumed campaign should start here, not from scratch: the toolkit around it is already green.

Resume

Same handle (resumeFromRunId: wf_e91ac441-9b8) but the script should be re-pointed at the branch so attempts inherit the landed modules. Needs spend headroom — this is the second run killed by the limit; consider a token budget at launch or fewer parallel attempts.

[hyperpolymath]

EtaExpand.lean diagnosed: four defects, not two stubs — one now fixed

I attempted the blocker directly on Opus 5 (no Fable spend). The file is worse than the earlier note implied — it ends at line 138 mid-proof, so the entire promised cluster (etaSubstHit, etaLaw, etaSubstAdj/etaSubstAdjSp, appSpEtaNe, nappEtaNe) was never written. Of what exists, four things break:

#	Location	Defect	Status
1	etaSubstMiss, .arr case	"unsolved goals" where LHS and RHS are literally identical — the tactic block just never closed	✅ FIXED — append rfl after rw [h2]
2	wkNfE_etaNe line ~52	rw fails: pattern wkNfE w.vs (etaNe c x.vs ((wkSpE Var.vz sp).cons ...)) not found. Root cause is a dependent-type mismatch: sp : SpE (rem w) x _ but the rewrite needs SpE (rem Var.vz) x _. Lean flags it as not type-correct at instances transparency — the semireducible-defeq trap in the gotcha bank	open
3	adjSwp line ~118	castV_vs (adjCtx (Adj.there a)) (adjCtx a) — application type mismatch: castV_vs wants (c :: Δ) = (c :: Δ') but gets rem (wkv X.vs H.vs) = rem X.vs. Needs the rem (Var.vs _) ≡ _ :: rem _ step made explicit (my named-argument attempt did not work)	open
4	adjWkv lines ~134/135	the two sorryAx_placeholder cases (there/vz and there/vs)	open

The fix for #1 (verified — this error disappears)

     simp only [wkv, substSpE] at h2
     rw [h2]
+    rfl
 termination_by structural j => j

Guidance for the resumed run

• Start from defect 3, not 4. adjSwp is the smaller cast problem and adjWkv uses the same rem (Var.vs _) reshaping; cracking 3 likely supplies the idiom for 4.
• Defect 2 is independent of the Adj machinery and can be attacked in parallel.
• All four are below the mutual cluster that was never written, so goal 2 (the normalizer nfE) remains a substantial piece of work even once these clear — budget accordingly.
• Everything else from that attempt is already landed and green (PR proofs(lean4): land the green half of the η extension (PARTIAL — ET-1..3 η) #34); the resumed run should branch from proofs/l1-eta-extension, not main.