proofs(lean4): land the green half of the η extension (PARTIAL — ET-1..3 η) - #34
Conversation
…1..3 eta)
Salvaged from a campaign whose four attempts all died on a spend limit before
reporting. One attempt had written six modules; five build green and are landed
here. The sixth (EtaExpand) is NOT included -- see below.
Landed, axiom-audited [propext, Quot.sound]:
EtaNormal eta-long normal forms NfE/SpE. The core design point: `ne` is
restricted to `.star` (`ne : Var G k -> SpE G k .star ->
NfE G .star`), so every arrow-kinded normal form is a `lam` --
the discipline the beta-only `Nf` deliberately lacks. Plus
spEKindLe.
EtaConversion DefEqE = all DefEq rules PLUS a genuine eta rule
`DefEqE t (.lam (.app (wkTy .vz t) (.var .vz)))`, and
defEq_to_defEqE : DefEq t u -> DefEqE t u (eta extends beta).
EtaSubstLemmas 26 theorems: cast/exchange toolkit for NfE/SpE.
EtaHsub hereditary substitution on eta-long forms.
EtaDecEq DecidableEq instances for NfE and SpE.
NOT landed, and why: EtaExpand.lean fails to compile because the agent stubbed
two cases of `adjWkv` (a weakening-exchange lemma for adjacent variable pairs)
with the identifier `sorryAx_placeholder`, which does not exist. That is an
honest failure -- it cannot masquerade as proven -- but it means goal 2 (the
eta-long normalizer nfE) is genuinely unproven, so the file is excluded rather
than shipped unlisted (an unMANIFESTed proof file is one of the failure modes
this repo's gate deliberately catches).
Scope, stated so nothing drifts: this does NOT close the "ET-1..3 (eta)" OPEN
row. Landed = goals 1, 3, and the DecidableEq half of 7. Still open = the
normalizer, soundness, completeness, defEqE_iff_nfE, decDefEqE, and the
anti-vacuity example. PROOF-STATUS records exactly that.
Verified: cold rebuild green (21 jobs); check-proofs.sh and scan-dangerous.sh
real exit 0; check-proof-status.sh real exit 0 after the gated 15->20 update.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
|
|
Note Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime. CI failed: K9 contract validation failed because 18 scanned K9 files are missing required fields such as the 'K9!' magic number, signature, and pedigree blocks.OverviewA single validation job failed due to 20 errors in K9 contract file formatting and required metadata blocks across 18 scanned files, directly blocking the CI pipeline. FailuresK9 Contract Validation Failure (confidence: high)
Summary
Code Review ✅ Approved 1 resolved / 1 findingsLands five verified Lean 4 modules implementing η-long forms, conversion rules, substitution lemmas, hereditary substitution, and decidable equality. Consider adding the new DecidableEq instances to Audit.lean for proper axiom auditing.
✅ 1 resolved✅ Quality: DecidableEq instances not axiom-audited in Audit.lean
Tip Comment OptionsDisplay: compact → Showing less information. Comment with these commands to change the behavior for this request:
Was this helpful? React with 👍 / 👎 | Gitar |
![gitar-bot[bot]](https://avatars.githubusercontent.com/in/827041?s=60&v=4){kind=small}
|
|
1 participant
Partial, deliberately. Salvaged from the η campaign whose four attempts all hit the monthly spend limit before reporting. One had written six modules; five build green and are landed; the sixth is excluded.
EtaNormalNfE/SpE—nerestricted to.star, so every arrow-kinded normal form is alam(the discipline β-onlyNflacks)EtaConversionDefEqE= β rules + a genuine η rule, anddefEq_to_defEqE : DefEq t u → DefEqE t uEtaSubstLemmasEtaHsubEtaDecEqDecidableEqforNfE/SpEExcluded and why:
EtaExpand.leanstubs two cases ofadjWkvwith the identifiersorryAx_placeholder, which doesn't exist — so it doesn't compile. Honest (it can't pass as proven) but it means goal 2, the normalizernfE, is genuinely unproven. Shipping it unlisted would trip the very failure mode this repo's gate is built to catch.Does NOT close the OPEN row. Landed = goals 1, 3, DecidableEq half of 7. Open = normalizer, soundness, completeness,
defEqE_iff_nfE,decDefEqE, anti-vacuity example. PROOF-STATUS says exactly that; issue #32 tracks the rest.Verified: cold rebuild 21 jobs green; all three gates real exit 0;
#print axioms→[propext, Quot.sound].