docs(state): refresh AFFIRMATION + STATE.a2ml; resync the template validator - #37
Conversation
…lidator
Human receipt and machine state were both stale at 2026-07-21 -- they still
described ET-2 as open, months of work after it closed.
AFFIRMATION.adoc (the dated, signed receipt -- claims re-run at this SHA):
* axiom audit 12/12 -> 22/22
* NEW affirmed-ran: ET-2 CLOSED for the core calculus (soundness,
completeness, defEq_iff_nf, decEqNf/decEqSp, decDefEq; #print axioms ->
[propext, Quot.sound] only)
* NEW affirmed-ran: the eta extension is PARTIALLY landed (eta-long NfE/SpE
with neutrals only at star, DefEqE with a real eta rule, defEq_to_defEqE,
DecidableEq)
* NEW affirmed: ADR-0002 accepted -- ET-14 item (3) fixed as the parametric
L0Observation; ET-16 in the ledger narrowly
* "What we do NOT claim" rewritten so the new results cannot be over-read:
ET-2 is BETA-ONLY (eta excluded, ET-3 untouched); the eta extension is
NOT finished (normalizer open, four diagnosed defects, issue #32); and
ADR-0002 decides a DEFINITION, not a theorem -- it lets ET-14 be stated,
which is not progress toward proving it.
STATE.a2ml (machine-readable):
* completion 32 -> 46; Phase 2 65 -> 88 with the remaining 12% explained
* issues 30 and 32 added to blockers
* critical-next-actions rewritten: milestone 2 is done, so the next action is
the eta cluster, with the ATTACK ORDER recorded (adjSwp before adjWkv --
same rem/vs reshaping idiom, smaller instance; wkNfE_etaNe in parallel)
scripts/validate-template.sh: dropped npm-bun-blocker.yml and ts-blocker.yml
from REQUIRED_WORKFLOWS. PR #35 deliberately retired both under the Bun-first
runtime policy, but the validator still demanded them -- so the repo's own
template check contradicted its own ruling and exited 1. Now PASSES.
Also added the two missing SPDX headers the validator warned about
(Systemet.lean, scripts/invariant-path.sh) -- both pre-existing.
Verified at this SHA: cold rebuild 21 jobs; check-proofs (22/22 audit),
scan-dangerous, check-proof-status, check-root-shape, validate-template all
real exit 0.
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. Code Review ✅ ApprovedRefreshes AFFIRMATION and STATE.a2ml documentation to reflect closed ET-2 status and updated metrics, while resyncing the template validator to align with the Bun-first policy. No issues found.
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
Both the human receipt and the machine state were stale at 2026-07-21 — still describing ET-2 as open.
AFFIRMATION.adoc — claims re-run at this SHA: audit 12/12 → 22/22; ET-2 closed; η partially landed; ADR-0002 accepted. The do-not-claim section is rewritten so none of it can be over-read — ET-2 is β-only (η excluded, ET-3 untouched), the η extension is not finished (normalizer open, issue #32), and ADR-0002 decides a definition, not a theorem.
STATE.a2ml — completion 32 → 46, Phase 2 65 → 88 with the remaining 12% explained; issues #30/#32 added; next-actions rewritten with the η attack order (adjSwp before adjWkv — same reshaping idiom, smaller instance; wkNfE_etaNe in parallel).
validate-template.sh — dropped
npm-bun-blocker.yml/ts-blocker.ymlfrom required workflows. PR #35 deliberately retired both under the Bun-first policy, so the template check was contradicting your own ruling and exiting 1. Now passes. Plus two pre-existing missing SPDX headers.All gates real exit 0 at this SHA.