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

Activity

1. hyperpolymath commented on Jul 28, 2026

   

   hyperpolymath

   on Jul 28, 2026

   OwnerAuthor

   More actions

   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.
2. hyperpolymath

   added a commit that references this issue on Jul 28, 2026

   proofs(lean4): land the green half of the η extension (PARTIAL — ET-1…

   ...

   b4a59d0
3. hyperpolymath commented on Jul 28, 2026

   

   hyperpolymath

   on Jul 28, 2026

   OwnerAuthor

   More actions

   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.
4. hyperpolymath

   added a commit that references this issue on Jul 29, 2026

   docs(state): refresh AFFIRMATION + STATE.a2ml; resync the template va…

   ...

   b5f7411
5. hyperpolymath

   added

   design

   on Aug 24, 2026
6. settings

   removed

   design

   on Sep 19, 2026
7. hyperpolymath

   added

   priority:p3Low - nice to haveLow - nice to have

   proofsFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debtFormal verification: Agda, Coq, Idris, Lean, Z3/SMT, axiom debt

   scope:repoConfined to this repositoryConfined to this repository

   on Sep 30, 2026
8. hyperpolymath

   added a commit that references this issue on Nov 10, 2026

   docs: add the STATE v2 thin journal (docs/status/JOURNAL.adoc) (#96)

   ...

   6e5706c