docs: Gate 1 adjacency refresh — cross-check 5 notes against current taxonomy#77
Merged
Merged
Conversation
7 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…-rot (#79) ## Summary Three independent bookkeeping items consolidated to avoid PR churn: 1. **CLAUDE.md "Current rung state (2026-05-20)"** — full session arc for the echo-types swarm (PRs #67-#72, #74-#77). §"Theory work — no proof assistant needed" is now essentially closed (Lane 2 BalancedTolerance is #78, awaiting review). Two patterns formalised (per-lemma Smoke pin for parameterised modules; `sandbox.excludedCommands` workaround for the agda positional-arg sandbox quirk). Plan for next Claude included. 2. **EchoAccess `Lift ⊤` carrier — design closure.** The post-#75 carrier-honesty work hit a structural wall on the owner-authorised existential design: `degrade-access` becomes uninhabitable because the access lattice tracks **decreasing** information as you climb, so degrading must drop info, never fabricate it. Conclusion: `Lift ⊤` IS the right honest carrier at the top of the lattice (same sense as `EchoGraded.forget = ⊤`). New `docs/echo-types/decisions/echo-access-trivial-carrier.adoc` captures the closure; `EchoAccess.agda` module header updated from "Deferred to follow-up" to "Resolved 2026-05-20" with the structural reasoning. 3. **Complete `≤a-⊔a-univ` baseline-rot** — 10 more wrong-RHS clauses in the same family as commit `a8ac211` (which fixed only some of the strict-inequality witnesses). Discovered by Agda 2.8.0 on a clean `.agdai` cache; previous "verified green" reports were spuriously passing because of stale incremental builds. Same diagnosis: when `c1 ⊔a c2 = c2` (strict `c1 < c2`), the universal property witness needs `c2≤c` shape (p2), not `c1≤c` shape (p1). Fixed clauses span the decidable/enum/feasible/infeasible rows. ## Test plan - [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda` exits 0 on Agda 2.8.0 - [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda` exits 0 on Agda 2.8.0 - [x] `--safe --without-K` invariants intact - [x] No postulates introduced - [x] No escape pragmas - [ ] CI Agda check passes - [ ] AsciiDoctor render of new decisions adoc (no asciidoctor in environment; hand-inspected against `decisions/no-2-cat.adoc` template) Refs CLAUDE.md "Rung-consolidation policy" §4 ("Update machine docs"). Does **not** close any issue. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…taxonomy Closes the roadmap.md § "Theory work" entry "Gate 1 adjacency refresh: the five existing adjacency notes predate the taxonomy." The five original notes (quotients, galois-connections, refinement-types, information-flow, provenance) were written 2026-04 against a five-axis taxonomy; the current taxonomy is eight numbered axes, with axes 2 (approximate, EchoApprox.agda) and 8 (information-theoretic vs computational access, EchoDecidable.agda + EchoAccess.agda + EchoCost.agda + EchoSearch.agda) landed 2026-04-27 → 2026-05-20. Per-note verdict: 5/5 REFINED, 0 STILL-VALID-as-stated, 0 RE-EVALUATE. Every distinctness claim survives the new taxonomy; every note benefits from being re-stated in terms of the now-numbered axes. Cross-cutting findings: * Axis 8 sharpens four of five notes (quotients, galois-connections, refinement-types, provenance gain a new sub-distinction once computational access is a separate axis). * The README's two-argument-families framing (truncation, 2-cell) is also refresh-eligible: cleanly axis-7/axis-1 vs axis-5, with provenance's multiplicity argument as its own family. * No content rewrites scheduled in this PR; coherence follow-ups (per-note one-liner cross-references, README refresh, gate-2-handoff axis-8 sub-test) listed in the closure note. This is a coherence pass: the notes are not invalidated by the post-2026-05 taxonomy, so no in-place edits to any adjacency note land here. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
802c1c5 to
e8675ab
Compare
6 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
…re (#93) ## 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 #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 #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 #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 * [x] Pure machine-readable data; no Agda touched * [x] `agda proofs/agda/All.agda` exit 0 * [x] `agda proofs/agda/Smoke.agda` exit 0 * [x] Append-only ADR discipline preserved (adr-001 through adr-006 unchanged; new ADRs at the end) * [x] 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](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
🔍 Hypatia Security ScanFindings: 10 issues detected
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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Coherence pass closing the
docs/echo-types/roadmap.md§ "Theory work" entry:The five original notes —
docs/adjacency/{quotients, galois-connections, refinement-types, information-flow, provenance}.adoc— were written 2026-04 against a five-axis taxonomy. The current taxonomy is eight numbered axes (axes 2 and 8 landed 2026-04-27 → 2026-05-20).Per-note verdict
quotients.adocgalois-connections.adocrefinement-types.adocinformation-flow.adocprovenance.adoc5/5 REFINED, 0 STILL-VALID-as-stated, 0 RE-EVALUATE. Every distinctness claim survives the new taxonomy; every note benefits from being re-stated in terms of the now-numbered axes.
Cross-cutting findings
Files
docs/echo-types/decisions/gate1-adjacency-refresh.adoc(closure note, perdecisions/no-2-cat.adoctemplate)docs/echo-types/roadmap.md— Theory-work entry status flipped to[refreshed — see decisions/gate1-adjacency-refresh.adoc]Refs
roadmap.md§ "Theory work" entry. Doc-only; no.agdachanges.Test plan
asciidoctorin this env — visual check on GitHub)git diff --stat: 2 files, no.agda🤖 Generated with Claude Code