docs(machine-readable): update STATE + META for F1/F3/earn-back closure

[hyperpolymath]

Summary

Brings .machine_readable/6a2/STATE.a2ml and META.a2ml in line
with the prose docs after this session's Pillar F earn-back closure
and §"Theory work" closing.

META.a2ml — three new ADRs (append-only)

No existing ADR is edited. Three appended after adr-006:

• adr-007 — F1 earn-back via monoid-graded iterated-residue
  construction. EchoGradedComonadF1.agda at (ℕ, +, 0) with
  Echo as grade-unit object, nested δ, all three comonad laws,
  D2-nontrivial separating witness. (PR F1 PASSED: gc-coassoc closed (earn-back gate, R-2026-05-18 follow-up) #86 merged 2026-05-20.)
• adr-008 — F3 earn-back via two non-isomorphic-grade-monoid
  instances of an abstract GradedComonadStructure interface. No
  ⊑-prop-equivalent field. nat-instance at commutative
  (ℕ, +, 0); list-instance at non-commutative (List Tag, ++, []).
  (PR F3 PASSED: GradedComonadStructure + two non-isomorphic-grade-monoid instances #88 open.)
• adr-009 — Retraction-discipline succeeded: the R-2026-05-18
  reframing converted into four earn-back gate passes (F4, F2, F1,
  F3); one retraction stays retracted (conservativity metatheorem,
  finding 5); none silently re-inflated.

Each ADR carries the strict scope qualifier — F1/F3 earn back claims
for a separate side-construction; EchoGraded itself remains a
thin-poset reindexing modality per R-2026-05-18, and paper.adoc /
types-abstract.adoc / conservativity.adoc are intentionally not
moved.

STATE.a2ml — next-actions pruned + two closure sections appended

Pruned: 3 of 5 April next-actions were stale and are resolved
in the prose:

• integration (apply 7-commit sequence) — done long ago
• t-3 (Gate-1 falsification test 3) — superseded by Gate 1
  adjacency refresh (decisions/gate1-adjacency-refresh.adoc, PR docs: Gate 1 adjacency refresh — cross-check 5 notes against current taxonomy #77)
• q2-4 (falsifier attempts) — absorbed by IntegrationAudit.agda
  EI-2 negative result; remaining attempts are bookkeeping

Remaining + added: q2-1 (echo-not-prop generalisation, still
high), q2-3 (RoleGraded as N5, still low), new
owner-gated-paper-update entry, new ordinal-track-path-1 entry
(in-flight in other session), and the original v0-2-recipe-extension
parked entry.

Two new closure sections at the end of STATE.a2ml:

• earn-back-summary — closure record for all four gates with
  module paths, claim wording, retraction-followup citations, and a
  forbidden-rebrandings list to prevent later mis-framing.
• theory-work-summary — closure record for §"Theory work — no
  proof assistant needed": axes fully mechanised list, ruled-out
  items, refreshed items, canonical examples cluster.

Test plan

• Pure machine-readable data; no Agda touched
• agda proofs/agda/All.agda exit 0
• agda proofs/agda/Smoke.agda exit 0
• Append-only ADR discipline preserved (adr-001 through adr-006
  unchanged; new ADRs at the end)
• No retracted claim moved; no earned-back claim overclaimed
• (owner) confirm a2ml schema validation if you run a validator
  against the standards/state-a2ml + meta-a2ml specs

Scope

Pure machine-readable data update. Disjoint from all currently-open
PRs (#88 F3, #90 partition-dec, #91 generic-codomain, #92 docs tidy).
paper.adoc / types-abstract.adoc / conservativity.adoc are
intentionally not touched.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 10 issues detected

Severity	Count
🔴 Critical	0
🟠 High	5
🟡 Medium	5

View findings

[
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Issue in secret-scanner.yml",
    "type": "missing_workflow",
    "file": "secret-scanner.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/cache@v4 needs attention",
    "type": "unpinned_action",
    "file": "agda.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "No dependabot.yml or renovate.json found in echo-types",
    "type": "DependencyUpdate",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "high",
    "remediation": "Add .github/dependabot.yml or renovate.json configuration.",
    "scorecard_check": "Dependency-Update-Tool"
  },
  {
    "reason": "Nominal-only SAST in echo-types: codeql.yml language matrix contains no language present in the repo and lacks `actions`, so CodeQL records zero results on every commit. Remediation: set the CodeQL matrix to `language: actions`.",
    "type": "StaticAnalysis",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Add CodeQL or equivalent SAST workflow.",
    "scorecard_check": "SAST"
  },
  {
    "reason": "1 workflow(s) with tag-pinned (not SHA-pinned) actions in echo-types",
    "type": "DependencyPinning",
    "file": "/home/runner/work/echo-types/echo-types",
    "action": "auto_fix",
    "rule_module": "scorecard",
    "severity": "medium",
    "remediation": "Pin GitHub Actions and Docker base images by SHA hash.",
    "scorecard_check": "Pinned-Dependencies"
  },
  {
    "reason": "Repository has 1 non-main remote branch(es). Policy: single main branch only.",
    "type": "GS007",
    "file": ".",
    "action": "delete_remote_branches",
    "rule_module": "git_state",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence