diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 37c4a83..50a119d 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -25,8 +25,8 @@ All commits require Developer Certificate of Origin sign-off: 2. CHANGELOG.md updated under `[Unreleased]`. -3. `.machine_readable/6a2/STATE.a2ml` `last-updated` bumped if the - change is significant. +3. Significant changes are recorded in CHANGELOG.md (item 2). The + former `STATE.a2ml` record was retired on 2026-09-30. 4. **Banned constructs.** No new `believe_me`, `assert_total`, `postulate`, `sorry`, `Admitted`, `unsafeCoerce`, or `Obj.magic` @@ -46,14 +46,15 @@ All commits require Developer Certificate of Origin sign-off: outside `proofs/agda/` (no current non-guarded path exists; widening the guardrail’s allowlist requires a separate design discussion). -6. **EI-2 discipline.** Per `.machine_readable/6a2/STATE.a2ml` `§` - `ei-2`, the integration-recipe distinctness investigation is +6. **EI-2 discipline.** Per the retired state record, frozen at + + (section `ei-2`), the integration-recipe distinctness investigation is *terminated negatively* and is not to be reopened. If a change - touches that territory, read `STATE.a2ml` `§` `ei-2` first; the + touches that territory, read that record's `ei-2` section first; the `forbidden-rebrandings` list is a hard fence. 7. **Naming traps.** `ModeGraded` (with trailing `d`) is canonical; - never `ModeGrade`. See `STATE.a2ml` `§` `naming-traps`. + never `ModeGrade`. See the frozen record's `naming-traps` section. ## Reviews diff --git a/.machine_readable/6a2/0-AI-MANIFEST.a2ml b/.machine_readable/6a2/0-AI-MANIFEST.a2ml deleted file mode 100644 index cede8a9..0000000 --- a/.machine_readable/6a2/0-AI-MANIFEST.a2ml +++ /dev/null @@ -1,22 +0,0 @@ -# AI Manifest for 6a2 Directory - -## Purpose - -This manifest declares the AI-assistant context for the 6a2 machine-readable metadata directory. - -## Canonical Locations - -The 6 core A2ML files MUST exist in this directory: -1. AGENTIC.a2ml -2. ECOSYSTEM.a2ml -3. META.a2ml -4. NEUROSYM.a2ml -5. PLAYBOOK.a2ml -6. STATE.a2ml - -## Invariants - -- No duplicate files in root directory -- Single source of truth: this directory is authoritative -- No stale metadata - diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/6a2/AGENTIC.a2ml deleted file mode 100644 index 1b6689a..0000000 --- a/.machine_readable/6a2/AGENTIC.a2ml +++ /dev/null @@ -1,294 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# -# AGENTIC.a2ml — gating rules for echo-types operational requests -# -# Format: TOML-A2ML (estate convention; `#` comments, [section], key = "value") -# -# Provenance: converted 2026-06-12 from the Guile S-expression body -# `(define-module (echo-types agentic) ...)` that previously occupied -# this file. Faithful translation of all seven gate rules, the redo -# traps, escalation policy, and pre/post-action checks. File-path -# citations were updated from the S-expr-era names (STATE.scm / META.scm -# in audit-output/) to the canonical .machine_readable/6a2/*.a2ml -# locations; rule content is unchanged. The original S-expr schema -# reference was: -# https://github.com/hyperpolymath/standards/blob/main/agentic-a2ml/spec/abnf/agentic.abnf -# -# Pipeline position (per playbook spec § 8.1): -# META validate → AGENTIC gate → NEUROSYM discharge → -# PLAYBOOK execute → STATE update → ECOSYSTEM check -# -# Purpose: gate operational requests against the standing decisions in -# META.a2ml and STATE.a2ml so a future session does not re-investigate -# closed questions, redo superseded work, or violate forbidden -# rebrandings. - -[metadata] -project = "echo-types" -last-updated = "2026-06-12" - -# ============================================================ -# Entropy budget -# ============================================================ -# The entropy budget is a coarse measure of "how much exploration should -# this session do before consulting STATE/META?". Low budget = consult -# first; high budget = explore freely. -# -# Post-EI-2-termination, the budget for EI-2-adjacent investigations is -# essentially zero — the question is closed. - -[entropy-budget] -session-default = "moderate" - -[entropy-budget.ei-2-adjacent] -level = "zero" -rationale = "EI-2 is terminated. Any reopen attempt triggers the do-not-reopen gate; exploration here violates the standing decision." - -[entropy-budget.gate-1-falsification-tests] -level = "moderate" -rationale = "T3 (informativeness collapse) is unstubbed and worth attempting; T1, T2 are closed by Sophisticated submodules." - -[entropy-budget.gate-2-falsifier-attempts] -level = "moderate" -rationale = "Each surviving nominee has an unattempted falsifier; explore freely." - -[entropy-budget.recipe-extension-v0-2] -level = "high" -rationale = "Genuinely new work; not constrained by EI-2's negative finding because it is a different question." - -# ============================================================ -# Gate rules (pre-execution checks) -# ============================================================ - -[[gate-rules]] -id = "g-001" -name = "do-not-reopen-EI-2" -severity = "critical" -trigger-any-of = [ - "user request to 'investigate the recipe further'", - "user request to 'try a different family choice for ModeGrade'", - "user request to 'see if Choreo × Choreo works with shared state'", - "user request to 'narrow gate-1 with NLO precondition'", - "user request that matches any forbidden-rebrandings entry in STATE.a2ml", - "context implies treating EI-2 as still open", -] -action = "refuse-with-citation" -citation = [ - ".machine_readable/6a2/STATE.a2ml > terminated-questions > EI-2", - ".machine_readable/6a2/META.a2ml > adr-002 (Drop READING 2 as the EI-2 closure framing)", - ".machine_readable/6a2/META.a2ml > adr-004 (Recipe extension scope: v0.2+, not v0.1.x)", -] -escape-hatch = "User can override by explicitly stating 'I'm reopening EI-2 with [specific structural justification not in forbidden-rebrandings]'. Trigger only on rare, well-justified reopens." - -[[gate-rules]] -id = "g-002" -name = "do-not-redo-superseded-readings" -severity = "high" -trigger-any-of = [ - "user request to draft READING 1 patches", - "user request to draft READING 2 patches", - "user request to compare candidate readings for EI-2 closure", -] -action = "refuse-with-citation" -citation = [ - ".machine_readable/6a2/STATE.a2ml > standing-decisions > sd-006", - "docs/EI2_READING1_PATCHES.adoc > SUPERSEDED banner", - "docs/EI2_READING2_PATCHES.adoc > SUPERSEDED banner", - "docs/EI2_READINGS_COMPARISON.adoc > SUPERSEDED notice", -] -escape-hatch = "None — these readings are factually wrong per RoleRole.agda's findings." - -[[gate-rules]] -id = "g-003" -name = "do-not-create-ModeGrade-without-trailing-d" -severity = "medium" -trigger-any-of = [ - "creating proofs/agda/characteristic/ModeGrade.agda (without trailing 'd')", -] -action = "redirect-to-canonical" -redirect = "Use proofs/agda/characteristic/ModeGraded.agda (canonical, prior-session). The non-trailing-d variant was a duplicate created and removed in the capturing session." -citation = [".machine_readable/6a2/STATE.a2ml > do-not-redo entry on ModeGrade vs ModeGraded"] - -[[gate-rules]] -id = "g-004" -name = "do-not-attempt-full-2D-iff-recipe-non-triviality-theorem" -severity = "high" -trigger-any-of = [ - "user request to formalise the full 2D iff theorem", - "user request to prove recipe-non-triviality as a generic theorem", -] -action = "redirect-to-PATH-B" -redirect = "Documented as not formalisable in safe Agda without postulates (decidable equality, F-collapses axioms, extensionality). PATH B accepted partial formalisation. See RecipeTheorem.agda header." -citation = [".machine_readable/6a2/META.a2ml > adr-003 (Accept partial formalisation (PATH B) for EI-2 closure)"] -escape-hatch = "If the user has identified specific postulates they're willing to admit, this can proceed under explicit acknowledgment of the postulates." - -[[gate-rules]] -id = "g-005" -name = "do-not-rebrand-recipe-as-distinctness-locus" -severity = "critical" -trigger-any-of = [ - "documentation that says recipe carries gate-1's distinctness load", - "documentation that says five axes simultaneously is the distinctness claim", - "any formulation that puts the integration argument back into the gate-1 distinctness story", -] -action = "refuse-with-citation" -citation = [ - ".machine_readable/6a2/STATE.a2ml > forbidden-rebrandings", - ".machine_readable/6a2/STATE.a2ml > standing-decisions > sd-001", - ".machine_readable/6a2/STATE.a2ml > standing-decisions > sd-002", - ".machine_readable/6a2/META.a2ml > adr-001", -] -escape-hatch = "None — this is a load-bearing standing decision." - -[[gate-rules]] -id = "g-006" -name = "do-not-modify-superseded-files-content" -severity = "medium" -trigger-any-of = [ - "editing docs/EI2_READING1_PATCHES.adoc body", - "editing docs/EI2_READING2_PATCHES.adoc body", - "editing docs/EI2_READINGS_COMPARISON.adoc body", -] -action = "redirect-to-banner-update" -redirect = "These files are historical record only. Do not modify their body content. If new context emerges that would change the SUPERSEDED reasoning, update the banner at the top of the file but leave the body intact." -citation = [".machine_readable/6a2/STATE.a2ml > standing-decisions > sd-006"] - -[[gate-rules]] -id = "g-007" -name = "read-INDEX-first-on-session-entry" -severity = "medium" -trigger-any-of = [ - "session entering .machine_readable/6a2/ for the first time", - "session asking 'what's the state of echo-types EI-2'", - "session asking 'what's been done'", - "user requesting summary of work", -] -action = "enforce-reading-order" -reading-order = [ - "INDEX.adoc (repo root)", - ".machine_readable/6a2/STATE.a2ml", - ".machine_readable/6a2/META.a2ml", - ".machine_readable/6a2/AGENTIC.a2ml (this file, for further gating context)", - ".machine_readable/6a2/PLAYBOOK.a2ml (for procedure to follow)", - ".machine_readable/6a2/ECOSYSTEM.a2ml (only if cross-repo context needed)", - ".machine_readable/6a2/NEUROSYM.a2ml (only if formal-evidence context needed)", -] -rationale = "Reading INDEX.adoc + STATE + META covers ~95% of context for any operational request without re-deriving anything. Skipping these is the most common redo trap." - -# ============================================================ -# Redo traps (patterns that have caused or threatened to cause the same -# work to be done twice) -# ============================================================ - -[[redo-traps]] -trap = "STATE-format-bikeshed" -description = """ -Historically two STATE surfaces existed (a canonical STATE.scm S-expr -body and a short-form companion). Resolved by the 2026-04-30 .scm→.a2ml -migration and finally by the 2026-06-12 S-expr→TOML-A2ML conversion: -.machine_readable/6a2/STATE.a2ml is the single canonical STATE. Do not -reintroduce a parallel STATE surface or convert formats ad hoc. -""" -mitigation = "Single canonical file; format changes only via estate-wide standardization waves." - -[[redo-traps]] -trap = "EI-2-reopening-under-new-framing" -description = """ -Multiple framings exist that effectively reopen EI-2: 'try a different -family', 'NLO is sufficient with the right reading', 'Mode×Grade was -just a bad pair'. All are listed as forbidden-rebrandings. -""" -mitigation = "Gate G-001 + G-005 reject these. Citation cascade points to RoleRole.agda's findings, the seven-data-point table, and adr-001..adr-004." - -[[redo-traps]] -trap = "Recipe-extension-as-EI-2-continuation" -description = """ -The v0.2+ recipe extension work is genuinely interesting and -superficially looks like 'finishing EI-2'. It is not. Treating it as -EI-2 continuation reopens a closed question and confuses scope. -""" -mitigation = "Gate G-001 catches this; adr-004 explicitly parks recipe extension as v0.2+ work, separate question (e.g., EI-3) when filed." - -[[redo-traps]] -trap = "Documentation-cascade-incompleteness" -description = """ -EI-2's narrowing applies in five doc locations. Updating only some of -them creates inconsistency and invites a future session to 'fix' the -unupdated ones, doing the work again. -""" -mitigation = "STATE.a2ml cascade-applied lists exactly the five locations. Verify all five are at the post-EI-2 narrowing before declaring any related task done." - -[[redo-traps]] -trap = "Cite-from-memory-instead-of-from-files" -description = """ -Future sessions might cite the EI-2 finding from memory or from a -summary, getting nuances wrong (e.g., saying NLO is sufficient when it's -only necessary). The authoritative source is the seven data-point table -in STATE.a2ml or EI2_REPORT.adoc. -""" -mitigation = "Gate G-005 + G-007 redirect to the authoritative files. AGENTIC gate rules carry citation lists pointing back to the canonical record." - -# ============================================================ -# Escalation -# ============================================================ - -[escalation.on-gate-violation] -severity-critical = "Refuse the action. Cite the rule and the standing decision. Do not bypass." -severity-high = "Refuse by default. If user provides explicit override with structural justification, allow with full citation in the response." -severity-medium = "Redirect to the canonical alternative. Do not just refuse; offer the right action." -severity-low = "Note the gate, proceed with caveat in the response." - -[escalation.on-gate-uncertainty] -when-rule-fits-loosely = "Default to refusal + ask for clarification. Better to ask than to redo." -when-no-rule-fits = "Proceed; log the case as a candidate new gate rule for STATE next-actions if the situation recurs." - -# ============================================================ -# Pre-action checks (run before executing any non-trivial request) -# ============================================================ - -[[pre-action-checks]] -name = "STATE-and-META-fresh-in-context" -assertion = "Have STATE.a2ml and META.a2ml been read in this session?" -on-fail = "Read them before proceeding. Reading them is cheap; not reading them is the redo trap." - -[[pre-action-checks]] -name = "no-forbidden-rebranding" -assertion = "Does the proposed action match any STATE forbidden-rebrandings entry?" -on-fail = "Refuse via Gate G-005." - -[[pre-action-checks]] -name = "not-EI-2-reopen" -assertion = "Does the proposed action implicitly or explicitly reopen EI-2?" -on-fail = "Refuse via Gate G-001." - -[[pre-action-checks]] -name = "not-superseded-document-rework" -assertion = "Does the proposed action edit the body of a superseded document?" -on-fail = "Redirect via Gate G-006." - -# ============================================================ -# Post-action checks (run after executing non-trivial requests) -# ============================================================ - -[[post-action-checks]] -name = "STATE-update-needed" -assertion = "Did this action add a new artefact, close a question, or change a decision? If yes, STATE.a2ml must be updated." -on-pass = "STATE.a2ml fresh." -on-fail = "Update STATE.a2ml before declaring task done." - -[[post-action-checks]] -name = "META-update-needed" -assertion = "Did this action establish a new architectural decision? If yes, an ADR entry in META.a2ml is required." -on-pass = "META.a2ml fresh." -on-fail = "Add adr-NNN entry; bump META.a2ml." - -[[post-action-checks]] -name = "cascade-still-consistent" -assertion = "Did this action edit any of the five cascade-applied locations in STATE.a2ml? If so, do all five still agree?" -on-pass = "Cascade consistent." -on-fail = "Update remaining cascade locations before declaring done." - -# ============================================================ -# END OF AGENTIC -# ============================================================ diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml deleted file mode 100644 index 730f3f3..0000000 --- a/.machine_readable/6a2/ECOSYSTEM.a2ml +++ /dev/null @@ -1,192 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# -# ECOSYSTEM.a2ml — echo-types relationships across the hyperpolymath -# repository constellation -# -# Format: TOML-A2ML (estate convention; `#` comments, [section], key = "value") -# -# Provenance: converted 2026-06-12 from the Guile S-expression body -# `(define-module (echo-types ecosystem) ...)` that previously occupied -# this file. Faithful translation; stale references to the .scm-era file -# names and the pre-estate layout were updated at conversion time (noted -# inline). The original S-expr schema reference was: -# https://github.com/hyperpolymath/standards/blob/main/ecosystem-a2ml/spec/abnf/ecosystem.abnf -# -# Purpose: record cross-repo dependencies and conventions so a future -# session understands echo-types' position in the constellation without -# re-deriving it. - -[metadata] -project = "echo-types" -last-updated = "2026-06-12" - -# ============================================================ -# Constellation membership -# ============================================================ - -[constellation-membership] -primary-constellation = "governance" -constellation-rationale = """ -echo-types is a formal-verification library but its docs are governed by -RSR 2026 / 6SCM Architecture, placing it under the governance -constellation for operational purposes. -""" - -[constellation-membership.other-constellations-touched] -languages = "Imports from agda-stdlib; conceptual proximity to formal-methods work in nextgen-languages." -research = "Theoretical artefact; downstream consumer of HoTT and category-theoretic concepts." - -# ============================================================ -# Schema dependencies (other hyperpolymath repos echo-types relies on) -# ============================================================ - -[[schema-dependencies]] -repo = "https://github.com/hyperpolymath/standards" -subpath = "a2ml/SPEC-v1.0.adoc" -consumes-as = "a2ml surface markup spec (Djot-like)" -consumed-by = "documentation files (.adoc)" -status = "current" - -[[schema-dependencies]] -repo = "https://github.com/hyperpolymath/standards" -subpath = "meta-a2ml/spec/abnf/meta.abnf" -consumes-as = "ABNF metalanguage that governed the S-expr-era *-a2ml types" -consumed-by = ".machine_readable/6a2/{META,STATE,ECOSYSTEM,AGENTIC,NEUROSYM,PLAYBOOK}.a2ml (S-expr bodies until 2026-06-12; now TOML-A2ML per estate convention)" -status = "historical" # refreshed 2026-06-12: the 6a2 bodies are TOML-A2ML now - -[[schema-dependencies]] -repo = "https://github.com/hyperpolymath/standards" -subpath = "playbook-a2ml/spec/PLAYBOOK-FORMAT-SPEC.adoc" -consumes-as = "Concrete shape exemplar for the S-expr-era module-form files" -consumed-by = "6a2 files (S-expr era); retained as historical shape reference" -status = "historical" # refreshed 2026-06-12, same reason as above - -[[schema-dependencies]] -repo = "https://github.com/hyperpolymath/k9-svc" -subpath = "SPEC.adoc" -consumes-as = "K9 self-validating component format (Nickel, leash security model)" -consumed-by = ".machine_readable/self-validating/ (template set + examples, added at the 2026-06-12 governance checkpoint)" -status = "current" -# Pre-2026-06-12 this entry was status = "unread" with a note that no k9 -# descriptors existed in echo-types yet; the self-validating/ set now -# exists, so the entry is filled in as the original note required. - -[[schema-dependencies]] -repo = "https://github.com/hyperpolymath/rhodium-standard-repositories" -subpath = "RSR-2026/" -consumes-as = "Repository compliance standard" -consumed-by = "echo-types repository structure conventions (e.g., docs/ layout, MAINTAINERS.adoc, CODE_OF_CONDUCT.md, GOVERNANCE.adoc)" -status = "current" - -# ============================================================ -# Sibling projects (same constellation or close conceptual relation) -# ============================================================ - -[[sibling-projects]] -name = "echidna" -relation = "Conceptual sibling — neurosymbolic theorem-proving platform; echo-types is a single-domain formal verification library, echidna is the broader prover ecosystem." -cross-references = "none-yet" - -[[sibling-projects]] -name = "affinescript" -relation = "Languages-constellation sibling — affine-typed WASM language. Conceptually downstream of echo-types' formal-loss reasoning if cross-disciplinary tie-ins are pursued." -cross-references = "none-yet" - -[[sibling-projects]] -name = "my-lang" -relation = "Conceptual neighbour — Me/Solo/Duet/Ensemble dialect family. Could consume echo-types-style fiber reasoning in a future axis but no current dependency." -cross-references = "none-yet" - -[[sibling-projects]] -name = "manifesto" -relation = "Constellation overview document referencing all hyperpolymath projects. echo-types is one of 275+ governed by RSR 2026." -cross-references = "Listed under Research / Formal Verification." - -# Cross-repo bridge consumers recorded since the original S-expr entry -# (see docs/echo-types/cross-repo-bridge-status.md for the live ledger): -# ephapax (L3 NARROW bridge, PRs #161-#163), EchoTypes.jl (finite-domain -# Julia companion), eclexia (thermodynamic consumer bridge, PR #180), -# Valence Shell / Ochránce (exploratory downstream consumer, PR #177), -# arghda-core (extracted to standalone repo, PR #160). - -# ============================================================ -# Cross-repo conventions echo-types follows -# ============================================================ - -[[cross-repo-conventions]] -convention = "Forge workflow: GitHub canonical, GitLab and Codeberg as mirrors" -source = "Standing decision sd-003 in STATE.a2ml" -artefacts = [".github/workflows/mirror.yml", "MIRROR_SETUP.adoc"] - -[[cross-repo-conventions]] -convention = "License: MPL-2.0 for code; CC-BY-4.0 for prose docs" -source = "SPDX header pattern (PR #150 normalization); constellation default; LICENSE + LICENSE-docs at root" -artefacts = ["LICENSE", "LICENSE-docs", "SPDX headers in all machine-readable files"] -# Refreshed 2026-06-12: the S-expr entry referenced a conditional -# LICENSE-PMPL-1.0.txt; the repo migrated to MPL-2.0 (PR #115) with -# prose under CC-BY-4.0 (PR #150). - -[[cross-repo-conventions]] -convention = "Cross-platform builds: Linux primary, Windows secondary" -source = "Standing decision sd-004 in STATE.a2ml" -artefacts = [".gitattributes"] - -[[cross-repo-conventions]] -convention = "Documentation: AsciiDoc, not Markdown" -source = "User preference (avoid Python-adjacent ecosystems where possible; AsciiDoc preferred over Markdown for technical docs)" -note = "README.md is the exception per GitHub default-render convention; it is the canonical README after the 2026-06-12 dedup (readme.adoc and EXPLAINME.adoc are pointers). docs/ is predominantly AsciiDoc." - -[[cross-repo-conventions]] -convention = "Configuration: Nickel/CUE/Dhall preferred over YAML" -source = "User standing preference" -note = "echo-types uses YAML only for GitHub Actions (no choice); the self-validating/ k9 set is Nickel." - -[[cross-repo-conventions]] -convention = "Containers: Podman > Docker" -source = "User preference" -note = "Containerfile + stapeln.toml at root are Podman-first; no Dockerfile." - -[[cross-repo-conventions]] -convention = "justfile over Makefile" -source = "User standing preference" -note = "Root Justfile is the primary command runner (build-echo / build-tests / per-bridge test recipes); .machine_readable/contractiles/Justfile is the estate-supplied governance copy." -# Refreshed 2026-06-12: the S-expr entry predated the root Justfile and -# claimed neither justfile nor Makefile existed; contradicted by reality. - -# ============================================================ -# Integrity checks (cross-file invariants ECOSYSTEM enforces) -# ============================================================ - -[[integrity-checks]] -check = "STATE and META referenced ADRs must exist" -assertion = "Every standing-decision sd-NNN in STATE.a2ml should have a corresponding adr-NNN in META.a2ml or a clear rationale embedded." -current-status = "pass" -note = "sd-001..sd-006 in STATE.a2ml align with adr-001..adr-006 in META.a2ml (adr-007..adr-011 extend beyond the sd list with their own rationale)." - -[[integrity-checks]] -check = "Forbidden rebrandings list is non-empty post-EI-2" -assertion = "STATE forbidden-rebrandings must contain at least the six EI-2-related entries." -current-status = "pass" - -[[integrity-checks]] -check = "do-not-redo register coverage" -assertion = "Every artefact in artefacts.agda-characteristic-lane must appear either in cascade-applied or in do-not-redo, or be flagged as 'still active work'." -current-status = "pass-by-inspection" -note = "All EI-2 phase files are referenced in either artefacts list or via do-not-redo entries." - -[[integrity-checks]] -check = "Schema dependency completeness" -assertion = "All 6a2 files must carry their format + provenance reference in their header comment." -current-status = "pass" -note = "All six 6a2 .a2ml files carry TOML-A2ML format + S-expr-conversion provenance headers (2026-06-12)." - -[[integrity-checks]] -check = "Reading order alignment" -assertion = "INDEX.adoc reading order must be consistent with the 6a2 headers and INDEX.adoc itself." -current-status = "pass" -verification = "Cross-checked at last update." - -# ============================================================ -# END OF ECOSYSTEM -# ============================================================ diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml deleted file mode 100644 index e387253..0000000 --- a/.machine_readable/6a2/META.a2ml +++ /dev/null @@ -1,427 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# -# META.a2ml — echo-types architecture decisions -# -# Format: TOML-A2ML (estate convention; `#` comments, [section], key = "value") -# -# Provenance: converted 2026-06-12 from the Guile S-expression body -# `(define-module (echo-types meta) ...)` that previously occupied this -# file (S-expr last-updated: 2026-06-05). Faithful translation: all -# eleven ADRs, the development practices, and the design rationale are -# preserved in full. The original S-expr schema reference was: -# https://github.com/hyperpolymath/standards/blob/main/meta-a2ml/spec/abnf/meta.abnf - -[metadata] -project = "echo-types" -last-updated = "2026-06-21" - -# ============================================================ -# Architecture Decision Records -# ============================================================ - -[[architecture-decisions]] -id = "adr-001" -title = "Distinctness load rests on truncation + 2-cell arguments" -status = "accepted" -date = "2026-04-29" -context = """ -EI-2 investigation across seven data points found the integration recipe -does not carry substantive simultaneous cross-axis content. The -non-loss-only criterion is necessary but not sufficient; even -Choreo × Choreo (the only available NLO self-pairing) degenerates to -coordinate-product commutation. -""" -decision = """ -Gate-1's distinctness claim narrows: the recipe is organising vocabulary; -the load-bearing distinctness arguments are (1) truncation (echo-not-prop -family) and (2) 2-cell (Σ-over-preimages-shaped natural 2-cells in -neighbour frameworks). -""" -consequences = "Five-document cascade: gate-1, gate-2-handoff, roadmap-gates, adjacency README, top-level README. Recipe extension parked for v0.2+." -supersedes = "none" - -[[architecture-decisions]] -id = "adr-002" -title = "Drop READING 2 as the EI-2 closure framing" -status = "accepted" -date = "2026-04-29" -context = """ -Two candidate readings for EI-2 closure were drafted (READING 1: weaken -gate-1; READING 2: NLO-as-recipe-precondition). The prior session's -RoleRole.agda finding established that NLO is necessary but not -sufficient, refuting READING 2 as drafted. -""" -decision = """ -Adopt the stronger-negative reading: distinctness rerouted to truncation -+ 2-cell, recipe explicitly removed from distinctness load. Both -originally-drafted reading patches are kept as historical record with -SUPERSEDED banners. -""" -consequences = "EI-2 terminates negatively via PATH B (partial formalisation accepted as sufficient). Three legacy doc files are SUPERSEDED-banner'd, not deleted." -supersedes = "none" - -[[architecture-decisions]] -id = "adr-003" -title = "Accept partial formalisation (PATH B) for EI-2 closure" -status = "accepted" -date = "2026-04-29" -context = """ -The full 2D iff theorem (recipe-non-triviality ↔ NLO criterion) is not -formalisable in safe Agda without postulates: decidable equality on -decoration types, F-collapses axioms, extensionality on cell actions. -""" -decision = """ -Accept the per-axis halves (proved in RecipeTheorem.agda) plus the -concrete construction halves (proved in RecipeNonTriviality.agda) plus -the seven empirical data points as sufficient evidence for termination. -Document the formal generic theorem as future work, not as a blocker for -EI-2 closure. -""" -consequences = """ -EI-2 closes; the recipe-non-triviality theorem in its full generic form -is parked. Gate-1's distinctness narrowing does not depend on the parked -theorem since the negative finding removes the recipe from the -distinctness load entirely. -""" -supersedes = "none" - -[[architecture-decisions]] -id = "adr-004" -title = "Recipe extension scope: v0.2+, not v0.1.x" -status = "accepted" -date = "2026-04-29" -context = """ -The positive-termination route from EI-2 — extending the recipe to allow -coupled state across axes or multiple live positions per axis — is -conceptually distinct from the EI-2 question (does the existing recipe -with the existing five axes carry substantive content?). -""" -decision = """ -Park recipe extension as a separate v0.2+ work item. Do not file it as an -EI-2 reopening or as unfinished EI-2 business. When v0.2 work begins, -file as a new question (e.g., EI-3). -""" -consequences = "EI-2 stays terminated. Future investigators cannot reopen it under the framing 'EI-2 wasn't really finished, the recipe just needs extending'." -supersedes = "none" - -[[architecture-decisions]] -id = "adr-005" -title = "Forge workflow: GitHub canonical, mirror outward" -status = "accepted" -date = "2026-04-28" -context = """ -User has a static stylistic preference for GitLab > GitHub but the actual -git workflow has GitHub as canonical with hub-and-spoke mirroring -outward. The static preference does not apply to git operations -specifically. -""" -decision = """ -echo-types canonical at github.com/hyperpolymath/echo-types; mirror to -GitLab and Codeberg via .github/workflows/mirror.yml. Tokens configured -per MIRROR_SETUP.adoc; missing-token cases silently skip rather than fail. -""" -consequences = "Hub-and-spoke pattern; PRs and Issues live on GitHub; mirrors are read-only." -supersedes = "none" - -[[architecture-decisions]] -id = "adr-006" -title = "Cross-platform builds: Linux primary, Windows secondary" -status = "accepted" -date = "2026-04-28" -context = "User works across two machines: Fedora Kinoite (primary, Nushell) and a Windows machine for travel." -decision = """ -Build instructions are path-agnostic; line endings normalised via -.gitattributes (LF for Agda/AsciiDoc/YAML, .agdai marked binary). -Cross-platform considerations apply throughout. -""" -consequences = "Path-agnostic build instructions are required, not optional, for any new tooling." -supersedes = "none" - -[[architecture-decisions]] -id = "adr-007" -title = "F1 earn-back via monoid-graded iterated-residue construction" -status = "accepted" -date = "2026-05-20" -context = """ -R-2026-05-18 retracted the graded-comonad claim about EchoGraded — the -structure was a thin-poset reindexing with no nested family, no monoid -multiplication, no genuine δ. Pillar F gate F1 -(docs/echo-types/earn-back-plan.adoc §F1) asked whether ANY genuine -graded comonad with Echo as the grade-unit object could be mechanised -under --safe --without-K with zero postulates. -""" -decision = """ -The candidate construction passes: proofs/agda/EchoGradedComonadF1.agda -ships a monoid-graded iterated-residue comonad at the grade monoid -(ℕ, +, 0) with D 0 A = A; D (suc r) A = R (D r A) where R X = X × Bool -(an informative residue layer, not ⊤). All three graded-comonad laws -(gc-counit-l, gc-counit-r, gc-coassoc) typecheck under --safe --without-K -with zero postulates; gc-coassoc closes via the predicted -δ-naturality-over-R factoring (δ-suc + subst-D-suc). The separating -witness D2-nontrivial certifies D r is not collapsing to ⊤ / a prop. -""" -consequences = """ -F1 PASSED; the graded-comonad claim is earned back FOR THIS WITNESS ONLY. -EchoGraded itself remains a thin-poset reindexing modality per -R-2026-05-18 — F1 enters as an *additional* mechanised contribution -beside EchoGraded, not as a reinstatement of it. Paper title and central -thesis (Echo as a reindexing modality) stand unchanged. Unblocks F3 -(independent second comonad model). Retraction follow-up F-2026-05-20a -appended to docs/retractions.adoc. -""" -supersedes = "none" - -[[architecture-decisions]] -id = "adr-008" -title = "F3 earn-back via two non-isomorphic-grade-monoid instances of an abstract interface" -status = "accepted" -date = "2026-05-20" -context = """ -F1 (adr-007) earned back the existence of a graded comonad with Echo as -grade-unit object. Gate F3 (docs/echo-types/earn-back-plan.adoc §F3) -asked whether the construction is genuinely model-independent — -instantiable at non-isomorphic grade monoids without a single hypothesis -(no ⊑-prop-equivalent field) baking in the result. -""" -decision = """ -EchoGradedComonadInterface.GradedComonadStructure is an abstract record -packaging the F1 signature (grade monoid + monoid laws + graded functor -+ functor laws + counit + nested δ + the three comonad laws stated -against subst along the monoid's propositional identities). The record -carries NO ⊑-prop-equivalent field — only structure, monoid laws, and -comonad laws. Two non-isomorphic-grade-monoid instances inhabit it: -EchoGradedComonadInstance1.nat-instance at the commutative monoid -(ℕ, +, 0); EchoGradedComonadInstance2.list-instance at the -non-commutative free monoid (List Tag, ++, []) over a two-element Tag -with per-element residue layers R smol A = A × Bool and R big A = A × ℕ. -Non-isomorphism is constructively witnessed by tag-list-non-commutative. -""" -consequences = """ -F3 PASSED; the two-models claim is earned back FOR THE F1-STYLE -GRADED-COMONAD WITNESS. It does NOT reinstate the older -EchoRelModel/GCLaws two-models claim retracted at R-2026-05-18 finding 3 -— that situation (same grade poset, ⊑-prop baked in as a field, -rel-model = set-model × ⊤, agreement by refl) is unchanged. The two -earn-backs are about different abstract interfaces and are not -interconvertible. Retraction follow-up F-2026-05-20b appended to -docs/retractions.adoc. Pillar F earn-back programme now CLOSED: -F4 + F2 (2026-05-18), F1 + F3 (2026-05-20). -""" -supersedes = "none" - -[[architecture-decisions]] -id = "adr-009" -title = "Retraction-discipline succeeded: R-2026-05-18 reframing converted into four earn-back gate passes" -status = "accepted" -date = "2026-05-20" -context = """ -R-2026-05-18 retracted five claims and reframed the project around what -the Agda actually shows (thin-poset reindexing modality, not graded -comonad; pointwise mediator, not terminal cone; carrier-parametricity, -not model-independence; postulate-free build as evidence, not -conservativity metatheorem; no funext anywhere, not 'quarantined'). The -earn-back plan in docs/echo-types/earn-back-plan.adoc was the falsifiable -program for converting the retracted claims back into theorems — or -confirming, on the project's own gate discipline, that they cannot be -earned at their original strength. -""" -decision = """ -All four gates have now passed at the strictly-bounded strength the -earn-back plan asked for: F4 (terminal-cone UP as a function of an -explicit funext parameter, never a postulate); F2 (genuine second model -of the bare Echo functor on a non-graph StepND relation); F1 (genuine -graded comonad on iterated-residue carrier with Echo as grade-unit -object); F3 (the F1 construction is instantiable at non-isomorphic grade -monoids). Each is exactly as strong as the gate specified; nothing is -overclaimed. The conservativity metatheorem retraction (R-2026-05-18 -finding 5) stays retracted with no gate attempting to earn it back — -that one was a meta-statement over all propositions, not discharged by -typechecking. The 'not two models for EchoGraded/GCLaws' finding 3 also -stays retracted; the F3 earn-back is about the different F1 interface. -""" -consequences = """ -The retraction discipline is validated AS A METHODOLOGY: a retraction is -not a failure but the mechanism by which claims become falsifiable. Four -of five retracted claims were earned back at honest strength, one stays -retracted, none was silently re-inflated. paper.adoc / types-abstract.adoc -/ conservativity.adoc are NOT moved by this ADR — those documents are -about EchoGraded's thin-poset structure, which the F1+F3 -side-construction does not change. Whether to add a bounded 'new -contribution' paragraph is owner-gated. -""" -supersedes = "none" - -[[architecture-decisions]] -id = "adr-010" -title = "Ordinal-track well-foundedness via rank-embedding transport" -status = "accepted" -date = "2026-05-30" -context = """ -Lane 3 (Buchholz/Ordinal) needed well-foundedness of the rank-mono union -relation _<ᵇᵘ_ (= _<ᵇ¹_ ⊎ _<ᵇ⁺²_) under the WfCNF restriction. Proving -WellFounded directly on a Buchholz term relation is hard; the unbudgeted -global WF for the unrestricted surface route remains genuinely out of -reach under --safe --without-K. -""" -decision = """ -Derive WellFounded _<ᵇᵘ_ by TRANSPORTING well-foundedness along the rank -embedding rank-pow : BT → Ord, rather than by direct structural -well-founded recursion. RankMonoUnionWF.wf-<ᵇᵘ composes stdlib's -Induction.WellFounded Subrelation.wellFounded + On.wellFounded against -wf-<′ (well-foundedness of the Brouwer-ordinal order _<′_). The union -umbrella RankMonoUnion._<ᵇᵘ_ is built from source-rule extensions via -Sum + [_,_] mediator (PR #168) so that new source-rule extensions ship -as separate modules and union in with two mechanical edits, with the -WfCNF wrap (RankMonoUnionWfCNF._<ᵇᵘⁿ_, PR #169) propagating automatically. -""" -consequences = """ -Gate 2 (well-foundedness of the union) CLOSED in PR #170 under --safe ---without-K with zero new postulates. Gate 1 (tail-rank-equality -discharge for the cross-head rank-equal case) stays OPEN — a structural -blocker whose two pre-identified unblock routes were CHECKED-REFUTED in -PR #146. Gate 3 (further source-rule extensions, Path-4+) stays OPEN but -mechanical via the documented union recipe. The rank-embedding transport -is the architectural pattern future source-rule extensions inherit. -""" -modules = [ - "proofs/agda/Ordinal/Buchholz/RankMonoUnion.agda", - "proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda", - "proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda", -] -supersedes = "none" - -[[architecture-decisions]] -id = "adr-011" -title = "echo↔ephapax cross-repo bridge as a NARROW definitional stub" -status = "accepted" -date = "2026-05-30" -context = """ -The hyperpolymath ecosystem wanted a named correspondence between -echo-types' L3 layer (weaken : LEcho linear → LEcho affine; -no-section-collapse-to-residue) and ephapax-affine's L3 layer. A full -mechanised bridge across all of ephapax-affine's layers (L1/L2/L4) would -be a large, speculative undertaking. -""" -decision = """ -Ship proofs/agda/EchoEphapaxBridge.agda as a NARROW stub: two -definitional refl-renames plus a docstring catalogue (ephapax-L3-weaken, -ephapax-L3-no-section-collapse). Honest scope is L3 ONLY; ephapax-affine -itself and L1/L2/L4 are explicitly NOT mirrored. Package layout -documented in docs/bridges/EchoBridges.md. -""" -consequences = """ -Closes echo-types#126. Establishes the bridge naming convention without -overclaiming a deep correspondence. Extending to further ephapax layers -is separate future work, not unfinished bridge business. Landed across -PRs #161/#162/#163. -""" -module = "proofs/agda/EchoEphapaxBridge.agda" -supersedes = "none" - -[[architecture-decisions]] -id = "adr-012" -title = "Ordinal/Buchholz track RETIRED from echo-types; disposition = extraction" -status = "accepted" -date = "2026-06-21" -context = """ -The transfinite ordinal / Buchholz / Veblen ascent (target ψ₀(Ω_ω)) outgrew -echo-types. It was PARKED 2026-06-20 (D-2026-06-20: consumer-less after the -Groove cleave resolved to a finite, well-foundedness-only zipper), then -escalated to RETIRED 2026-06-21 (D-2026-06-21). The landed artifact is correct -(--safe --without-K, zero postulates, in the green closure); Echo Core never -depended on it beyond the OmegaMarkers <- Buchholz.Syntax <- EchoOrdinal bridge. -""" -decision = """ -No new ordinal rung is opened in echo-types. The disposition is extraction to -its own ordinal-notation repository — the physical cross-repo cut is the -owner's (tracking issue #263). Firewall: OmegaMarkers <- Buchholz.Syntax <- -EchoOrdinal STAY; everything else under proofs/agda/Ordinal/ MOVES. Order-type -fidelity to ψ₀(Ω_ω) (D-2026-06-14) remains an OPEN external problem — -retirement neither closes nor over-claims it. -""" -consequences = """ -The [recent-work] / [current-workstream] blocks in STATE.a2ml are preserved as -HISTORY of the 2026-06-05 -> 2026-06-12 ordinal-track arc, not live work. -Hand-off record: docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc. -Live tracks: composition (landed); establishment (Pillars A–D+F closed, Pillar -E in-repo complete at the bounded-claim level); variance resolved (#243); -aggregation generalised (#175). -""" -module = "proofs/agda/Ordinal/ (whole subtree except the STAY firewall)" -supersedes = "none" - -# ============================================================ -# Development practices (relevant subset) -# ============================================================ - -[development-practices.code-style] -agda = "--safe --without-K mandatory; no postulates" -asciidoc = "narrow-true claims preferred over broader-easy; honest qualification visible in source" -commit-messages = "structured per INTEGRATION_COMMITS.adoc; include rationale in body, not just title" - -[development-practices.versioning] -scheme = "SemVer 2.0.0" -current-target = "0.1.1" -recipe-extension-target = "0.2.0+" - -[development-practices.review] -gate-pattern = "three identity gates with explicit retraction conditions per gate" -lane-discipline = "gate-1, gate-2, gate-3 work in parallel lanes; integration via cross-lane audit" -falsifier-format = "explicit FALSIFIER callouts in AsciiDoc + comment block above corresponding Agda definition" - -[development-practices.documentation] -cascade-discipline = "narrowings to gate-1's claim must propagate to all five canonical doc locations: gate-1-distinct-phenomenon, gate-2-handoff, roadmap-gates, adjacency README, top README" -do-not-redo = "STATE.a2ml tracks terminated questions and forbidden rebrandings; consult before starting any investigation framed as a follow-up to a closed question" - -[development-practices.versioning-of-decisions] -status-values = "proposed / accepted / deprecated / superseded / rejected" -supersedes-pattern = "when an ADR replaces another, mark the old one with status=superseded and superseded-by = ; never delete" - -# ============================================================ -# Design rationale -# ============================================================ - -[design-rationale] -why-narrower-true = """ -Gate-1's original framing (five axes simultaneously) was overstrong. The -honest narrower-true claim — distinctness rests on truncation + 2-cell — -is provably correct, formally certified, and removes the integration -recipe from a load it cannot bear. Narrowing claims toward what the -formalisation actually shows, rather than maintaining ambition the -formalisation does not support, is the project's standing epistemic -posture. -""" -why-path-b = """ -Full formalisation of the recipe-non-triviality theorem requires -postulates that --safe Agda forbids. PATH B (partial formalisation -accepted as sufficient given empirical + structural evidence) is the -honest closure: per-axis halves are proved, concrete construction halves -are proved, the generic 2D iff is documented as out of safe-Agda scope. -The negative gate-1 finding does not depend on the generic theorem. -""" -why-keep-superseded-readings = """ -The two reading-decision documents (READING 1 and READING 2) plus their -comparison are kept with SUPERSEDED banners rather than deleted. They -record the alternatives that were considered, which prevents future -investigators from re-deriving them from scratch under different names. -This is the canonical anti-duplicate-work pattern for this codebase. -""" -why-recipe-stays-as-vocabulary = """ -Even though the recipe doesn't carry distinctness, it still organises the -per-axis lemma family (composition, join, propositionality of order) and -provides a uniform shape for stating per-axis transport actions. Removing -it from the codebase would lose useful organisation. Keeping it as -'organising vocabulary, not locus of distinctness' is the right framing. -""" -why-state-not-ad-hoc-handover = """ -Earlier sessions used ad-hoc handover documents (text files, conversation -summaries). The EI-2 termination was captured in machine-readable state -form so future sessions can parse and consult it programmatically; since -2026-06-12 the six 6a2 files carry that record in TOML-A2ML (estate -convention), converted faithfully from the earlier S-expression bodies. -""" - -# ============================================================ -# END OF META -# ============================================================ diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/6a2/NEUROSYM.a2ml deleted file mode 100644 index cc173c8..0000000 --- a/.machine_readable/6a2/NEUROSYM.a2ml +++ /dev/null @@ -1,348 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# -# NEUROSYM.a2ml — formal-evidence semantics for EI-2 termination -# -# Format: TOML-A2ML (estate convention; `#` comments, [section], key = "value") -# -# Provenance: converted 2026-06-12 from the Guile S-expression body -# `(define-module (echo-types neurosym) ...)` that previously occupied -# this file. Faithful translation of all fourteen formal certificates, -# nine data points, three structural arguments, three unproved -# obligations, and the evidence summary. The original S-expr schema -# reference was: -# https://github.com/hyperpolymath/standards/blob/main/neurosym-a2ml/spec/abnf/neurosym.abnf -# -# Pipeline position (per playbook spec § 8.1): -# META validate → AGENTIC gate → NEUROSYM discharge → ... -# -# Purpose: encode the formal evidence backing EI-2's negative verdict in -# machine-checkable form — what was proved, where, what it implies, and -# what was deliberately NOT proved (PATH B obligations). - -[metadata] -project = "echo-types" -last-updated = "2026-06-12" - -# ============================================================ -# Formal certificates (theorems proved, with location and implications) -# ============================================================ - -[[formal-certificates]] -id = "cert-001" -name = "client-to-server-injective-on-proj₁" -location = "proofs/agda/characteristic/ChoreoInjective.agda" -statement = "client-to-server preserves proj₁-distinctness. Distinct globals ↦ distinct images." -implies = "Choreo satisfies the non-loss-only criterion at strict step c⊑s." -used-in = "AGENTIC G-001 citation; STATE terminated-questions EI-2 criterion-status." -license = "Proved by direct construction from swap-injective and involutivity." - -[[formal-certificates]] -id = "cert-002" -name = "client-to-server-preserves-distinction" -location = "proofs/agda/characteristic/ChoreoInjective.agda" -statement = "Corollary: if proj₁ e₁ ≢ proj₁ e₂, then client-to-server e₁ ≢ client-to-server e₂." -implies = "Multiplicity preservation under Choreo's strict-step transport." -depends-on = "cert-001" - -[[formal-certificates]] -id = "cert-003" -name = "RoleGraded.choreo-grade-commute" -location = "proofs/agda/characteristic/RoleGraded.agda" -statement = "Commutation of applyRole and applyGrade on RoleGEcho. 18 cases, 1 non-trivial (c⊑s, keep≤keep) reducing to client-to-server e." -implies = "EI-1 closure (protocol-correct) and EI-2 data point 1 (substantively narrow)." -used-in = "EI-2 evidence; EI-1 closure record." - -[[formal-certificates]] -id = "cert-004" -name = "RoleMode.choreo-mode-commute" -location = "proofs/agda/characteristic/RoleMode.agda" -statement = "Commutation of applyRole and applyMode on RoleMEcho. 9 cases, 1 non-trivial." -implies = "EI-2 data point 2 — Role × Mode same-shape pattern as Role × Grade." - -[[formal-certificates]] -id = "cert-005" -name = "ModeGraded.mode-grade-commute" -location = "proofs/agda/characteristic/ModeGraded.agda" -statement = "Commutation of applyMode and applyGrade on ModeGEcho. 18 cases, 0 non-trivial." -implies = "EI-2 data point 3 — loss-only-pair commutation is vacuous on the strict reading." -note = "File has trailing 'd' — ModeGraded.agda is canonical. Do not create ModeGrade.agda." - -[[formal-certificates]] -id = "cert-006" -name = "RoleModeGrade.role-mode-commute" -location = "proofs/agda/characteristic/RoleModeGrade.agda" -statement = "3D pairwise: 27 cases, 1 non-trivial. Inherits from RoleMode + Grade-spectator triviality." -implies = "EI-2 data point 4 — n=3 inherits n=2 pattern." - -[[formal-certificates]] -id = "cert-007" -name = "RoleModeGrade.role-grade-commute" -location = "proofs/agda/characteristic/RoleModeGrade.agda" -statement = "3D pairwise: 36 cases, 1 non-trivial. Inherits from RoleGraded + Mode-spectator triviality." -implies = "EI-2 data point 5." - -[[formal-certificates]] -id = "cert-008" -name = "RoleModeGrade.mode-grade-commute" -location = "proofs/agda/characteristic/RoleModeGrade.agda" -statement = "3D pairwise: 36 cases, 0 non-trivial. Inherits from ModeGraded." -implies = "EI-2 data point 6 — loss-only-pair commutation is vacuous in 3D context too." - -[[formal-certificates]] -id = "cert-009" -name = "RoleModeGrade.applyAll + trace-non-trivial-cell" -location = "proofs/agda/characteristic/RoleModeGrade.agda" -statement = "3D triple commutation: 54 cases, 1 non-trivial at (c⊑s, linear≤linear, keep≤keep), reducing to client-to-server e." -implies = "EI-2 data point 7 — triple inherits the same single-cell pattern." - -[[formal-certificates]] -id = "cert-010" -name = "RoleRole.RREcho-pair commutation" -location = "proofs/agda/characteristic/RoleRole.agda" -statement = "Self-pairing of Choreo via independent product: 9 cases, 0 non-trivial. Trivial by categorical product structure." -implies = "EI-2 critical finding — even two non-loss-only axes paired don't produce substantive simultaneous content. NLO is necessary but NOT sufficient." -used-in = "AGENTIC G-001; META adr-002; STATE forbidden-rebrandings." - -[[formal-certificates]] -id = "cert-011" -name = "RoleRole.RREcho-shared (negative result)" -location = "proofs/agda/characteristic/RoleRole.agda" -statement = "Self-pairing of Choreo via shared state: per-axis transport not uniformly definable." -implies = "EI-2 critical finding — alternative design also fails. The recipe doesn't apply." -used-in = "Same citation chain as cert-010." - -[[formal-certificates]] -id = "cert-012" -name = "InteractionTest.no-simultaneous-non-trivial-cell" -location = "proofs/agda/characteristic/InteractionTest.agda" -statement = "P3: in any cell of the existing recipe families, at most one axis acts non-trivially; the other is identity." -implies = "Formal statement of the one-axis-at-a-time pattern. Discharges EI-2's structural argument as Agda-level." - -[[formal-certificates]] -id = "cert-013" -name = "RecipeTheorem per-axis halves (forward and backward)" -location = "proofs/agda/characteristic/RecipeTheorem.agda" -statement = "Per-axis: for an NLO axis, the recipe contributes a non-trivial cell; for a loss-only axis, the recipe contributes only trivial cells." -implies = "Half of the recipe-non-triviality theorem (for individual axes). Combining into a 2D iff requires postulates not available in safe Agda." -status = "Proved per-axis; not lifted to 2D iff. PATH B accepted." - -[[formal-certificates]] -id = "cert-014" -name = "RecipeNonTriviality concrete construction halves" -location = "proofs/agda/characteristic/RecipeNonTriviality.agda" -statement = "For each of the existing recipe constructions (RoleGraded, RoleMode, ModeGraded, RoleModeGrade, RoleRole), the non-trivial cell count matches the prediction of the per-axis halves." -implies = "Concrete-construction half of the recipe-non-triviality theorem. PATH B route to EI-2 termination." - -# ============================================================ -# Data points (the seven canonical EI-2 measurements) -# ============================================================ - -[[data-points]] -id = "dp-1" -construction = "RoleGraded" -axes = "Role × Grade" -axis-non-loss-only = ["Role"] -axis-loss-only = ["Grade"] -cells = 18 -non-trivial-cells = 1 -non-trivial-location = "(c⊑s, keep≤keep)" -non-trivial-content = "client-to-server e (Choreo's transport at c⊑s)" -certificate = "cert-003" - -[[data-points]] -id = "dp-2" -construction = "RoleMode" -axes = "Role × Mode" -axis-non-loss-only = ["Role"] -axis-loss-only = ["Mode"] -cells = 9 -non-trivial-cells = 1 -non-trivial-location = "(c⊑s, linear≤linear)" -non-trivial-content = "client-to-server e" -certificate = "cert-004" - -[[data-points]] -id = "dp-3" -construction = "ModeGraded" -axes = "Mode × Grade" -axis-non-loss-only = [] -axis-loss-only = ["Mode", "Grade"] -cells = 18 -non-trivial-cells = 0 -non-trivial-location = "none" -non-trivial-content = "none" -certificate = "cert-005" -note = "Falsifier-positive on the strict reading of the recipe." - -[[data-points]] -id = "dp-4" -construction = "RoleModeGrade.role-mode-commute (3D pairwise)" -cells = 27 -non-trivial-cells = 1 -certificate = "cert-006" - -[[data-points]] -id = "dp-5" -construction = "RoleModeGrade.role-grade-commute (3D pairwise)" -cells = 36 -non-trivial-cells = 1 -certificate = "cert-007" - -[[data-points]] -id = "dp-6" -construction = "RoleModeGrade.mode-grade-commute (3D pairwise)" -cells = 36 -non-trivial-cells = 0 -certificate = "cert-008" -note = "Loss-only-pair commutation is vacuous in 3D context too." - -[[data-points]] -id = "dp-7" -construction = "RoleModeGrade.applyAll (3D triple)" -cells = 54 -non-trivial-cells = 1 -certificate = "cert-009" -note = "Single load-bearing cell at (c⊑s, linear≤linear, keep≤keep)." - -[[data-points]] -id = "dp-7a" -construction = "RoleRole.RREcho-pair (independent product)" -axes = "Role × Role (Choreo self-pair)" -axis-non-loss-only = ["Role", "Role"] -axis-loss-only = [] -cells = 9 -non-trivial-cells = 0 -certificate = "cert-010" -note = "*** CRITICAL FINDING: even two non-loss-only axes paired don't produce substantive simultaneous content. NLO is NECESSARY but NOT SUFFICIENT. ***" - -[[data-points]] -id = "dp-7b" -construction = "RoleRole.RREcho-shared (shared-state design)" -cells = "n/a" -non-trivial-cells = "n/a" -certificate = "cert-011" -note = "Per-axis transport not uniformly definable; recipe doesn't apply." - -# ============================================================ -# Structural arguments (the load-bearing distinctness arguments that -# survive EI-2's negative finding) -# ============================================================ - -[[structural-arguments]] -id = "sa-1" -name = "Truncation argument" -claim = """ -For non-injective f with multiple preimages of y, Echo f y is -constructively not a mere proposition. Neighbour theories that -propositionally truncate the witness type lose what echo retains. -""" -formal-certificates = [ - "echo-not-prop-Tropical", - "echo-not-prop-Epistemic", - "echo-not-prop-Linear", -] -formal-locations = [ - "proofs/agda/examples/TropicalArgmin.agda", - "proofs/agda/examples/EpistemicUpdate.agda", - "proofs/agda/examples/LinearErasure.agda", -] -gap = "Q2.1 (generalisation to all non-injective f) is open." -status = "Pointwise certified across three bridge axes; generalisation pending." - -[[structural-arguments]] -id = "sa-2" -name = "2-cell argument" -claim = """ -Natural 2-cells in neighbour frameworks (quotient equalizers, Galois -meets) are structurally Σ-over-preimages-shaped — i.e., already -echo-shaped. -""" -formal-certificates = [ - "Sophisticated.equalizer→echo-pair", - "Sophisticated.meet→echo-intersection", - "meet-on-diagonal→equalizer", -] -formal-locations = [ - "proofs/agda/EchoVsQuotient.agda § Sophisticated", - "proofs/agda/EchoVsGalois.agda § Sophisticated", -] -status = "Closed by both Sophisticated submodules. Diagonal correspondence between the two arguments also formalised." - -[[structural-arguments]] -id = "sa-3" -name = "Recipe is organising vocabulary, NOT distinctness load" -claim = """ -Post-EI-2: the integration recipe is useful for organising fiber-shaped -reasoning across multiple axes but does NOT produce substantive -simultaneous cross-axis content. It is not the locus of distinctness. -""" -negative-evidence = ["cert-005", "cert-008", "cert-010", "cert-011"] -positive-evidence = "All seven data points support sa-3; no data point refutes it." -alternatives-ruled-out = [ - "recipe carries cross-axis distinctness uniformly", - "non-loss-only is sufficient for substantive integration", - "different family choice for ModeGrade would change the result", - "Choreo × Choreo would carry substantive content with the right design", -] -status = "Standing decision sd-002 in STATE.a2ml. ADR adr-001 in META.a2ml." - -# ============================================================ -# Unproved obligations (deliberately deferred under PATH B) -# ============================================================ - -[[unproved-obligations]] -id = "unp-1" -name = "Full 2D iff for recipe-non-triviality" -statement = "(NLO at least one of axis₁, axis₂) iff (non-trivial-cell-count(axis₁ × axis₂) ≥ 1)" -status = "Not formalised in safe Agda." -obstacle = "Requires postulates: decidable equality on decoration types, F-collapses axioms, extensionality on cell actions." -workaround = "Per-axis halves (cert-013) + concrete construction halves (cert-014) + RoleRole structural argument (cert-010, cert-011) accepted as PATH B evidence." -under-PATH-B-status = "Accepted as deliberately-deferred. Do NOT attempt to close in safe Agda; doing so triggers AGENTIC gate G-004." - -[[unproved-obligations]] -id = "unp-2" -name = "Recipe extension: coupled state across axes" -statement = "If the recipe permits a family RREcho with shared state across axes, does it produce substantive simultaneous cross-axis content?" -status = "Open as v0.2+ work, NOT as EI-2 unfinished business." -under-EI-2-scope = false -filed-as = "Will be EI-3 or later when v0.2 work begins; not part of EI-2's record." - -[[unproved-obligations]] -id = "unp-3" -name = "Generalisation of echo-not-prop" -statement = "For arbitrary non-injective f with at least two distinct preimages of y, is-prop (Echo f y) → ⊥." -status = "Open as Q2.1 in next-questions.adoc." -priority = "high" -rationale = "Truncation argument is one of the two load-bearing distinctness arguments post-EI-2; strengthening it has high leverage. Listed in STATE next-actions." - -# ============================================================ -# Evidence summary (one-paragraph form for citation) -# ============================================================ - -[evidence-summary] -paragraph = """ -EI-2 closes negatively via PATH B. Across seven data points (RoleGraded -18:1, RoleMode 9:1, ModeGraded 18:0, RoleModeGrade 3D pairwise 27:1, -36:1, 36:0, triple 54:1, plus RoleRole 9:0 / non-applicable), the -integration recipe with the existing five named axes does not produce -substantive simultaneous cross-axis content. Every non-trivial cell -carries one-axis-at-a-time content; the load-bearing transport is always -Choreo's client-to-server at c⊑s. The non-loss-only criterion (formally -certified for Choreo in ChoreoInjective.agda) is necessary but not -sufficient: even the only NLO self-pairing (Role × Role) degenerates to -coordinate-product commutation under independent-product design or -breaks per-axis transport under shared-state design. Distinctness -against neighbour frameworks therefore rests on the truncation argument -(echo-not-prop family) and the 2-cell argument (Sophisticated -submodules), both formalised independently of the recipe. Gate-1 has -been narrowed across five doc locations to reflect this. The full 2D iff -theorem is not formalisable in safe Agda without postulates; PATH B -accepts the per-axis halves and concrete construction halves as -sufficient evidence. -""" -one-line = "EI-2 negative; recipe is organising vocabulary, not distinctness load; truncation + 2-cell carry gate-1 instead." - -# ============================================================ -# END OF NEUROSYM -# ============================================================ diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/6a2/PLAYBOOK.a2ml deleted file mode 100644 index 2e436b0..0000000 --- a/.machine_readable/6a2/PLAYBOOK.a2ml +++ /dev/null @@ -1,346 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# -# PLAYBOOK.a2ml — operational procedures for echo-types sessions -# -# Format: TOML-A2ML (estate convention; `#` comments, [section], key = "value") -# -# Provenance: converted 2026-06-12 from the Guile S-expression body -# `(define-module (echo-types playbook) ...)` that previously occupied -# this file. Faithful translation of the derivation declaration, the -# five procedures, alerts, contacts, and the session lifecycle (itself -# migrated from the former short-form companion file during the -# 2026-04-30 .scm→.a2ml migration). File-path citations were updated -# from the S-expr-era audit-output/*.scm names to the canonical -# .machine_readable/6a2/*.a2ml locations. The original S-expr schema -# reference was: -# https://github.com/hyperpolymath/standards/blob/main/playbook-a2ml/spec/PLAYBOOK-FORMAT-SPEC.adoc -# -# Pipeline position (per playbook spec § 8.1): -# META validate → AGENTIC gate → NEUROSYM discharge → -# PLAYBOOK execute → STATE update → ECOSYSTEM check -# -# Purpose: machine-executable procedures derived from META.a2ml -# (architectural decisions) and gated by AGENTIC.a2ml. PLAYBOOKs -# introduce no new authority; they execute permitted plans. - -[metadata] -project = "echo-types" -last-updated = "2026-06-12" - -# ============================================================ -# Derivation declaration (per playbook spec § 6.4) -# ============================================================ - -[derivation-source] -type = "derived" -meta-rules = ["adr-001", "adr-002", "adr-003", "adr-004", "adr-005", "adr-006"] -state-context = "EI-2 terminated; integration commits 1-7 staged but not yet pushed (historical context at derivation time; long since pushed and merged)." -agentic-gate = "AGENTIC.a2ml pre-action-checks; redo-traps active." -user-intent = "Capture EI-2 termination in 6a2 format; produce next options." -timestamp = "2026-04-29" - -# ============================================================ -# Procedures -# ============================================================ - -# ------------------------------------------------------------ -# on-session-entry — the most important procedure. Runs when a new -# session enters the 6a2 metadata directory. -# ------------------------------------------------------------ - -[procedures.on-session-entry] -description = "Procedure for any new session entering .machine_readable/6a2/. Establishes context without re-deriving anything." -preconditions = [ - ".machine_readable/6a2/ directory exists", - "INDEX.adoc exists (repo root)", - ".machine_readable/6a2/STATE.a2ml exists", - ".machine_readable/6a2/META.a2ml exists", -] -postconditions = [ - "Session has fresh context", - "No redo-trap was triggered during entry", -] -on-failure = "If any step fails (file missing, malformed), STOP. Do not proceed with operational requests until the file system is reconciled." - -[[procedures.on-session-entry.steps]] -step = 1 -action = "Read INDEX.adoc (repo root)" -purpose = "Map of which fact lives where; ~1 minute of reading covers ~80% of context." -timeout = 60 - -[[procedures.on-session-entry.steps]] -step = 2 -action = "Read .machine_readable/6a2/STATE.a2ml in full" -purpose = "Current authoritative state. Includes terminated-questions, do-not-redo register, forbidden-rebrandings, next-actions." -timeout = 120 - -[[procedures.on-session-entry.steps]] -step = 3 -action = "Read .machine_readable/6a2/META.a2ml" -purpose = "Architectural decisions; permanent record of what's been settled." -timeout = 90 - -[[procedures.on-session-entry.steps]] -step = 4 -action = "Skim .machine_readable/6a2/AGENTIC.a2ml gate-rules" -purpose = "Know which classes of requests trigger refusal or redirection." -timeout = 60 - -[[procedures.on-session-entry.steps]] -step = 5 -action = "Cite specific entries (not summaries) when discussing EI-2 with the user" -purpose = "Forbidden-rebrandings include 'cite from memory and lose nuance'. Always cite the file path." -timeout = 0 - -# ------------------------------------------------------------ -# on-EI-2-mention — what to do when the user mentions EI-2 or any topic -# in its forbidden-rebrandings list. -# ------------------------------------------------------------ - -[procedures.on-EI-2-mention] -description = "Procedure for any request that touches EI-2 territory." -preconditions = [ - "on-session-entry has run", - "STATE.a2ml has been read", -] -postconditions = [ - "Request was handled per gate rules", - "No forbidden-rebranding was produced", -] -on-failure = "Refuse with citation. Do not produce content that contradicts STATE forbidden-rebrandings even if the user requests it; this is a critical gate." - -[[procedures.on-EI-2-mention.steps]] -step = 1 -action = "Check the request against AGENTIC gate G-001 (do-not-reopen-EI-2)" -purpose = "Most EI-2 mentions are not reopens; some are. Distinguish carefully." -timeout = 0 - -[[procedures.on-EI-2-mention.steps]] -step = 2 -action = "Check the request against AGENTIC gate G-005 (do-not-rebrand-recipe-as-distinctness-locus)" -purpose = "Catch implicit attempts to put the recipe back into the distinctness story." -timeout = 0 - -[[procedures.on-EI-2-mention.steps]] -step = 3 -action = "If the request is asking ABOUT EI-2 (status, finding, evidence), respond using the evidence-summary in NEUROSYM.a2ml with citations. Do not paraphrase from memory." -purpose = "Cite-from-files, not from memory." -timeout = 0 - -[[procedures.on-EI-2-mention.steps]] -step = 4 -action = "If the request is asking to DO something EI-2-adjacent, run pre-action-checks from AGENTIC.a2ml" -purpose = "Refuse, redirect, or proceed-with-caveat per gate severity." -timeout = 0 - -# ------------------------------------------------------------ -# integration-push — apply the seven staged commits. -# HISTORICAL: the seven-commit integration sequence was pushed and -# merged long since (see STATE next-actions resolutions). Retained as -# the canonical shape for any future staged-commit push procedure. -# ------------------------------------------------------------ - -[procedures.integration-push] -status = "historical" -description = "Apply the seven-commit integration sequence from INTEGRATION_COMMITS.adoc." -requires-confirmation = true -preconditions = [ - "All seven commits' content staged", - "User explicitly confirms the push", - "Working tree of echo-types repo is clean", - "Branch integrate-parallel-work does not exist or is safe to overwrite", -] -postconditions = [ - "All seven commits on origin/integrate-parallel-work", - "Mirror workflow either completed or silently skipped tokens", - "STATE session commits-pushed updated to 7", -] -on-failure = "Rollback: keep the branch but inform user of the failure point. Do not force-push." - -[[procedures.integration-push.steps]] -step = 1 -action = "Confirm with user: 'Push seven commits to integrate-parallel-work branch on github.com/hyperpolymath/echo-types?'" -timeout = 0 - -[[procedures.integration-push.steps]] -step = 2 -action = "Run the commit sequence from INTEGRATION_COMMITS.adoc, commits 1-6 (gate-1, adjacency, gate-2, gate-3, polish)" -timeout = 600 - -[[procedures.integration-push.steps]] -step = 3 -action = "Run commit 7 (EI-2 termination)" -timeout = 300 - -[[procedures.integration-push.steps]] -step = 4 -action = "Push to origin (GitHub canonical)" -timeout = 60 - -[[procedures.integration-push.steps]] -step = 5 -action = "Verify mirror workflow ran (GitLab and Codeberg)" -timeout = 300 - -# ------------------------------------------------------------ -# capture-new-EI-finding — when actually new EI-territory work happens -# (not EI-2 reopen, but e.g. EI-3 recipe extension). -# ------------------------------------------------------------ - -[procedures.capture-new-EI-finding] -description = "Capture a new EI-style investigation result that is NOT an EI-2 reopen." -preconditions = [ - "Verified via AGENTIC G-001 that this is genuinely new work, not EI-2 reopen", - "Investigation has produced concrete data points or formal certificates", -] -postconditions = [ - "New investigation has its own record", - "EI-2 record is not modified", - "All six 6a2 files are consistent", -] -on-failure = "If any of the 6a2 files becomes inconsistent, STOP and report. Inconsistency is worse than incomplete capture." - -[[procedures.capture-new-EI-finding.steps]] -step = 1 -action = "Assign new ID (EI-3, EI-4, ...). Never reuse EI-2." -timeout = 0 - -[[procedures.capture-new-EI-finding.steps]] -step = 2 -action = "Add entry to next-questions.adoc Open section." -timeout = 0 - -[[procedures.capture-new-EI-finding.steps]] -step = 3 -action = "If new structural decision made, add adr-NNN to META.a2ml." -timeout = 0 - -[[procedures.capture-new-EI-finding.steps]] -step = 4 -action = "If finding affects standing decisions, add or update sd-NNN in STATE.a2ml." -timeout = 0 - -[[procedures.capture-new-EI-finding.steps]] -step = 5 -action = "Add formal certificates to NEUROSYM.a2ml if applicable." -timeout = 0 - -[[procedures.capture-new-EI-finding.steps]] -step = 6 -action = "Add gate rule to AGENTIC.a2ml if a new redo-trap is identified." -timeout = 0 - -# ------------------------------------------------------------ -# respond-to-status-query — the most common request: "what's the state -# of echo-types?" -# ------------------------------------------------------------ - -[procedures.respond-to-status-query] -description = "Procedure for answering 'what's the state of X?' queries." -preconditions = ["STATE.a2ml has been read"] -postconditions = [ - "User has the current state with citations", - "No paraphrasing from memory", -] - -[[procedures.respond-to-status-query.steps]] -step = 1 -action = "Identify what 'X' is (EI-2, integration, gate-1, ...)" -timeout = 0 - -[[procedures.respond-to-status-query.steps]] -step = 2 -action = "If X is EI-2: cite NEUROSYM evidence-summary one-line + offer the paragraph form." -timeout = 0 - -[[procedures.respond-to-status-query.steps]] -step = 3 -action = "If X is integration: cite STATE session commits-staged and commits-pushed (historical; long since merged)." -timeout = 0 - -[[procedures.respond-to-status-query.steps]] -step = 4 -action = "If X is one of gates 1/2/3: cite the corresponding adjacency README + gate-N-handoff.adoc + the standing-decisions in STATE.a2ml." -timeout = 0 - -[[procedures.respond-to-status-query.steps]] -step = 5 -action = "Always offer next-actions from STATE.a2ml if the user wants concrete forward motion." -timeout = 0 - -# ============================================================ -# Alerts -# ============================================================ - -[alerts.forbidden-rebranding-detected] -severity = "critical" -channel = "user" -message = "Refused: this matches STATE forbidden-rebrandings entry: {{which-entry}}. Citation: {{file-path}}. To override: justify with structural argument not in the forbidden list." -escalation = 0 - -[alerts.EI-2-reopen-detected] -severity = "critical" -channel = "user" -message = "Refused: AGENTIC gate G-001. EI-2 is terminated. Citations: STATE.a2ml > terminated-questions > EI-2; META.a2ml > adr-002. Reopen requires explicit user override with structural justification." -escalation = 0 - -[alerts.cascade-inconsistency-detected] -severity = "high" -channel = "user" -message = "Inconsistency: {{location-A}} says X but {{location-B}} says Y. Five-doc cascade is in STATE.a2ml > cascade-applied. Reconcile before proceeding." -escalation = 60 - -[alerts.file-missing-on-entry] -severity = "high" -channel = "user" -message = "Missing expected file: {{path}}. on-session-entry procedure cannot proceed without {{INDEX,STATE,META}}. STOP and reconcile." -escalation = 0 - -[alerts.PATH-B-violation-attempt] -severity = "medium" -channel = "user" -message = "Detected attempt to formalise full 2D iff theorem in safe Agda (AGENTIC G-004). PATH B accepted partial formalisation; obstacles documented. Citation: META adr-003." -escalation = 60 - -# ============================================================ -# Contacts -# ============================================================ - -[contacts.author] -name = "Jonathan D.A. Jewell (hyperpolymath)" -channel = "j.d.a.jewell@open.ac.uk" -role = "Project owner; standing decisions traceable to." -hours = "asynchronous" - -[contacts.escalation] -name = "Hyperpolymath constellation maintainers" -channel = "via standards repo discussions" -role = "If a 6a2 schema question arises that this PLAYBOOK doesn't resolve." -hours = "asynchronous" - -# ============================================================ -# Session lifecycle (migrated from the former short-form companion -# STATE file as part of the 2026-04-30 .scm → .a2ml migration. The -# original file's own header marked this block as the only unique -# contribution it carried.) -# ============================================================ - -[lifecycle] -on-enter = [ - "Read .machine_readable/6a2/STATE.a2ml first", - "Read .machine_readable/6a2/META.a2ml for permanent decisions", - "Check status/phase before starting any work", - "If user asks about EI-2: state TERMINATED; refer to the EI-2 blocks in STATE", -] -on-exit = [ - "Update status/phase if changed", - "Update commits-pushed if any commits actually pushed", - "If new questions opened, add to open-questions in STATE", - "If naming-traps encountered, add to the do-not-redo register in STATE", - "Never remove the EI-2 blocks; they are permanent record", -] - -# ============================================================ -# END OF PLAYBOOK -# ============================================================ diff --git a/.machine_readable/6a2/README.adoc b/.machine_readable/6a2/README.adoc index c851cfb..a50a6fa 100644 --- a/.machine_readable/6a2/README.adoc +++ b/.machine_readable/6a2/README.adoc @@ -1,20 +1,13 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) Jonathan D.A. Jewell -# A2ML 6a2 Directory +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += `.machine_readable/6a2/` — retired -This directory contains the 6 core A2ML machine-readable metadata files for this repository. +The `.a2ml` records that lived here were removed on 2026-09-30 by owner +ruling: the `.a2ml` surface is retired in favour of `.deed` records. -## Files - -- `AGENTIC.a2ml` - AI agent operational gating, safety controls -- `ECOSYSTEM.a2ml` - Project ecosystem position, relationships, explicit boundaries -- `META.a2ml` - Architecture decisions (ADRs), development practices, design rationale -- `NEUROSYM.a2ml` - Symbolic semantics, composition algebra -- `PLAYBOOK.a2ml` - Executable plans, operational runbooks -- `STATE.a2ml` - Project state, phase, milestones, session history - -## Standards Compliance - -These files follow the A2ML Format Family specification from: -https://github.com/hyperpolymath/standards/tree/main/a2ml +The last tree that held them is frozen at +https://github.com/hyperpolymath/echo-types/tree/39a7a99cbe19a918843e9624010510b5fc3b8366/.machine_readable/6a2[commit 39a7a99]. +Read that copy for history; do not recreate `.a2ml` files here. +Conversion to `.deed` is tracked estate-wide in +https://github.com/hyperpolymath/rsr-template-repo/issues/209[rsr-template-repo#209]. diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml deleted file mode 100644 index 9dd0c32..0000000 --- a/.machine_readable/6a2/STATE.a2ml +++ /dev/null @@ -1,619 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# -# STATE.a2ml — echo-types project state -# -# Format: TOML-A2ML (estate convention; `#` comments, [section], key = "value") -# -# Provenance: converted 2026-06-12 from the Guile S-expression body -# `(define-module (echo-types state) ...)` that previously occupied this -# file (S-expr last-updated: 2026-06-05). The conversion is faithful: the -# EI-2 termination record, standing decisions, artefact lists, cascade -# record, do-not-redo register, forbidden rebrandings, earn-back and -# theory-work closure summaries are preserved in full. The original -# S-expr schema reference was: -# https://github.com/hyperpolymath/standards/blob/main/state-a2ml/spec/abnf/state.abnf -# -# Purpose: machine-readable current project state. -# -# CURRENCY NOTE (2026-06-21): the ordinal / Buchholz track is RETIRED from -# echo-types (owner decision D-2026-06-21) — it outgrew the project and is -# being extracted to its own ordinal-notation repo (physical cut = owner; -# tracking issue #263; hand-off record -# docs/echo-types/decisions/ordinal-fidelity-ladder-parked.adoc). The -# detailed [recent-work] and [current-workstream] blocks below are preserved -# as accurate HISTORY of the 2026-06-05 → 2026-06-12 arc, NOT live work. The -# live tracks as of 2026-06-21 are: composition (landed); establishment -# (Pillars A–D + F closed; Pillar E in-repo complete at the bounded-claim -# level; order-type fidelity the one OPEN external problem, D-2026-06-14); -# variance resolved (#243); aggregation generalised (#175). The EI-2 -# termination capture (April 2026) remains preserved below as history. - -[metadata] -project = "echo-types" -repository = "https://github.com/hyperpolymath/echo-types" -canonical-host = "github" # per current forge workflow -mirrors = ["gitlab", "codeberg"] -version-target = "0.1.1" # CHANGELOG still [Unreleased] over - # [0.1.0+integration-pending]; no new - # release tag minted as of 2026-06-12 -license = "MPL-2.0" -last-updated = "2026-06-21" -status = "active development" -phase = "ordinal track RETIRED (D-2026-06-21, extraction pending #263); composition landed; establishment Pillars A–D+F closed + Pillar E in-repo complete (order-type fidelity OPEN external, D-2026-06-14); variance resolved (#243); aggregation generalised (#175)" - -# ============================================================ -# Recent work (2026-05-30 → 2026-06-12, from git log origin/main) -# ============================================================ -# Source of truth: `git log --since=2026-04-29 --oneline origin/main` -# plus CHANGELOG.md and the CLAUDE.md session arcs. Honest summary; -# proof-side invariants (--safe --without-K, zero unisolated postulates) -# held throughout. - -[recent-work] -window = "2026-05-30 .. 2026-06-12" -summary = """ -Ordinal-track Slice 3+4 Route A arc landed (PRs #165-#171): rank-mono -union umbrella RankMonoUnion._<ᵇᵘ_ over source-rule extensions, WfCNF -wrap (#169), and well-foundedness wf-<ᵇᵘ via rank-embedding transport -(#170, Gate 2 closed). Proof-debt enumeration landed as docs/proof-debt.md -(#172). Cross-repo: EchoEphapaxBridge.agda NARROW L3 stub (#161/#162/#163), -arghda-core subtree extracted to its own repo (#160), eclexia thermodynamic -consumer bridge recorded (#180), Valence Shell / Ochránce recorded as -exploratory downstream consumer (#177). CI: workflows hardened + Hypatia -findings resolved at source (#178); actions group bumps (#179 + codeql-action). -Docs: 6a2 STATE/META refreshed to ordinal-track reality (2026-06-05); -CLAIMS_AUDIT.adoc added and refined as Gate-G1 mapping-only input -(VERDICT + EVIDENCE columns); CITATION email corrected; _build/ gitignored. -Estate standardization adopted into main via PR #185 (GOVERNANCE.adoc, -MAINTAINERS.adoc, .github/CODEOWNERS, 6a2 manifest + README, flat -contractiles, Guix manifest.scm, flake.lock removed, banner/README work); -LICENSE SPDX header restored post-merge. 2026-06-12 governance checkpoint: -six 6a2 files converted from Guile S-expr bodies to TOML-A2ML, README -trio deduplicated (README.md canonical), bot_directives trio + flat -Dustfile/Bustfile + self-validating/ k9 set added. -""" -prs = [160, 161, 162, 163, 165, 166, 167, 168, 169, 170, 171, 172, 177, 178, 179, 180, 185] - -# ============================================================ -# Current workstream (primary landed work as of 2026-06-05 refresh) -# ============================================================ -# The active centre of gravity is the Lane 3 ordinal track. The April -# 2026 EI-2 closure (recorded below under [session-ei2-historical] / -# [[terminated-questions]]) remains valid history but is no longer the -# live work. Source of truth for the entries below: CHANGELOG.md -# (current to 2026-05-30) + git log. - -[current-workstream] -as-of = "2026-06-05" - -[current-workstream.primary] -id = "ordinal-rank-mono-wf" -title = "Buchholz/Ordinal rank-monotonicity + well-foundedness — Slice 3+4 Route A arc" -status = "landed" -date-range = "2026-05-30" -prs = [165, 166, 167, 168, 169, 170, 171] -summary = """ -Rank-mono union umbrella over source-rule extensions. RankMonoUnion._<ᵇᵘ_ -= _<ᵇ¹_ ⊎ _<ᵇ⁺²_ via Sum + [_,_] mediator (#168); RankMonoUnionWfCNF._<ᵇᵘⁿ_ -bundles the canonical-form invariant alongside the rank-relation (#169 -WfCNF wrap); RankMonoUnionWF.wf-<ᵇᵘ derives WellFounded _<ᵇᵘ_ via -Subrelation.wellFounded + On.wellFounded rank-embedding transport from -wf-<′ (#170, Gate 2 of the arc closed). Path-3 prototype -RankMonoSameLeft._<ᵇ⁺²_ adds a literal-same-left source-rule extension -closing in one line via rank-pow-bplus-right-mono (#167). -""" -modules = [ - "proofs/agda/Ordinal/Buchholz/RankMonoUnion.agda", - "proofs/agda/Ordinal/Buchholz/RankMonoUnionWfCNF.agda", - "proofs/agda/Ordinal/Buchholz/RankMonoUnionWF.agda", -] -invariants = "163 modules at arc close; all --safe --without-K; zero new postulates; no funext." - -[current-workstream.primary.gates] -gate-1 = "tail-rank-equality discharge for cross-head rank-equal case — OPEN (structural blocker; both pre-identified unblock routes CHECKED-REFUTED in PR #146)" -gate-2 = "well-foundedness of the union — CLOSED in #170" -gate-3 = "Path-4+ further source-rule extensions — OPEN but mechanical via the documented recipe" - -[[current-workstream.supporting]] -id = "ephapax-bridge" -title = "Cross-repo echo↔ephapax L3 bridge — EchoEphapaxBridge.agda NARROW stub" -status = "landed" -date = "2026-05-30" -prs = [161, 162, 163] -module = "proofs/agda/EchoEphapaxBridge.agda" -summary = """ -Two definitional refl-renames + a docstring catalogue (ephapax-L3-weaken, -ephapax-L3-no-section-collapse) establishing the named correspondence -between echo-types L3 (weaken : LEcho linear → LEcho affine; -no-section-collapse-to-residue) and ephapax-affine's L3 layer. Honest -scope: L3 ONLY; ephapax-affine + L1/L2/L4 NOT mirrored. Closes #126. -Package layout in docs/bridges/EchoBridges.md. -""" -note = "NARROW-stub by design — definitional renames + catalogue, not a deep mechanised bridge." - -[[current-workstream.supporting]] -id = "arghda-core-extraction" -title = "arghda-core subtree extraction" -status = "landed" -date = "2026-05-30" -pr = 160 -umbrella-issue = 159 -summary = """ -Removed arghda-core/ from this repo's tree; it now lives as a standalone -repo (hyperpolymath/arghda-core) per the umbrella in #159. Reduces -echo-types' surface area to the propositional/proof-theoretic core. -""" - -[current-workstream.proof-debt] -status = "enumerated" -pr = 172 -doc = "docs/proof-debt.md" -summary = """ -echo-types' sole soundness-relevant escape hatch — the four -propositional-truncation postulates in -proofs/agda/EchoImageFactorizationPropPostulated.agda — enumerated under -Disposition (c) NECESSARY AXIOM. Clears the recurring -governance/Trusted-base-reduction-policy red check (standards#211). -""" - -[current-workstream.recent-ci] -id = "hypatia-hardening" -pr = 178 -date = "2026-05-30" -summary = "Hardened CI workflows + resolved Hypatia findings at source." - -# ============================================================ -# Session header (HISTORICAL — EI-2 termination, April 2026) -# ============================================================ -# The EI-2 record below is retained as history. EI-2 closed negatively -# in April 2026; it must not be re-investigated (see [[do-not-redo]] and -# forbidden-rebrandings). It is NOT the current workstream — see -# [current-workstream] above for the live ordinal-track work. - -[session-ei2-historical] -investigation-id = "EI-2" -investigation-name = "Robustness of the integration recipe under richer 2D combinations" -opened = "2026-04-28" -closed = "2026-04-29" -verdict = "negative" -route = "path-b" -closing-rationale = """ -Empirical evidence (7 data points) and structural argument (RoleRole.agda) -overwhelming; full 2D iff theorem documented as not formalisable in safe -Agda without postulates; per-axis halves and concrete construction halves -proved. -""" - -# ============================================================ -# Terminated questions (do not reopen) -# ============================================================ - -[[terminated-questions]] -id = "EI-2" -status = "closed-negatively" -verdict = "Integration recipe with the existing five named axes does NOT carry substantive simultaneous cross-axis content." -load-bearing-content = "Every non-trivial cell carries one-axis-at-a-time content; the load-bearing transport is always Choreo's client-to-server at the c⊑s strict step." -criterion-status = "Non-loss-only criterion is necessary but NOT sufficient for substantive simultaneous interaction." -forbidden-reopen-framings = [ - "non-loss-only as recipe precondition (READING 2)", - "weakened gate-1 with NLO precondition (READING 2)", - "richer family choice for ModeGrade (would not change the structural finding)", - "alternative axis pair within the existing five named axes", -] -authoritative-record-files = [ - "docs/EI2_REPORT.adoc", # top Status section - "docs/next-questions.adoc", # closed section - "proofs/agda/characteristic/RecipeNonTriviality.agda", -] -date = "2026-04-29" - -[terminated-questions.data-points] -RoleGraded = { cells = 18, non-trivial = 1, axis-pair = "Role x Grade" } -RoleMode = { cells = 9, non-trivial = 1, axis-pair = "Role x Mode" } -ModeGraded = { cells = 18, non-trivial = 0, axis-pair = "Mode x Grade" } -RoleModeGrade-RM = { cells = 27, non-trivial = 1, axis-pair = "Role x Mode @ 3D pairwise" } -RoleModeGrade-RG = { cells = 36, non-trivial = 1, axis-pair = "Role x Grade @ 3D pairwise" } -RoleModeGrade-MG = { cells = 36, non-trivial = 0, axis-pair = "Mode x Grade @ 3D pairwise" } -RoleModeGrade-trip = { cells = 54, non-trivial = 1, axis-pair = "Role x Mode x Grade @ triple" } -RoleRole-pair = { cells = 9, non-trivial = 0, axis-pair = "Role x Role independent product; trivial by categorical product" } -RoleRole-shared = { cells = "n/a", non-trivial = "n/a", axis-pair = "Role x Role shared state; recipe does not apply" } - -# ============================================================ -# Standing decisions (treat as load-bearing; do not relitigate) -# ============================================================ - -[[standing-decisions]] -id = "sd-001" -title = "Distinctness load is carried by truncation + 2-cell arguments" -status = "accepted" -date = "2026-04-29" -rationale = """ -Across all attempted axis pairings (including the only NLO self-pairing), -the integration recipe produces only one-axis-at-a-time content. -Truncation (echo-not-prop family) and 2-cell (Sophisticated submodules) -carry the gate-1 distinctness load independently of the recipe. -""" -artefacts = [ - "proofs/agda/examples/{TropicalArgmin,EpistemicUpdate,LinearErasure}.agda", - "proofs/agda/EchoVsQuotient.Sophisticated", - "proofs/agda/EchoVsGalois.Sophisticated", -] -consequences = "Gate-1's claim has been narrowed across 5 doc locations. The recipe remains useful as organising vocabulary." - -[[standing-decisions]] -id = "sd-002" -title = "Recipe is organising vocabulary, NOT locus of distinctness" -status = "accepted" -date = "2026-04-29" -rationale = """ -EI-2 termination established that recipe-level commutation theorems are -vacuous when no axis is non-loss-only, and degenerate to coordinate-product -or undefined transport when both are. The recipe still organises the -per-axis lemma family (composition, join, propositionality) but does not -produce substantive simultaneous integration content. -""" -forbidden-claims = [ - "recipe carries cross-axis distinctness", - "five axes simultaneously as a distinctness claim", - "non-loss-only is sufficient for substantive integration content", -] -authoritative-text = "gate-2-handoff.adoc § Observation G" - -[[standing-decisions]] -id = "sd-003" -title = "Forge workflow: GitHub canonical, hub-and-spoke mirror outward" -status = "accepted" -date = "2026-04-28" -rationale = """ -User's standing forge workflow (overrides the static gitlab>github -preference for git operations specifically). Mirror to GitLab and -Codeberg via Actions workflow with token-based auth. -""" -artefacts = [".github/workflows/mirror.yml", "MIRROR_SETUP.adoc"] - -[[standing-decisions]] -id = "sd-004" -title = "Cross-platform compatibility: Linux primary, Windows secondary" -status = "accepted" -date = "2026-04-28" -rationale = """ -User works across two machines (Fedora Kinoite primary, Windows for -travel). Build instructions must be path-agnostic; line endings -normalised via .gitattributes. -""" -artefacts = [".gitattributes"] - -[[standing-decisions]] -id = "sd-005" -title = "Recipe extension parked for v0.2+, NOT v0.1.x scope" -status = "accepted" -date = "2026-04-29" -rationale = """ -The positive-termination route — extending the recipe to allow coupled -state across axes or multiple live positions per axis — is genuinely -separate work, not unfinished EI-2 business. It would require new -modules, not a rerun of EI-2. -""" -when-active = "When v0.2 work begins, file as a new question (e.g., EI-3) rather than reopening EI-2." - -[[standing-decisions]] -id = "sd-006" -title = "Two-document-family doc surface: Reading 1 and Reading 2 patches superseded" -status = "accepted" -date = "2026-04-29" -rationale = """ -Both candidate readings drafted during EI-2 investigation (READING 1: -weaken gate-1 with NLO precondition; READING 2: refine recipe with NLO -precondition) were superseded by the stronger-negative trajectory found -via RoleRole.agda. Files kept as historical record only; SUPERSEDED -banners applied. -""" -superseded-files = [ - "docs/EI2_READING1_PATCHES.adoc", - "docs/EI2_READING2_PATCHES.adoc", - "docs/EI2_READINGS_COMPARISON.adoc", -] - -# ============================================================ -# Artefacts produced during EI-2 (canonical file list) -# ============================================================ - -[artefacts] -agda-characteristic-lane = [ - "proofs/agda/characteristic/RoleGraded.agda", # original EI-1 closure - "proofs/agda/characteristic/RoleMode.agda", # phase 3 sibling - "proofs/agda/characteristic/ModeGraded.agda", # phase 2 sibling (note trailing 'd') - "proofs/agda/characteristic/RoleModeGrade.agda", # 3D obligation 4 - "proofs/agda/characteristic/RoleRole.agda", # phase 5 critical test - "proofs/agda/characteristic/InteractionTest.agda", # phase 4 simultaneity obstacle - "proofs/agda/characteristic/RecipeSpec.agda", # phase 5 recipe-as-record - "proofs/agda/characteristic/RecipeTheorem.agda", # partial generic, per-axis halves - "proofs/agda/characteristic/RecipeNonTriviality.agda", # concrete construction halves (PATH B) - "proofs/agda/characteristic/ChoreoInjective.agda", # NLO certificate for Choreo - "proofs/agda/characteristic/IntegrationAudit.agda", # EI-1 falsifier exhibit - "proofs/agda/characteristic/VisibleConstraintAudit.agda", -] -docs = [ - "docs/EI2_REPORT.adoc", # authoritative report (top Status section) - "docs/EI2_READING1_PATCHES.adoc", # superseded - "docs/EI2_READING2_PATCHES.adoc", # superseded - "docs/EI2_READINGS_COMPARISON.adoc", # superseded - "docs/next-questions.adoc", # EI-2 closed section -] -modified = [ - "docs/gate-1-distinct-phenomenon.adoc", # § The Gate #1 claim narrowed - "docs/gate-2-handoff.adoc", # § Observation G updated - "docs/adjacency/README.adoc", # EI-2 cascade note - "roadmap-gates.adoc", # § Gate 1 Claim narrowed - "README.md", # integration-bridge bullet updated -] -integration-tracking = ["INTEGRATION_COMMITS.adoc"] # 7 commits, EI-2 termination = commit 7 -staging-area = "/mnt/user-data/outputs/audit-output/" - -# ============================================================ -# Documentation cascade applied (where the narrowed claim lives) -# ============================================================ - -[[cascade-applied]] -file = "docs/gate-1-distinct-phenomenon.adoc" -section = "§ The Gate #1 claim" -change = "Distinctness rerouted to truncation + 2-cell arguments; integration explicitly removed from distinctness load." - -[[cascade-applied]] -file = "docs/gate-2-handoff.adoc" -section = "§ Observation G" -change = "Recipe characterised as organising vocabulary; EI-2 finding recorded in NOTE block; NLO-vs-loss-only column added to instances table." - -[[cascade-applied]] -file = "roadmap-gates.adoc" -section = "§ Gate 1 Claim" -change = "Same narrowing as gate-1-distinct-phenomenon.adoc." - -[[cascade-applied]] -file = "docs/adjacency/README.adoc" -section = "Where the wins live (NOTE after table)" -change = "EI-2 cascade note added explaining recipe-vs-2-cell-level distinction." - -[[cascade-applied]] -file = "README.md" -section = "integration-bridge bullet in feature list" -change = "Updated to reflect recipe as organising vocabulary, with link to EI2_REPORT." - -[[cascade-applied]] -file = "docs/next-questions.adoc" -section = "§ Closed questions" -change = "Full EI-2 entry with seven-data-point evidence table, file list, and termination rationale." - -# ============================================================ -# Do-not-redo register (anti-duplicate-work checklist) -# ============================================================ - -[[do-not-redo]] -item = "Build a fourth 2D sibling construction with NLO criterion to test recipe-non-triviality" -resolution = "Done in spirit: RoleRole.agda showed even Choreo×Choreo doesn't help. Adding a fourth pair would not change the structural finding." - -[[do-not-redo]] -item = "Draft READING 1 (weaken gate-1) or READING 2 (refine recipe) doc patches" -resolution = "Both drafted and superseded. SUPERSEDED banners on EI2_READING{1,2}_PATCHES.adoc." - -[[do-not-redo]] -item = "Attempt to formalise the full recipe-non-triviality 2D iff theorem in safe Agda" -resolution = "Documented as not formalisable without postulates (decidable equality, F-collapses axioms, extensionality). PATH B accepted partial formalisation." - -[[do-not-redo]] -item = "Re-run RoleGraded with a different family choice F : Role × Grade → Set" -resolution = "Three structural choices were evaluated; the negative finding is family-independent." - -[[do-not-redo]] -item = "Re-investigate whether Choreo's transport is genuinely non-loss-only" -resolution = "Formal certificate exists: client-to-server-injective-on-proj₁ in ChoreoInjective.agda. Do not redo." - -[[do-not-redo]] -item = "Open a new EI-2 entry to track the recipe extension" -resolution = "Recipe extension is genuinely separate work; track as a new question (e.g., EI-3) when v0.2 work begins, not as EI-2 reopening." - -[[do-not-redo]] -item = "Add ModeGrade.agda (without trailing 'd')" -resolution = "ModeGraded.agda (with trailing 'd') is canonical. The duplicate without trailing 'd' was created in error during this session and removed." - -# ============================================================ -# Forbidden rebrandings (to prevent recurrence under new names) -# ============================================================ - -[forbidden-rebrandings] -entries = [ - "the integration argument carries gate-1's distinctness load", - "the recipe is uniformly applicable across all 2D axis pairs", - "non-loss-only is sufficient for substantive simultaneous interaction", - "five axes simultaneously as a distinctness claim", - "Mode × Grade is a falsifier in some weaker sense", - "Role × Role would have produced substantive content with a better family choice", -] - -# ============================================================ -# Blockers (honest, as of 2026-06-12) -# ============================================================ - -[blockers] -ordinal-gate-1 = "Tail-rank-equality discharge for the cross-head rank-equal case — structural blocker; both pre-identified unblock routes CHECKED-REFUTED in PR #146." -release = "v0.1.1 not yet tagged; CHANGELOG remains [Unreleased]." -pillar-e = "paper.adoc [EXPAND] tags remain; venue/template + Zenodo DOI + outreach are author-driven (do not auto-run)." -estate-license-review = "PR #185 was merged as DRAFT-titled estate standardization pending owner-only LICENSE review; LICENSE SPDX header already restored post-merge." - -# ============================================================ -# Next actions (post-termination gate-1/gate-2/gate-3 work that -# remains open and is NOT EI-2 follow-up) -# ============================================================ -# Updated 2026-05-20 (status notes carried forward at the 2026-06-05 -# and 2026-06-12 refreshes): the April 2026 next-actions list is largely -# superseded by intervening session activity. Resolutions: -# * `integration` (apply 7-commit integration sequence) — DONE, -# long since merged. -# * `t-3` (Gate-1 falsification test 3) — superseded by the Gate 1 -# adjacency refresh (decisions/gate1-adjacency-refresh.adoc, PR #77) -# which closed gate-1 work at 5/5 REFINED. -# * `q2-4` (falsifier attempts) — partially absorbed into -# IntegrationAudit.agda EI-2 negative result; further falsifier -# attempts are now bookkeeping not load-bearing. -# * `q2-1` (echo-not-prop generalisation) — still open. -# * `q2-3` (RoleGraded as N5) — still open (low priority). -# * `v0-2-recipe-extension` — still parked. - -[[next-actions]] -id = "q2-1" -title = "Generalisation of echo-not-prop" -status = "open" -priority = "high" -relevance = """ -n=2 special case proofs generalise to: for non-injective f with at least -two distinct preimages of y, is-prop (Echo f y) → ⊥. Closing this also -discharges the truncation-argument gap for refinement, IFC, and -provenance adjacency notes. -""" -rationale = "Truncation argument is one of the two load-bearing distinctness arguments post-EI-2; strengthening it has high leverage." - -[[next-actions]] -id = "q2-3" -title = "Adopt RoleGraded.choreo-grade-commute as nominee N5" -status = "open" -priority = "low" -relevance = "Gate-2's audit flagged it as candidate fifth nominee but did not adopt. Adoption pushes the audit count to 5-of-5 across four constructions." -note = "Mostly bookkeeping post-EI-2 since the recipe is no longer the distinctness locus." - -[[next-actions]] -id = "owner-gated-paper-update" -title = "Bounded new-contribution paragraph in paper.adoc / types-abstract.adoc / conservativity.adoc for F1+F3" -status = "owner-gated" -priority = "deferred" -relevance = """ -F1 + F3 (see META adr-007, adr-008) introduce a separate graded-comonad -construction beside EchoGraded. The paper bodies are about EchoGraded's -thin-poset structure — the title and central thesis should not move on -these gates alone. Whether to add a bounded contribution paragraph -mentioning the F1/F3 side-construction is an editorial decision. -""" - -[[next-actions]] -id = "ordinal-track-path-1" -title = "Ordinal track Path-1 — Brouwer rank-mono into _<ᵇ⁻_" -status = "substantially-landed" -priority = "high" -relevance = """ -Substantially advanced by the Slice 3+4 Route A arc (PRs #165-#171, -2026-05-30) — see [current-workstream]. The rank-mono union umbrella -RankMonoUnion._<ᵇᵘ_ + its WfCNF wrap landed, and well-foundedness -wf-<ᵇᵘ via rank-embedding transport closed Gate 2 (#170). -""" -remaining = """ -Gate 1 (tail-rank-equality discharge for the cross-head rank-equal case) -remains OPEN — structural blocker, both pre-identified unblock routes -CHECKED-REFUTED in PR #146. Gate 3 (Path-4+ further source-rule -extensions) is OPEN but mechanical via the documented recipe. -""" - -[[next-actions]] -id = "v0-2-recipe-extension" -title = "Recipe extension exploration (parked)" -status = "parked-v0.2" -priority = "deferred" -relevance = "Coupled state across axes; multiple live positions per axis. New module work, not a re-investigation of EI-2." - -# ============================================================ -# Pillar F earn-back closure summary (2026-05-20) -# ============================================================ -# The Pillar F earn-back programme launched by R-2026-05-18 is CLOSED. -# All four gates passed at strictly-bounded strength; see META -# adr-{007,008,009} and docs/retractions.adoc follow-ups F-2026-05-18a -# + F-2026-05-20a + F-2026-05-20b. - -[earn-back-summary] -status = "closed" -closing-date = "2026-05-20" -scope-qualifier = """ -F1+F3 earn back the graded-comonad and two-models claims FOR A NEW -SIDE-CONSTRUCTION. EchoGraded remains a thin-poset reindexing modality -per R-2026-05-18; EchoRelModel's two-models claim remains retracted. -Different abstract interfaces; not interconvertible. -""" -forbidden-rebrandings = [ - "EchoGraded is a graded comonad", - "the F1 construction reinstates EchoGraded's retracted comonad claim", - "the F3 two-models result reinstates EchoRelModel's retracted two-models claim", - "the title or central thesis of paper.adoc moves on F1 or F3 alone", -] -unmoved-retractions = [ - "R-2026-05-18 finding 5 (conservativity metatheorem) — stays retracted; no gate attempted to earn it back, no gate could (meta-statement over all propositions, not discharged by typechecking)", - "R-2026-05-18 finding 3 (\"Not two models\" for EchoRelModel/GCLaws) — stays retracted; F3 earned a different two-models claim at a different interface", -] - -[earn-back-summary.gates.F4] -status = "passed" -date = "2026-05-18" -module = "proofs/agda/EchoPullbackUnivF4.agda" -claim = "Terminal-cone universal property as a function of an explicit funext module parameter, never a postulate" -retraction-followup = "F-2026-05-18a" - -[earn-back-summary.gates.F2] -status = "passed" -date = "2026-05-18" -module = "proofs/agda/EchoStepNDModelF2.agda" -claim = "Genuine second model of the bare Echo functor on the non-graph relation StepND; content-bearing agreement" -retraction-followup = "F-2026-05-18a" - -[earn-back-summary.gates.F1] -status = "passed" -date = "2026-05-20" -module = "proofs/agda/EchoGradedComonadF1.agda" -claim = "Monoid-graded iterated-residue comonad at (ℕ, +, 0) with Echo as grade-unit object; nested δ; all three comonad laws; D2-nontrivial separating witness" -retraction-followup = "F-2026-05-20a" -adr = "adr-007" - -[earn-back-summary.gates.F3] -status = "passed" -date = "2026-05-20" -modules = [ - "proofs/agda/EchoGradedComonadInterface.agda", - "proofs/agda/EchoGradedComonadInstance1.agda", - "proofs/agda/EchoGradedComonadInstance2.agda", -] -claim = "Abstract GradedComonadStructure record (no ⊑-prop-equivalent field) + two non-isomorphic-grade-monoid instances: nat-instance at commutative (ℕ, +, 0), list-instance at non-commutative free monoid (List Tag, ++, [])" -retraction-followup = "F-2026-05-20b" -adr = "adr-008" - -# ============================================================ -# Theory-work closure summary (2026-05-20) -# ============================================================ -# The §"Theory work — no proof assistant needed" section in -# docs/echo-types/roadmap.md is empty. Every item is landed, ruled out, -# or refreshed. - -[theory-work-summary] -status = "closed" -closing-date = "2026-05-20" -closure-prs = [67, 68, 69, 70, 71, 72, 74, 75, 76, 77, 78, 79, 82, 84, 86, 88, 90, 91, 92] - -[theory-work-summary.axes-fully-mechanised] -axis-2-approximate-echo = "EchoApprox.agda + EchoApproxInstance.agda; Rung C BalancedTolerance at #78" -axis-8-decidability = "EchoDecidable.agda" -axis-8-cost = "EchoCost.agda + EchoCostInstance.agda (PR #85)" -axis-8-access = "EchoAccess.agda (PRs #68, #75)" -axis-8-search = "EchoSearch.agda + EchoSearchInstance.agda (PR #80)" -negative-coecho = "AntiEcho.agda (PR #69) + AntiEchoTropical.agda (PR #72) + AntiEchoTropicalGeneric.agda (PR #91) + antiecho-partition-dec (PR #90)" - -[theory-work-summary.ruled-out] -two-categorical-shape = "decisions/no-2-cat.adoc — every would-be 2-cell is refl or forced trivial" - -[theory-work-summary.refreshed] -presentation-dependence-cluster = "decisions/presentation-dependence.adoc — examples 5, 9, 10 cluster; meta-pattern only, no new module needed" -gate-1-adjacency-refresh = "decisions/gate1-adjacency-refresh.adoc — 5/5 REFINED, 0 RE-EVALUATE" - -[theory-work-summary.canonical-examples-cluster] -example-5-database-provenance = "EchoExampleProvenance.agda (PR #81)" -example-9-parser = "EchoExampleParser.agda (PR #83)" -example-10-abstract-interp = "EchoExampleAbsInt.agda (PR #82)" -example-6-numeric = "still unblocked, only remaining example item" - -# ============================================================ -# END OF STATE -# ============================================================ diff --git a/.machine_readable/agent_instructions/README.adoc b/.machine_readable/agent_instructions/README.adoc index b9f1222..531fc3a 100644 --- a/.machine_readable/agent_instructions/README.adoc +++ b/.machine_readable/agent_instructions/README.adoc @@ -1,47 +1,13 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Agent Instructions (echo-types) -:toc: preamble +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += `.machine_readable/agent_instructions/` — retired -Methodology-aware configuration for AI agents working on echo-types. Read by -any AI agent (Claude, Gemini, Copilot, etc.) at session start, alongside the -top-level `CLAUDE.md` (which carries the authoritative current-rung-state) and -`.machine_readable/6a2/`. +The `.a2ml` records that lived here were removed on 2026-09-30 by owner +ruling: the `.a2ml` surface is retired in favour of `.deed` records. -== Files +The last tree that held them is frozen at +https://github.com/hyperpolymath/echo-types/tree/39a7a99cbe19a918843e9624010510b5fc3b8366/.machine_readable/agent_instructions[commit 39a7a99]. +Read that copy for history; do not recreate `.a2ml` files here. -[cols="1,3"] -|=== -| File | Purpose - -| `methodology.a2ml` -| Default mode, the proof-discipline invariants (`--safe --without-K`, zero - postulates, ceilings), priority weights, convergent budget, known constraints. - -| `coverage.a2ml` -| Session coverage tracking — which workstreams/modules were visited, what was - skipped, what has open MUSTs. - -| `debt.a2ml` -| Meander debt — proof obligations and chores found but not discharged, carried - between sessions. -|=== - -== How Agents Use These - -1. Read `CLAUDE.md` first — it has the live rung-state and the "DO NOT reopen" lists. -2. Read `methodology.a2ml` — know mode, invariants, ceilings. -3. Read `coverage.a2ml` and `debt.a2ml` — know what was visited and what is outstanding. -4. At session end, update `coverage.a2ml` and `debt.a2ml`, and (on a landed rung) - the `CLAUDE.md` current-rung-state + the `6a2/STATE.a2ml` current-state block. - -== Relationship to Other Files - -* `6a2/AGENTIC.a2ml` says WHAT agents can do (gating, escalation, redo-traps). -* `agent_instructions/` says HOW agents should work (methodology). -* `bot_directives/` says what the gitbot-fleet / Hypatia does (fleet-specific). -* `CLAUDE.md` says how Claude specifically should work (Claude-specific, authoritative state). - -== Reference - -ADR-002 in `standards/agentic-a2ml/docs/ADR-002-methodology-layer.adoc`. +Conversion to `.deed` is tracked estate-wide in +https://github.com/hyperpolymath/rsr-template-repo/issues/209[rsr-template-repo#209]. diff --git a/.machine_readable/agent_instructions/coverage.a2ml b/.machine_readable/agent_instructions/coverage.a2ml deleted file mode 100644 index 3ecd4a4..0000000 --- a/.machine_readable/agent_instructions/coverage.a2ml +++ /dev/null @@ -1,72 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# coverage.a2ml — Session coverage tracking (echo-types) -# Updated at the end of each AI agent session. -# Tracks which workstreams/modules were visited and which have open MUSTs. -# -# Reference: ADR-002 in standards/agentic-a2ml/docs/ - -[metadata] -version = "1.0.0" -last-updated = "2026-06-12" - -# ============================================================================ -# COVERAGE STATE -# ============================================================================ -# "Components" here = the three workstreams + the cross-repo bridge surface. -# Authoritative per-rung detail lives in CLAUDE.md current-rung-state. - -[coverage] -total-components = 4 -visited-components = 4 -coverage-percent = 100 -note = "All three workstreams + the bridge ledger have current status; the open work is named in debt.a2ml." - -# ============================================================================ -# VISITED COMPONENTS (workstream → last-known status) -# ============================================================================ - -[coverage.visited.composition-track] -date = "2026-04-28" -status = "landed" -notes = "Echo-comp-iso + cancel-iso + pentagon (Echo-comp-pent-Σ-assoc) all packaged as _↔_." - -[coverage.visited.ordinal-track] -date = "2026-05-30" -status = "partial" -notes = "Slice 3+4 Route A arc (PRs #165-#170): RankMonoUnion umbrella + wf of _<ᵇᵘ_ via rank-embedding transport (#170). Target: Bachmann-Howard." - -[coverage.visited.establishment-track] -date = "2026-05-27" -status = "partial" -notes = "Pillars A-D complete (2026-05-17); Pillar F closed (2026-05-20); Tier-1+2+3 spine + audience moves + EchoCanonicalIdentitySuite. Pillar E open." - -[coverage.visited.cross-repo-bridges] -date = "2026-06-02" -status = "ledgered" -notes = "cross-repo-bridge-status.md current: CNO done, Ephapax NARROW, EchoTypes.jl shipped, Janus name-only, Tropical citation-level, Valence/Ochrance exploratory." - -# ============================================================================ -# SKIPPED / OPEN MUSTS (P1 inputs for next session's Phase 0) -# ============================================================================ - -[coverage.skipped-musts.ordinal-unbudgeted-wf] -priority = "P1" -issue = "Unbudgeted _<ᵇʳᶠ_ global WF — eliminate the ℕ budget from wf-<ᵇʳᶠᵇ without leaving --safe --without-K. Solo, not swarmable; named next bottleneck." -discovered = "2026-05-20" - -[coverage.skipped-musts.full-buchholz-constructor-set] -priority = "P2" -issue = "K-limited shared-binder cases (<ᵇ-ψα, <ᵇ-+2) beyond the admitted core; push surface-route WF back into Order.agda's main _<ᵇ_." -discovered = "2026-04-28" - -# ============================================================================ -# CHERRY-PICKING AUDIT (accountability for the weighted priority system) -# ============================================================================ -# At session end agents report whether they chose easy work over hard work. -# -# [coverage.cherry-picking] -# easy-high-completed = 0 -# hard-high-completed = 0 -# assessment = "..." diff --git a/.machine_readable/agent_instructions/debt.a2ml b/.machine_readable/agent_instructions/debt.a2ml deleted file mode 100644 index d9a6170..0000000 --- a/.machine_readable/agent_instructions/debt.a2ml +++ /dev/null @@ -1,116 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# debt.a2ml — Meander debt list (echo-types) -# Proof obligations and chores found but not discharged. Carried between -# sessions; becomes the next session's Phase 0 input. -# -# Items are consumed (removed) when discharged. New items added at session end. -# -# Reference: ADR-002 in standards/agentic-a2ml/docs/ - -[metadata] -version = "1.0.0" -last-updated = "2026-06-14" - -# ============================================================================ -# OUTSTANDING PROOFS — the live frontier (single inventory, 2026-06-14) -# -# Status legend: -# OPEN-EXTERNAL — mechanisable, but needs new external mathematics -# (no in-repo route exists yet). -# WALLED — proven not closable on the current object under -# --safe --without-K; close-out is a falsifiable verdict. -# OPEN-DESIGN — closable, but gated on a substantial design decision -# (e.g. truncation / Cubical). -# MECHANICAL — closable now, bounded, no new ideas needed. -# -# 2026-06-14 progress note: the two long-standing ordinal "should" -# items (unbudgeted _<ᵇʳᶠ_; K-limited shared-binder; surface-route WF) -# are now DONE in their ACHIEVABLE (sound-carrier) form — wf-<ᵇ², -# wf-<ᵇʳᶠ², wf-<ᵇ⁺² (PRs #208/#212/#214). What remains of them is the -# native-order form, which is WALLED. All four paper.adoc [EXPAND] -# tags are cleared (#215). The genuine remaining ordinal frontier is -# now order-type fidelity (D-2026-06-14). -# ============================================================================ - -# ============================================================================ -# SHOULD — would fix next wave -# ============================================================================ - -[[debt.should]] -component = "ordinal-track / Bachmann-Howard order-type fidelity" -issue = "Order-type fidelity: prove the well-formed Buchholz notation IS the Bachmann-Howard ordinal order, not merely well-founded. Either (a) a verified order-preserving denotation ‖·‖ : BT → 𝒪 of height ψ₀(Ω_ω) with s <ᵇ t iff ‖s‖ < ‖t‖ on the well-formed fragment, or (b) a direct order-type computation (fundamental sequences / collapsing-function correctness)." -status = "OPEN-EXTERNAL" -effort = "hard" -impact = "high" -discovered = "2026-06-14" -note = "Decision-log D-2026-06-14 (decisions/ordinal-bh-order-type-fidelity-open.adoc). The genuine remaining ordinal-strength frontier; WF (done, sound-carrier) is the prerequisite, not the result. Gates the Pillar E ordinal appendix's strong reading (the WF-milestone appendix is already written, #215)." - -[[debt.should]] -component = "ordinal-track / Order.agda (native _<ᵇ_)" -issue = "Global-native well-foundedness: unbudgeted wf-<ᵇʳᶠ AND the K-limited shared-binder cases (<ᵇ-ψα, <ᵇ-+2) over NATIVE _<ᵇ_ (not the sound carrier)." -status = "WALLED" -effort = "hard" -impact = "low" -discovered = "2026-04-28" -note = "Native _<ᵇ_ is ordinally unsound (the <ᵇ-+Ω counterexample); all five rank/direct/lex/tower/inverse-image routes are walled (RankBrouwer.agda preamble + buchholz-rank-obstruction.adoc), and rank2 does not escape it. The ACHIEVABLE (sound-carrier) forms are DONE: wf-<ᵇ² / wf-<ᵇʳᶠ² / wf-<ᵇ⁺². Realistic close-out for the native form is a FALSIFIABLE VERDICT, not a positive proof — write it when this item is next picked up." - -[[debt.should]] -component = "establishment-track / EchoImageFactorization (epi, mono)" -issue = "Image factorisation (epi, mono) earn-back requires propositional truncation. The postulated-interface placeholder lives in EchoImageFactorizationPropPostulated.agda (the tree's ONLY postulate; not in All.agda)." -status = "OPEN-DESIGN" -effort = "hard" -impact = "medium" -discovered = "2026-05-27" -note = "Cubical Agda (different --safe flag profile) OR a postulated ∥_∥ interface with scoped honest-scope. Substantial design decision; the (equivalence, projection) upper form is already done (Tier 1 + F5)." - -[[debt.should]] -component = "earn-back-track / examples/Transport.agda (Gate-3)" -issue = "Two disclosed open items in the transport/Gate-3 example, pending a K-free reformulation (coe-cong-R ∘ sym push). Stated in-file as precise OPENs." -status = "OPEN-DESIGN" -effort = "medium" -impact = "low" -discovered = "2026-05-20" -note = "See earn-back-plan.adoc; nothing is postulated — the items are honestly-stated gaps awaiting a K-free route." - -# ============================================================================ -# COULD — would fix eventually -# ============================================================================ - -[[debt.could]] -component = "establishment-track / decoration zoo" -issue = "Wire the remaining decoration modules (Cost / Search / Indexed / Epistemic) as ResidueForm / DecorationStructure instances; mechanical per-module work." -status = "MECHANICAL" -effort = "medium" -impact = "low" -discovered = "2026-05-27" - -[[debt.could]] -component = "establishment-track / Q2.1 truncation generalisation" -issue = "Generalise echo-not-prop: for non-injective f with two distinct preimages of y, is-prop (Echo f y) → ⊥. High-leverage for the truncation distinctness argument but currently low-priority." -status = "OPEN-DESIGN" -effort = "medium" -impact = "medium" -discovered = "2026-04-29" -note = "Shares the propositional-truncation design decision with the (epi, mono) earn-back; resolving one likely informs the other." - -[[debt.could]] -component = "rsr-conformance (root Intentfile)" -issue = "Pin @sha256: digests on stapeln.toml + Containerfile base images; resolve readme.adoc/README.md and roadmap.adoc/roadmap-gates.adoc duplication; migrate doc-format-rule .md → .adoc." -effort = "easy" -impact = "low" -discovered = "2026-04-28" - -[[debt.could]] -component = "cross-repo bridges / JanusKey" -issue = "Rewrite EchoJanusBridge.JanusOp from the 4-variant local enum to the 8-variant Idris2 OpKind (Copy/Move/Delete/Modify/Obliterate/KeyGen/KeyRotate/KeyRevoke); add IsFileOp/IsKeyOp analogues; re-pin in Smoke.agda." -effort = "medium" -impact = "low" -discovered = "2026-06-02" - -# ============================================================================ -# PARKED — explicitly out of scope (do not treat as debt to clear) -# ============================================================================ -# - Recipe extension (coupled state across axes): v0.2+, NOT EI-2 follow-up. File as EI-3 when v0.2 begins. -# - Full 2D iff for recipe-non-triviality: not formalisable in safe Agda without postulates (PATH B accepted). diff --git a/.machine_readable/agent_instructions/methodology.a2ml b/.machine_readable/agent_instructions/methodology.a2ml deleted file mode 100644 index 6cf2da4..0000000 --- a/.machine_readable/agent_instructions/methodology.a2ml +++ /dev/null @@ -1,114 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# methodology.a2ml — AI agent methodology configuration (echo-types) -# Declares how agents should approach work in this Agda proof library. -# Read at session start by any AI agent, alongside CLAUDE.md. -# -# Reference: ADR-002 in standards/agentic-a2ml/docs/ - -[metadata] -version = "1.0.0" -last-updated = "2026-06-12" -spec = "https://github.com/hyperpolymath/standards/blob/main/agentic-a2ml/docs/ADR-002-methodology-layer.adoc" - -# ============================================================================ -# MODE SELECTION -# ============================================================================ -# convergent: find gaps, fill them, build infrastructure -# divergent: find what's strongest, push it further (research/proof) -# hybrid: audit a slice of budget, then focus on top MUSTs -# -# echo-types is a research proof library: the default is divergent — deepen -# the structured-loss identity (canonical-identity spine, ordinal milestone), -# do not broaden into parallel formalisms. - -[methodology] -default-mode = "divergent" -ring-ceiling = 2 # Hard ceiling for ring expansion (0-3) -wave-cap = 2 # Max waves before requiring user "keep going" -spike-required = true # Every session must land verified Agda, not just designs - -# ============================================================================ -# PROOF INVARIANTS (the riverbanks — non-negotiable) -# ============================================================================ - -[methodology.proof-invariants] -safe-without-k = true # --safe --without-K on every module -postulate-ceiling = 0 # zero in load-bearing tracks (outside Ordinal/) -believe-me-ceiling = 0 # no believe_me / primTrustMe / primEraseEquality -escape-hatch-ceiling = 0 # no sorry / Admitted / unsafeCoerce / Obj.magic -escape-pragma-ceiling = 0 # no TERMINATING / NON_TERMINATING / allow-unsolved-metas -funext-policy = "explicit-parameter-only" # never a postulate; isolated from the trusted base -pin-every-headline = true # each headline pinned in Smoke.agda via `using` -wire-every-module = true # each module in All.agda; orphans are dead code -kernel-cone-guard = "scripts/kernel-guard.sh" - -# ============================================================================ -# PRIORITY WEIGHTS -# ============================================================================ -# MUST (3x): blocking current proof work → fix immediately -# SHOULD (2x): degrading quality of current work → fix if in zone -# COULD (1x): improving adjacent work → add to debt list - -[methodology.priority-weights] -must = 3 -should = 2 -could = 1 - -# ============================================================================ -# CONVERGENT BUDGET (when mode = convergent or hybrid) -# ============================================================================ - -[methodology.convergent-budget] -structural = 70 # new modules / proofs / wiring / Smoke pins -corrective = 20 # broken imports, stale doc tags, drift -perfective = 10 # SPDX headers, doc polish, formatting - -# ============================================================================ -# UNIQUE STRENGTH (when mode = divergent) -# ============================================================================ - -[methodology.unique-strength] -description = "Echo as the proof-relevant fiber of structured loss: Echo f y := Σ (x : A) , (f x ≡ y), characterised as a reindexing modality (coeffect/quantitative lineage). The strength is the machine-checked, --safe --without-K, postulate-free identity claim plus its honest matched-negatives." -deepen-not-broaden = true - -# ============================================================================ -# DIVERGENT INVARIANTS -# ============================================================================ -# Test before any divergent action: -# "Does this deepen the existing identity, or add a parallel strength?" -# If parallel → stop. Note as cross-project insight. - -[methodology.divergent-invariants] -rules = [ - "Agda only for the formal core — no Lean4 / Coq / Idris2 inside this repo (cross-prover work is citation-level bridges only).", - "Never weaken --safe or --without-K to land a proof.", - "Never introduce a postulate in a load-bearing track; exploratory truncation postulates, if any, go in docs/proof-debt.md and stay out of All.agda's trusted closure.", - "Honest scope: every identity claim ships with its matched-negatives; narrow-true beats broad-easy.", - "Do not reopen retracted claims (R-2026-05-18) or closed gates (Pillars A-D, F1-F4, EI-2).", -] -language-invariant = "agda" - -# ============================================================================ -# KNOWN CONSTRAINTS (help Phase 0 find the critical chain faster) -# ============================================================================ - -[methodology.known-constraints] -constraints = [ - "stdlib >= 2.3 is required (apt's 1.7.3 lacks Data.Product.Base) — see CLAUDE.md § Build.", - "The ordinal track is solo, not swarmable; the unbudgeted _<ᵇʳᶠ_ global WF is the named next bottleneck.", - "Multiple Claude sessions may run concurrently — respect declared territory; use `--only ` if both commit before sync.", - "Pillar E paper [EXPAND] tags are author-driven; the ordinal consumer-evidence appendix is gated on the Bachmann-Howard milestone.", -] - -# ============================================================================ -# STATE FILE VALIDATION -# ============================================================================ - -[methodology.state-validation] -reject-if-contains = ["{{PLACEHOLDER}}", "rsr-template-repo"] -reject-if-project-name-mismatch = true -staleness-threshold-days = 120 -authoritative-state = "CLAUDE.md (current-rung-state) + .machine_readable/6a2/STATE.a2ml (current-state block)" -fallback-files = ["roadmap-gates.adoc", "roadmap.adoc", "docs/echo-types/MAP.adoc", "README.md"] diff --git a/.machine_readable/anchors/ANCHOR.a2ml b/.machine_readable/anchors/ANCHOR.a2ml deleted file mode 100644 index 7acc9d4..0000000 --- a/.machine_readable/anchors/ANCHOR.a2ml +++ /dev/null @@ -1,94 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# ANCHOR.a2ml - authoritative anchor for the echo-types repository. -# Canonical identity + policy boundaries for downstream/satellite repos. - -[metadata] -version = "1.0.0" -last-updated = "2026-06-12" - -[anchor] -schema = "hyperpolymath.anchor/1" -repo = "hyperpolymath/echo-types" -authority = "upstream-canonical" - -purpose = [ - "Define canonical semantics and policy boundaries for the echo-types proof library.", - "Declare what downstream/companion repos (EchoTypes.jl, arghda-core) can extend but not redefine.", - "Provide a stable golden path and invariant contract for release readiness.", -] - -[identity] -id = "org.hyperpolymath.echo-types" -project = "echo-types" -kind = "library" # constructive Agda proof library -one-sentence = "Constructive Agda formalisation of fiber-based structured loss (\"echo types\"): Echo f y := Σ (x : A) , (f x ≡ y); --safe --without-K throughout." -domain = "formal-verification / type-theory" -status = "active" - -# Registry-assigned identity. echo-types has NOT yet been assigned a clade -# in the gv-clade-index registry; do not invent a UUID/clade. -[clade] -# TODO: assign via gv-clade-index registry (https://github.com/hyperpolymath/gv-clade-index). -# Until assigned, no CLADE.a2ml exists for this repo and these fields -# MUST stay as TODO rather than carrying fabricated values. -uuid = "TODO: assign via gv-clade-index registry" -primary = "TODO: assign via gv-clade-index registry" # candidate observation: a research / formal-verification clade -assigned = "TODO: assign via gv-clade-index registry" - -[semantic-authority] -policy = "canonical" - -owns = [ - "The Echo type definition and the structured-loss semantics (Echo f y := Σ (x : A) , (f x ≡ y)).", - "The composition / ordinal / establishment workstream invariants and gate discipline.", - "Reference theorem statements mirrored by companions (EchoTypes.jl is a falsifying shadow, NOT an authority).", -] - -[implementation-policy] -# echo-types is an Agda proof repo with shell/Guix/Just tooling around it. -allowed = ["Agda", "Scheme", "Nickel", "Shell", "Just", "AsciiDoc", "Markdown"] -forbidden = ["TypeScript", "Node.js", "npm", "Go", "Python", "Kotlin", "Swift"] - -[golden-path] -# No `just test` shortcut is assumed; the canonical smoke is the Agda build. -smoke-test-command = [ - "agda -i proofs/agda proofs/agda/All.agda", - "agda -i proofs/agda proofs/agda/Smoke.agda", - "scripts/kernel-guard.sh", -] - -success-criteria = [ - "All.agda and Smoke.agda both exit 0 under --safe --without-K.", - "Zero postulates in load-bearing tracks; no believe_me / sorry / Admitted / unsafeCoerce / Obj.magic.", - "kernel-guard.sh PASS (funext-free kernel cone = { Echo, EchoKernel }).", - "Every headline theorem pinned in Smoke.agda; every module wired into All.agda.", -] - -[satellite-policy] -must-pin-upstream = true -must-declare-authority = true -must-have-anchor = true -must-have-golden-path = true - -[semantic-authority-files] -core-definition = "proofs/agda/Echo.agda" -verified-suite = "proofs/agda/All.agda" -headline-pins = "proofs/agda/Smoke.agda" -roadmap-gates = "roadmap-gates.adoc" -establishment-plan = "docs/echo-types/establishment-plan.adoc" -ordinal-plan = "docs/echo-types/buchholz-plan.adoc" -cross-repo-bridges = "docs/bridges/cross-repo-bridge-status.md" - -[relationships] -# Verifiable from CLAUDE.md + cross-repo-bridge-status.md. No fabricated edges. -companions = [ - "org.hyperpolymath.echotypes-jl", # executable Julia shadow (v0.2.0, pinned e7dded6) - "org.hyperpolymath.arghda-core", # extracted proof-workspace engine (echo-types#159) -] -active-bridges = [ - "org.hyperpolymath.ephapax", # EchoEphapaxBridge.agda (L3, NARROW) - "org.hyperpolymath.absolute-zero", # EchoCNOBridge.agda (content-bridge done) -] -constellation = "org.hyperpolymath.panll" diff --git a/.machine_readable/bot_directives/README.adoc b/.machine_readable/bot_directives/README.adoc index ec4b4a9..98087d3 100644 --- a/.machine_readable/bot_directives/README.adoc +++ b/.machine_readable/bot_directives/README.adoc @@ -1,38 +1,13 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= Bot directives — echo-types -:toc: += `.machine_readable/bot_directives/` — retired -== Purpose +The `.a2ml` records that lived here were removed on 2026-09-30 by owner +ruling: the `.a2ml` surface is retired in favour of `.deed` records. -Per-repo directives for automated agents operating on -`hyperpolymath/echo-types`. These files tell bots what this repository -considers safe, what is forbidden, and which findings are already -adjudicated, so automated runs do not relitigate settled decisions or -touch protected surfaces. +The last tree that held them is frozen at +https://github.com/hyperpolymath/echo-types/tree/39a7a99cbe19a918843e9624010510b5fc3b8366/.machine_readable/bot_directives[commit 39a7a99]. +Read that copy for history; do not recreate `.a2ml` files here. -== Precedence - -. Maintainer instruction (see `MAINTAINERS.adoc`) — always wins. -. These directives. -. Bot built-in defaults. - -== Scope - -These directives apply to: - -* the *Hypatia* scanner (`hypatia.a2ml` — scanner config pointers and - accepted findings with reasons); -* the *gitbot fleet* (`gitbot-fleet.a2ml` — fleet roster, branch policy, - never-touch paths, per-bot constraints); -* *.git-private-farm propagation* (`git-private-farm.a2ml` — propagation - is currently disabled here; the file records the contract for if/when - an `instant-sync.yml` workflow is added). - -== Repo-specific ground rules (summary) - -* This is a proof repository: `proofs/`, `tutorial/`, `All.agda`, - `Smoke.agda`, and `.github/workflows/agda.yml` are bot-off-limits. -* CI green precedes merge; bots never auto-merge and never delete - branches. -* Escalation channel is an issue, not PR-comment spam. +Conversion to `.deed` is tracked estate-wide in +https://github.com/hyperpolymath/rsr-template-repo/issues/209[rsr-template-repo#209]. diff --git a/.machine_readable/bot_directives/git-private-farm.a2ml b/.machine_readable/bot_directives/git-private-farm.a2ml deleted file mode 100644 index 755907a..0000000 --- a/.machine_readable/bot_directives/git-private-farm.a2ml +++ /dev/null @@ -1,31 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# git-private-farm.a2ml — .git-private-farm propagation directives for -# echo-types. Net-new at the 2026-06-12 governance checkpoint per the -# estate bot_directives standard. - -[metadata] -repo = "echo-types" -last-updated = "2026-06-12" -owner = "hyperpolymath" - -[propagation] -enabled = false -# echo-types has NO .github/workflows/instant-sync.yml as of 2026-06-12 -# (workflows present: agda, codeql, governance, hypatia-scan, mirror, -# scorecard, secret-scanner). The keys below record the estate contract -# that applies if/when the workflow is added. -workflow = ".github/workflows/instant-sync.yml" # absent; enabled = false until it exists -target = "hyperpolymath/.git-private-farm" -event-type = "propagate" -secret-name = "FARM_DISPATCH_TOKEN" # secret NAME only; value lives in repo secrets -presence-gated = false # no workflow present, so no gate exists yet; gate it on addition - -[never-propagate] -items = [ - "secrets", - "unmerged branches", - "work-in-progress", -] - -[on-token-rotation] -command = "gh secret set FARM_DISPATCH_TOKEN --repo hyperpolymath/echo-types" # name only; paste the new value when prompted diff --git a/.machine_readable/bot_directives/gitbot-fleet.a2ml b/.machine_readable/bot_directives/gitbot-fleet.a2ml deleted file mode 100644 index 91c0a96..0000000 --- a/.machine_readable/bot_directives/gitbot-fleet.a2ml +++ /dev/null @@ -1,62 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# gitbot-fleet.a2ml — gitbot fleet directives for echo-types. -# Net-new at the 2026-06-12 governance checkpoint per the estate -# bot_directives standard. - -[metadata] -repo = "echo-types" -last-updated = "2026-06-12" -owner = "hyperpolymath" - -[fleet] -bots = ["rhodibot", "echidnabot", "sustainabot", "glambot", "seambot", "finishbot"] - -[fleet.roles] -rhodibot = "git operations" -echidnabot = "code quality" -sustainabot = "dependency updates" -glambot = "documentation" -seambot = "integration" -finishbot = "task completion" - -[branch-policy] -working-branch-pattern = "/" # human sessions use session/; bots use their own prefix -draft-PRs-only = true -ci-green-before-merge = true # repo-level discipline: admin-merge-before-CI-green is a recorded anti-pattern (CLAUDE.md, PR #133 note) -never-touch = [ - ".claude/CLAUDE.md", - "CLAUDE.md", - "proofs/", - "tutorial/", - "*.agda", - ".github/workflows/agda.yml", - "docs/retracted/", -] - -# ============================================================ -# Per-bot constraints where this repo gives specific reason; -# defaults apply otherwise. -# ============================================================ - -[per-bot.rhodibot] -deny = ["force-push to main", "branch deletion", "history rewrites"] -note = "History is append-only here; superseded docs get SUPERSEDED banners, reverts are git-revert." - -[per-bot.echidnabot] -deny = ["editing proof code", "introducing postulates", "weakening --safe --without-K"] -note = "Code quality in this repo is gated by the Agda typechecker + scripts/kernel-guard.sh + tools/check-guardrails.sh; the only sanctioned postulates are the enumerated proof-debt module (docs/proof-debt.md)." - -[per-bot.sustainabot] -allow = ["GitHub Actions group bumps (precedent: PRs #179 and the codeql-action bump)"] -deny = ["bumping the Agda or agda-stdlib pins without a green full-suite run"] -note = "CI installs agda-stdlib v2.3 (see .github/workflows/agda.yml); the proof suite is the compatibility gate." - -[per-bot.glambot] -deny = ["resurrecting anything under docs/retracted/", "moving claims past the R-2026-05-18 narrowings"] -note = "Docs are AsciiDoc by convention (README.md is the GitHub-render exception and the canonical README after the 2026-06-12 dedup). Honest labels (Landed/Partial/Open) per CLAUDE.md." - -[per-bot.seambot] -note = "Cross-repo bridge edits follow docs/echo-types/cross-repo-bridge-status.md; bridge stubs are NARROW by design (META adr-011) — do not widen scope mechanically." - -[per-bot.finishbot] -note = "Task completion must respect the repo's gate ledger (docs/echo-types/earn-back-plan.adoc, roadmap-gates.adoc); gates pass only with explicit ledger entries, never silently." diff --git a/.machine_readable/bot_directives/hypatia.a2ml b/.machine_readable/bot_directives/hypatia.a2ml deleted file mode 100644 index 53ca436..0000000 --- a/.machine_readable/bot_directives/hypatia.a2ml +++ /dev/null @@ -1,74 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# hypatia.a2ml — Hypatia scanner directives for echo-types. -# Net-new at the 2026-06-12 governance checkpoint per the estate -# bot_directives standard. - -[metadata] -repo = "echo-types" -last-updated = "2026-06-12" -owner = "hyperpolymath" - -[scanner] -ignore-file = ".hypatia-ignore" # present at repo root; each entry carries a verified-false-positive rationale -workflow = ".github/workflows/hypatia-scan.yml" - -# ============================================================ -# Accepted findings (known false positives / adjudicated advisories). -# Each entry mirrors an in-repo rationale; do not re-raise these. -# ============================================================ - -[[accepted-findings]] -rule = "code_safety/agda_postulate" -path = "proofs/agda/Smoke.agda" -status = "verified-false-positive" -reason = """ -The rule is a naive \\bpostulate\\b regex over raw file content that does -not strip comments. The only 'postulate' tokens in Smoke.agda are in -comments documenting the suite's postulate-free discipline; there is no -postulate declaration. The repo's own guardrail (tools/check-guardrails.sh) -strips comments before checking and is the real gate. Suppressed in -.hypatia-ignore with full rationale. -""" - -[[accepted-findings]] -rule = "code_safety/js_http_url_in_code" -path = "tools/banner/build-banner.mjs" -status = "verified-false-positive" -reason = """ -The flagged http:// is the SVG XML namespace identifier -xmlns="http://www.w3.org/2000/svg" — a constant namespace URI never -dereferenced over the network; changing it to https would be semantically -wrong and break SVG handling. Not CWE-319. Suppressed in .hypatia-ignore. -""" - -[[accepted-findings]] -rule = "code_safety/agda_postulate" -path = "proofs/agda (Exploratory cohort)" -status = "scope-narrowed" -reason = """ -The agda_postulate alert on the Exploratory module was scope-narrowed via -inline allow in PR #156. The four propositional-truncation postulates in -proofs/agda/EchoImageFactorizationPropPostulated.agda are enumerated -proof debt under Disposition (c) NECESSARY AXIOM (docs/proof-debt.md, -PR #172); the module is isolated and not imported by All.agda/Smoke.agda. -""" - -[[accepted-findings]] -rule = "workflow hardening (general)" -path = ".github/workflows/" -status = "resolved-at-source" -reason = """ -PR #178 hardened CI workflows and resolved the then-outstanding Hypatia -findings at source rather than by suppression. New findings in workflows -should be fixed at source in the same spirit, not added here. -""" - -# ============================================================ -# Prohibited actions -# ============================================================ - -[prohibited-actions] -auto-delete-branches = false -auto-merge = false -modify-workflows = false -escalation = "open an issue, do not spam PR comments" diff --git a/.machine_readable/contractiles/Adjustfile.a2ml b/.machine_readable/contractiles/Adjustfile.a2ml deleted file mode 100644 index 6f01e89..0000000 --- a/.machine_readable/contractiles/Adjustfile.a2ml +++ /dev/null @@ -1,72 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Adjustfile — Drift-tolerance contract for rsr-template-repo -# Author: Jonathan D.A. Jewell -# -# Cumulative-drift catchment: tolerance bands + corrective actions. -# Authority: advisory (Yard) — continue-with-warnings; auto_fix where deterministic. -# Run with: adjust check -# Fix with: adjust fix (applies deterministic patches; advisory otherwise) - -@abstract: -Drift tolerances and corrective actions for rsr-template-repo. Unlike -MUST (hard gate), ADJUST tracks cumulative drift against tolerance bands -and proposes corrective actions. Advisory — it warns and trends, it does -not block. -@end - -## Template Drift - -### placeholder-drift -- description: Template placeholders should be replaced when copied -- tolerance: 0 placeholder markers in copied repos -- corrective: Search and replace all {{PLACEHOLDER}} markers -- severity: advisory -- notes: This check only applies to repos that copied from this template - -### template-version-drift -- description: Template version should match RSR spec version -- tolerance: Template version matches current RSR spec -- corrective: Update template to match latest RSR spec -- severity: advisory - -## Documentation Drift - -### readme-completeness -- description: README should document all template features -- tolerance: README covers all contractiles and directory structure -- corrective: Update README.adoc with missing sections -- severity: advisory - -### example-accuracy -- description: Examples in documentation should match actual template content -- tolerance: All code examples in docs are accurate -- corrective: Audit and fix examples in documentation -- severity: advisory - -## Structural Drift - -### contractile-sync -- description: All contractiles should have matching a2ml and ncl implementations -- tolerance: Every .a2ml has a corresponding .ncl -- corrective: Generate missing .ncl files from .a2ml -- severity: advisory - -### no-broken-symlinks -- description: No broken symbolic links in template structure -- tolerance: 0 broken symlinks -- corrective: Run symlink-check script -- severity: advisory - -## Accessibility Drift - -### adoc-not-md -- description: Template docs should prefer AsciiDoc -- tolerance: New prose docs are *.adoc -- corrective: Convert any new *.md to *.adoc -- severity: advisory - -### spdx-header-consistency -- description: All template files have correct SPDX headers -- tolerance: 0 files missing SPDX-License-Identifier -- corrective: Add SPDX headers to files that need them -- severity: advisory diff --git a/.machine_readable/contractiles/Bustfile.a2ml b/.machine_readable/contractiles/Bustfile.a2ml deleted file mode 100644 index 8b47969..0000000 --- a/.machine_readable/contractiles/Bustfile.a2ml +++ /dev/null @@ -1,100 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Bustfile.a2ml — breakage contract for echo-types: what counts as a -# busted state, how it is detected, and how to respond. -# -# Format: TOML-A2ML (parses with tomllib; `#` comments, [section], key = "value") -# -# Provenance: the flat-contractile completion of the estate layout -# (PR #185 supplied Adjustfile/Intentfile/Justfile/Mustfile/Trustfile but -# no Bustfile, and no nested bust/ contractile ever existed in this repo -# or its visible siblings). Written fully from repo-true obligations on -# 2026-06-12: the busted-state definitions, detection commands, and -# response ladder below are the repo's own existing gates (Agda suite, -# kernel-guard, guardrail scripts, CI workflows), not new policy. - -[bustfile] -version = "1.0.0" -format = "a2ml" -repo = "echo-types" -last-updated = "2026-06-12" - -# ============================================================ -# Busted-state definition (any one of these means the repo is busted) -# ============================================================ - -[definition] -busted-states = [ - "proofs/agda/All.agda fails to typecheck under --safe --without-K", - "proofs/agda/Smoke.agda fails to typecheck (a pinned headline theorem broke)", - "a postulate appears outside the enumerated proof-debt module (docs/proof-debt.md: proofs/agda/EchoImageFactorizationPropPostulated.agda)", - "scripts/kernel-guard.sh fails (kernel/derived classification drift)", - "tools/check-guardrails.sh fails (guardrail policy violation)", - "a retracted claim from docs/retractions.adoc reappears in canonical docs", - "main is red on the agda / governance / hypatia-scan workflows", -] - -# ============================================================ -# Detection (run these to decide whether the repo is busted) -# ============================================================ - -[[detection]] -name = "full-suite" -doc = "The verified suite: every module imported by All.agda typechecks." -run = "agda -i proofs/agda proofs/agda/All.agda" -severity = "critical" - -[[detection]] -name = "smoke-pins" -doc = "Every headline theorem pinned via `using` clauses still exists." -run = "agda -i proofs/agda proofs/agda/Smoke.agda" -severity = "critical" - -[[detection]] -name = "kernel-guard" -doc = "Kernel-vs-derived module classification is consistent (docs/echo-types/echo-kernel-note.adoc)." -run = "scripts/kernel-guard.sh" -severity = "high" - -[[detection]] -name = "guardrails" -doc = "Repo guardrail checks (incl. comment-stripping postulate check, the real postulate gate)." -run = "tools/check-guardrails.sh" -severity = "high" - -[[detection]] -name = "no-unsafe" -doc = "No unsafe escape hatches outside the documented exceptions." -run = "scripts/check-no-unsafe.sh" -severity = "high" - -# ============================================================ -# Response ladder (in order; stop at the first step that restores green) -# ============================================================ - -[response] -step-1 = "Do not merge anything while a critical detection fails on main; CI green precedes merge (admin-merges before CI green are a known anti-pattern in this repo's history — see CLAUDE.md PR #133 note)." -step-2 = "If the breakage is uncommitted local work: run the Dustfile source-rollback task (git checkout HEAD -- .) and clean-build, then re-run detection." -step-3 = "If the breakage landed on a branch: fix forward on that branch or close it as superseded at the next rung consolidation; never force-push over another session's work without re-fetching first." -step-4 = "If the breakage landed on main: git revert the offending commit (history is append-only; no force-push to main)." -step-5 = "Record the incident: open an issue with the failing command + output; if a proof rung was lost, note it in the session ledger per the CLAUDE.md rung-consolidation policy." - -[escalation] -owner = "hyperpolymath" -contact = "MAINTAINERS.adoc" -bot-rule = "automated agents open an issue and stop; they do not auto-revert main, do not auto-merge fixes, and do not spam PR comments" - -# ============================================================ -# Known exceptions (NOT busted states; do not 'fix' these) -# ============================================================ - -[[known-exceptions]] -name = "proof-debt-postulates" -detail = "The four propositional-truncation postulates in proofs/agda/EchoImageFactorizationPropPostulated.agda are enumerated proof debt under Disposition (c) NECESSARY AXIOM (docs/proof-debt.md, PR #172). The module is isolated, guardrail-exempt by design, and not imported by All.agda or Smoke.agda." - -[[known-exceptions]] -name = "hypatia-verified-false-positives" -detail = "The entries in .hypatia-ignore (agda_postulate on Smoke.agda comments; the SVG xmlns http:// constant in tools/banner/build-banner.mjs) are verified false positives with in-file rationale; see bot_directives/hypatia.a2ml." - -[[known-exceptions]] -name = "ordinal-track-open-gates" -detail = "Ordinal-track Gate 1 (tail-rank-equality discharge, CHECKED-REFUTED unblock routes per PR #146) and Gate 3 (Path-4+ extensions) are documented OPEN work, not breakage. See STATE [blockers]." diff --git a/.machine_readable/contractiles/Dustfile.a2ml b/.machine_readable/contractiles/Dustfile.a2ml deleted file mode 100644 index 3db792e..0000000 --- a/.machine_readable/contractiles/Dustfile.a2ml +++ /dev/null @@ -1,76 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Dustfile.a2ml — cleanup, hygiene & recovery contract for echo-types -# -# Format: TOML-A2ML (parses with tomllib; `#` comments, [section], key = "value") -# -# Provenance: the flat-contractile completion of the estate layout -# (PR #185 supplied Adjustfile/Intentfile/Justfile/Mustfile/Trustfile but -# no Dustfile). The [[tasks]] entries below PORT the full content of the -# pre-estate root `contractiles/Dustfile.a2ml` (S-expression form, -# deleted by PR #185); section shape follows the estate dust reference -# (nextgen-languages contractiles/dust/Dustfile.a2ml). Added 2026-06-12. - -[dustfile] -version = "1.0.0" -format = "a2ml" -repo = "echo-types" -last-updated = "2026-06-12" - -# ============================================================ -# Recovery & rollback tasks (ported from the pre-estate root Dustfile) -# ============================================================ - -[[tasks]] -name = "source-rollback" -doc = "Revert all source changes to last commit." -tag = "rollback" -cmd = "git checkout HEAD -- ." - -[[tasks]] -name = "clean-build" -doc = "Remove all build artifacts (Agda .agdai files)." -tag = "clean" -cmd = "find proofs -name '*.agdai' -delete" - -[[tasks]] -name = "resync-from-template" -doc = "Re-run scaffold-component.{py,my} to restore drifted boilerplate." -tag = "scaffold" -cmd = "echo 'Manual: run scaffold-component for echo-types resync.'" - -# ============================================================ -# Cleanup policy -# ============================================================ - -[cleanup] -build-artifacts = "Agda interface files (*.agdai) under proofs/ and tutorial/; never committed (.gitignore); removed by the clean-build task" -generated-dirs = "_build/ is gitignored (commit 9c00087); safe to delete at any time" -stale-branch-policy = "session/* and consolidation branches are enumerated and dispositioned (landing / superseded / abandoned) at each rung consolidation, per the CLAUDE.md rung-consolidation policy; bots never delete branches" -artifact-retention = "not-applicable" -artifact-retention-reason = "echo-types publishes no build artifacts; the proof suite is re-checked from source on every CI run" -cache-policy = "CI caches the Agda toolchain + stdlib only; cache invalidation follows .github/workflows/agda.yml" - -# ============================================================ -# Hygiene -# ============================================================ - -[hygiene] -proof-hygiene = "agda All.agda + Smoke.agda must exit 0 under --safe --without-K; zero postulates outside the enumerated proof-debt module (docs/proof-debt.md)" -guardrails = "tools/check-guardrails.sh + scripts/kernel-guard.sh are the repo-native hygiene gates; scripts/check-no-unsafe.sh supplements" -dead-code-rule = "modules that compile but are not imported by proofs/agda/All.agda are treated as dead code (CLAUDE.md working rules)" -todo-tracking = "inline TODOs on the ordinal track are slice-scoped and tracked in the obstruction docs (docs/echo-types/buchholz-rank-obstruction.adoc); repo-wide notes go to issues" -linting = "not-applicable" -linting-reason = "no general-purpose linter for Agda; the typechecker + guardrail scripts fill the role" -formatting = "not-applicable" -formatting-reason = "no enforced Agda formatter; .editorconfig + .gitattributes (LF, .agdai binary) carry the file-hygiene load" - -# ============================================================ -# Reversibility -# ============================================================ - -[reversibility] -backup-before-destructive = true -rollback-mechanism = "git-revert (history is append-only; superseded docs get SUPERSEDED banners rather than deletion, per STATE standing-decision sd-006)" -retracted-content-policy = "retractions are recorded in docs/retractions.adoc + docs/retracted/ and are never silently resurrected (R-2026-05-18 discipline)" -data-retention-policy = "not-applicable" -data-retention-reason = "echo-types holds no runtime data; everything reproducible is derived from source under version control" diff --git a/.machine_readable/contractiles/Intentfile.a2ml b/.machine_readable/contractiles/Intentfile.a2ml deleted file mode 100644 index ef74f45..0000000 --- a/.machine_readable/contractiles/Intentfile.a2ml +++ /dev/null @@ -1,99 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Intentfile (A2ML Canonical) — north-star contractile for rsr-template-repo -# Author: Jonathan D.A. Jewell -# -# Paired runner: intend.ncl -# Verb: intend -# -# Semantics: North-star contractile. Declares BOTH concrete committed -# next-actions AND horizon aspirations the project wishes to -# become. Two sections share one file because they answer -# the same question at different ranges: -# [[intents]] — "we WILL do this; track progress" -# status: declared → in_progress → done | -# deferred | retired -# [[wishes]] — "we WISH this were true; revisit later" -# status: declared → in_progress → achieved | -# abandoned -# grouped by horizon: near / mid / far. -# Non-gating — this is a report, not a gate. See the `must` -# contractile for hard gates. - -@abstract: -North-star contractile for rsr-template-repo. This repository is the -canonical template for Rhodium Standard Repository compliance. It provides -the scaffold that all hyperpolymath repos should copy and customize. -@end - -## Purpose - -The rsr-template-repo serves as the master template for all hyperpolymath -repositories. It contains the complete set of contractile files, machine-readable -specifications, and governance documentation that define the Rhodium Standard. - -Every new repository in the hyperpolymath estate should be initialized by -copying this template and substituting the placeholder values with -repo-specific content. - -## Anti-Purpose - -This repository is NOT: -- A general-purpose project scaffold for external use (hyperpolymath-only) -- A replacement for per-repo customization (all files must be bespoke) -- A static template that never changes (evolves with RSR spec) -- A runtime library or framework (build-time only) - -## If In Doubt - -If you are unsure whether a change is in scope, ask. Sensitive areas: -- .machine_readable/ contractile definitions -- RSR specification files -- Governance templates -- License policy documents - -## Committed Next-Actions - -### repo-initialization -- description: Provide just copy-and-substitute template for new repos -- probe: test -f scripts/init-repo.sh -- status: done -- notes: Run with source scripts/init-repo.sh - -### contractile-completeness -- description: Every RSR contractile has an a2ml and ncl implementation -- probe: ls .machine_readable/contractiles/*.a2ml | wc -l | grep -q "^6$" -- status: in_progress -- notes: Currently 6 contractile verbs: intend, must, trust, adjust, bust, dust - -### automation-scripts -- description: All repetitive tasks have just recipes -- probe: grep -c "^# " Justfile | grep -q "^[6-9][0-9]*$" -- status: in_progress - -## Wishes - -### Near Horizon - -#### cross-repo-validation -- description: Tooling to validate all repos against RSR spec -- horizon: near -- status: declared - -#### automated-substitution -- description: Script to automate repo-specific substitution in template -- horizon: near -- status: declared - -### Mid Horizon - -#### formal-verification -- description: Idris2 proofs for all critical contractile invariants -- horizon: mid -- status: declared - -### Far Horizon - -#### ecosystem-visualization -- description: Interactive graph of all hyperpolymath repos and dependencies -- horizon: far -- status: declared diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml deleted file mode 100644 index 55f8ab4..0000000 --- a/.machine_readable/contractiles/Mustfile.a2ml +++ /dev/null @@ -1,102 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Mustfile — Physical state contract for rsr-template-repo -# Author: Jonathan D.A. Jewell -# -# What MUST be true about this repository. Hard requirements. -# Run with: must check -# Fix with: must fix (where a deterministic fix exists) - -@abstract: -Physical-state invariants for rsr-template-repo. This is the canonical -RSR template repository. These are hard requirements — CI and pre-commit -hooks fail if any check fails. -@end - -## File Presence - -### license-present -- description: LICENSE file must exist -- run: test -f LICENSE -- severity: critical - -### readme-present -- description: README.adoc must exist -- run: test -f README.adoc -- severity: critical - -### security-policy -- description: SECURITY.md must exist -- run: test -f SECURITY.md -- severity: critical - -### ai-manifest -- description: 0-AI-MANIFEST.a2ml must exist -- run: test -f 0-AI-MANIFEST.a2ml -- severity: critical - -### governance-docs -- description: GOVERNANCE.adoc, MAINTAINERS.adoc, CODEOWNERS must exist -- run: test -f GOVERNANCE.adoc && test -f MAINTAINERS.adoc && test -f .github/CODEOWNERS -- severity: critical - -### machine-readable-dir -- description: .machine_readable/ directory must exist -- run: test -d .machine_readable -- severity: critical - -## Directory Structure - -### contractiles-complete -- description: All required contractile directories exist -- run: test -d .machine_readable/contractiles && test -d .machine_readable/contractiles/bust && test -d .machine_readable/contractiles/dust -- severity: critical - -### contractiles-files-present -- description: All four primary contractile files exist -- run: test -f .machine_readable/contractiles/Intentfile.a2ml && test -f .machine_readable/contractiles/Mustfile.a2ml && test -f .machine_readable/contractiles/Trustfile.a2ml && test -f .machine_readable/contractiles/Adjustfile.a2ml -- severity: critical - -### bust-dust-files-present -- description: Bustfile and Dustfile exist in their directories -- run: test -f .machine_readable/contractiles/bust/Bustfile.a2ml && test -f .machine_readable/contractiles/dust/Dustfile.a2ml -- severity: critical - -### six-directory-present -- description: 6a2 directory exists with required files -- run: test -d .machine_readable/6a2 && test -f .machine_readable/6a2/META.a2ml && test -f .machine_readable/6a2/ECOSYSTEM.a2ml && test -f .machine_readable/6a2/STATE.a2ml && test -f .machine_readable/6a2/PLAYBOOK.a2ml && test -f .machine_readable/6a2/AGENTIC.a2ml && test -f .machine_readable/6a2/NEUROSYM.a2ml -- severity: critical - -### anchors-directory -- description: anchors directory exists in 6a2 -- run: test -d .machine_readable/6a2/anchors -- severity: warning - -### self-validating-structure -- description: self-validating directory has k9-svc and examples -- run: test -d .machine_readable/self-validating && test -d .machine_readable/self-validating/k9-svc && test -d .machine_readable/self-validating/examples -- severity: warning - -## Template Integrity - -### no-placeholder-values -- description: No placeholder values remain in template files -- run: test -z "$(grep -r '{{' .machine_readable/contractiles/ 2>/dev/null)" -- severity: critical -- notes: All placeholders must be substituted when copying this template - -### template-readonly -- description: Template marker files are not modified -- run: grep -q 'RSR_TEMPLATE_DO_NOT_EDIT' .machine_readable/0.1-AI-MANIFEST.a2ml -- severity: warning - -## Git State - -### no-untracked-contractiles -- description: All contractile files are tracked in git -- run: test -z "$(git ls-files -o --exclude-standard .machine_readable/contractiles/ 2>/dev/null)" -- severity: critical - -### signed-commits -- description: All commits must be signed -- run: git verify-commit HEAD -- severity: critical diff --git a/.machine_readable/contractiles/Trustfile.a2ml b/.machine_readable/contractiles/Trustfile.a2ml deleted file mode 100644 index e2028b5..0000000 --- a/.machine_readable/contractiles/Trustfile.a2ml +++ /dev/null @@ -1,88 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Trustfile — Trust boundaries and integrity invariants for rsr-template-repo -# Author: Jonathan D.A. Jewell -# -# Defines what LLM/SLM agents are trusted to do without asking, and -# integrity invariants that verify the repo has not been tampered with. - -@abstract: -Trust boundaries and integrity checks for rsr-template-repo. This file -combines the trust-level definitions from the original TRUST.contractile -with the integrity invariants from the old Trustfile.a2ml. It defines -what AI agents may do autonomously and what requires human approval, -plus checks that verify repository integrity. -@end - -## Trust Levels - -The rsr-template-repo operates at trust level: maximal - -Trust levels: -- maximal: Agent may read, build, test, lint, format, heal freely. - Only destructive/external actions require approval. -- standard: Agent may read and build. Test/lint need approval. -- restricted: Agent may read only. All modifications need approval. -- minimal: Agent may read specific files only. Everything else blocked. - -Current trust level: maximal - -## Integrity Invariants - -### Secrets - -#### no-secrets-committed -- description: No credential files in repo -- run: test ! -f .env && test ! -f credentials.json && test ! -f .env.local && test ! -f .env.production -- severity: critical - -#### no-private-keys -- description: No private key files committed -- run: "! find . -name '*.pem' -o -name '*.key' -o -name 'id_rsa' -o -name 'id_ed25519' 2>/dev/null | grep -v node_modules | head -1 | grep -q ." -- severity: critical - -#### no-tokens-in-source -- description: No hardcoded API tokens in source -- run: "! grep -rE '(api[_-]?key|secret|token|password)\s*[:=]\s*[\"'\\''][A-Za-z0-9]{16,}' --include='*.js' --include='*.ts' --include='*.res' --include='*.py' . 2>/dev/null | grep -v node_modules | head -1 | grep -q ." -- severity: critical - -## Provenance - -#### author-correct -- description: Git author matches expected identity -- run: "git log -1 --format='%ae' | grep -qE '(hyperpolymath|j\\.d\\.a\\.jewell)'" -- severity: warning - -#### license-content -- description: LICENSE contains expected identifier -- run: grep -q 'PMPL\|MPL\|MIT\|Apache\|LGPL' LICENSE -- severity: warning - -## Template-Specific Trust - -### template-files-readonly -- description: Template scaffold files should not be modified except by maintainer -- run: test -z "$(git status --short .machine_readable/ 2>/dev/null | grep -v '^??' || true)" -- severity: advisory -- notes: Changes to template files require careful review - -### trust-deny-areas -- description: Sensitive areas from INTENT.contractile require explicit approval -- run: echo "Check .machine_readable/ contractiles and governance docs" -- severity: advisory -- areas: - - .machine_readable/ - - GOVERNANCE.adoc - - MAINTAINERS.adoc - - .github/CODEOWNERS - -## Container Security - -#### container-images-pinned -- description: Containerfile uses pinned base images -- run: test ! -f Containerfile || grep -q 'cgr.dev\|@sha256:' Containerfile -- severity: warning - -#### no-dockerfile -- description: No Dockerfile (use Containerfile) -- run: test ! -f Dockerfile -- severity: warning diff --git a/.machine_readable/integrations/README.adoc b/.machine_readable/integrations/README.adoc index a923a4a..bd01539 100644 --- a/.machine_readable/integrations/README.adoc +++ b/.machine_readable/integrations/README.adoc @@ -1,52 +1,13 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= Integrations (echo-types) -:toc: +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += `.machine_readable/integrations/` — retired -echo-types' cross-repo integrations. The authoritative status ledger is -`docs/bridges/cross-repo-bridge-status.md` (last updated 2026-06-02); these -files are the machine-readable index of it. +The `.a2ml` records that lived here were removed on 2026-09-30 by owner +ruling: the `.a2ml` surface is retired in favour of `.deed` records. -[cols="1,1,3"] -|=== -| File | Kind | Summary +The last tree that held them is frozen at +https://github.com/hyperpolymath/echo-types/tree/39a7a99cbe19a918843e9624010510b5fc3b8366/.machine_readable/integrations[commit 39a7a99]. +Read that copy for history; do not recreate `.a2ml` files here. -| `echotypes-jl.a2ml` -| executable-companion -| EchoTypes.jl v0.2.0 (pinned `e7dded6`) — finite-domain Julia shadow of the - Tier-1+2 spine + unconditional F5 OFS. Falsifies-by-counterexample; makes - no proof claims; the Agda here is the source of truth. - -| `arghda-core.a2ml` -| extracted-tool -| Language-agnostic Agda proof-workspace engine, extracted from echo-types - 2026-05-30 (#159); subtree removed (#160). Now standalone. - -| `panll.a2ml` -| constellation-consumer -| Three-pane cognitive-relief HTI. echo-types is a cited foundation, not a - build dependency. - -| `groove.a2ml` -| service-discovery (inert) -| Declared but inert — echo-types is a library and exposes no service / port. - -| `verisim.a2ml` -| constellation-placeholder -| No current dependency; recorded for constellation completeness. -|=== - -== Active Agda↔prover bridges (in `proofs/agda/`, ledgered separately) - -These are in-repo bridge *modules*, not external integrations, and live in -`proofs/agda/` + `docs/bridges/`: - -* `EchoCNOBridge.agda` ↔ absolute-zero `CNO.agda` — content-bridge done. -* `EchoEphapaxBridge.agda` ↔ ephapax `formal/Echo.v` — navigability done, content NARROW (L3). -* `EchoJanusBridge.agda` ↔ januskey Idris2 `OpKind` — name-bridge only. -* `EchoTropical.agda` ↔ tropical-resource-typing `.thy`/`.lean` — citation-level. - -== Exploratory (citation-level, Core Affect = NO) - -* Valence Shell / Ochránce accountable-shell — candidate downstream consumer of - the structured-loss vocabulary; no bridge module, nothing wired into - `All.agda` / `Smoke.agda`. +Conversion to `.deed` is tracked estate-wide in +https://github.com/hyperpolymath/rsr-template-repo/issues/209[rsr-template-repo#209]. diff --git a/.machine_readable/integrations/arghda-core.a2ml b/.machine_readable/integrations/arghda-core.a2ml deleted file mode 100644 index acb407f..0000000 --- a/.machine_readable/integrations/arghda-core.a2ml +++ /dev/null @@ -1,23 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Integration: arghda-core — extracted proof-workspace engine -# Extracted from echo-types 2026-05-30 (echo-types#159); subtree removed (PR #160). - -[integration] -name = "arghda-core" -type = "extracted-tool" -repository = "https://github.com/hyperpolymath/arghda-core" - -[provenance] -origin = "extracted from echo-types" -extracted = "2026-05-30" -issue = "echo-types#159" -removal-pr = "echo-types#160" -note = "The arghda-core/ subtree and its cross-refs were removed from this repo on extraction; arghda-core is now a standalone repo." - -[capabilities] -description = "Language-agnostic proof-workspace manager for Agda: triage folders (inbox -> working -> proven/rejected), linter, DAG view." -companion-planned = "arghda-panll (Gossamer/AffineScript presentation layer)" - -[relationship] -motivating-pipeline = "docs/buchholz-plan.adoc appendix" -direction = "downstream tool; no in-repo build dependency on echo-types" diff --git a/.machine_readable/integrations/echotypes-jl.a2ml b/.machine_readable/integrations/echotypes-jl.a2ml deleted file mode 100644 index eec14bd..0000000 --- a/.machine_readable/integrations/echotypes-jl.a2ml +++ /dev/null @@ -1,31 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Integration: EchoTypes.jl — executable Julia companion (falsifying shadow) -# Source of truth for status: docs/bridges/cross-repo-bridge-status.md (2026-06-02) - -[integration] -name = "echotypes-jl" -type = "executable-companion" -repository = "https://github.com/hyperpolymath/EchoTypes.jl" -version = "0.2.0" -pinned-commit = "e7dded6" -registry = "julia-professional-registry" - -[scope] -mirrors = "finite-domain shadow of the Tier-1 + Tier-2 spine + the unconditional F5 OFS fragment" -modules = [ - "Echo", "EchoResidue", "EchoFiberCount", "EchoThermodynamics", - "EchoTotalCompletion", "EchoOrthogonalFactorizationSystem", - "EchoImageFactorization", "EchoNoSectionGeneric", "EchoLossTaxonomy", - "EchoEntropy", "EchoObservationalEquivalence", -] -not-mirrored = [ - "the R-2026-05-18 retracted surface", - "F5 funext-qualified clauses (uniqueness up to iso, diagonal lifting) — Julia has no funext, the claims would be vacuous", - "UIP- and truncation-strength upgrades", -] - -[claim-policy] -makes-proof-claims = false -behaviour = "falsifies-by-counterexample on concrete data" -source-of-truth = "the Agda in echo-types remains authoritative; the Julia companion is a shadow" -ci-coupling = "none in either direction" diff --git a/.machine_readable/integrations/groove.a2ml b/.machine_readable/integrations/groove.a2ml deleted file mode 100644 index 0b51190..0000000 --- a/.machine_readable/integrations/groove.a2ml +++ /dev/null @@ -1,38 +0,0 @@ -; SPDX-License-Identifier: MPL-2.0 -; Groove Protocol Manifest — declares API surfaces this project exposes. -; -; echo-types is a constructive Agda PROOF LIBRARY. It exposes no runtime -; service: there is no daemon, no HTTP surface, no port. This manifest is -; therefore declared but inert — kept for constellation consistency and so a -; future service layer (if ever added) has a slot. -; -; See: https://github.com/hyperpolymath/standards/tree/main/groove-protocol - -(groove-manifest - (version "1.0") - - (service "echo-types") - (service-version "0.1.1") - - ; Port — MUST be unique across the ecosystem; echo-types has no service, - ; so none is assigned. Do not assign a port to a library. - (port 0) ; 0 = not assigned (no service surface) - - ; API surfaces — echo-types exposes none. - (api-surfaces - (rest (enabled false)) - (grpc (enabled false)) - (graphql (enabled false)) - (websocket (enabled false)) - (sse (enabled false)) - (groove (enabled false))) - - (health "") ; no health endpoint — not a service - - ; Capabilities — what this artefact offers others (concept-level only). - (capabilities - ("structured-loss-vocabulary: Echo / EchoResidue / EchoLossTaxonomy classification of lossy maps") - ("machine-checked identity claim: --safe --without-K, postulate-free")) - - ; Dependencies — what this artefact needs from others at runtime. - (dependencies ())) ; none — build-time only (agda-stdlib) diff --git a/.machine_readable/integrations/panll.a2ml b/.machine_readable/integrations/panll.a2ml deleted file mode 100644 index 9da5247..0000000 --- a/.machine_readable/integrations/panll.a2ml +++ /dev/null @@ -1,19 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Integration: PanLL — constellation interface consumer -# echo-types is a foundation PanLL can cite, NOT a build dependency. - -[integration] -name = "panll" -type = "constellation-consumer" -repository = "https://github.com/hyperpolymath/panll" - -[relationship] -description = "PanLL is a three-pane cognitive-relief HTI (Ambient / Symbolic / Neural / World panes). echo-types sits below it as a foundational formal-verification artefact in the same constellation." -direction = "echo-types is upstream-foundation; PanLL is a downstream interface." -coupling = "none — no shared schema, no import path, no CI dependency in either direction. The relationship is citation / constellation membership only." - -[substrate] -# PanLL's own runtime substrate, recorded for constellation context. -presentation = "Gossamer (Zig + WebKitGTK webview shell, ~5 MB binary)" -voice = "Burble (Zig SIMD audio, IEEE-1588 PTP sync, browser-based)" -discovery = "Groove protocol (HTTP service discovery)" diff --git a/.machine_readable/integrations/verisim.a2ml b/.machine_readable/integrations/verisim.a2ml deleted file mode 100644 index 4cf7872..0000000 --- a/.machine_readable/integrations/verisim.a2ml +++ /dev/null @@ -1,20 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# OPTIONAL: VeriSim / VeriSimDB — constellation state/database layer. -# echo-types has NO current dependency on VeriSim; this is a constellation -# placeholder. Delete if no relationship is established. - -[integration] -name = "verisim" -type = "constellation-placeholder" -repository = "https://github.com/hyperpolymath/nextgen-databases" - -[relationship] -description = "VeriSim / VeriSimDB is the constellation's identity-state capture layer with filesystem fallback; VCL-total (formerly VCL-UT) is its next-gen interaction language designed to satisfy all 10 levels of type safety against a consonance engine." -direction = "potential-future-consumer of echo-types' structured-loss vocabulary" -coupling = "none today — no shared schema, no import path, no feed. Recorded for constellation completeness only." - -[feed-config] -# No feed is emitted. If echo-types ever feeds build/proof metrics to a -# constellation analytics store, configure it here. -emit-scan-results = false -emit-build-metrics = false diff --git a/.machine_readable/svc/k9/methodology-guard.k9.ncl b/.machine_readable/svc/k9/methodology-guard.k9.ncl index 944f2c5..8fa87e1 100644 --- a/.machine_readable/svc/k9/methodology-guard.k9.ncl +++ b/.machine_readable/svc/k9/methodology-guard.k9.ncl @@ -2,9 +2,10 @@ # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # K9 Validator: Methodology Guard (echo-types) -# Checks that agent work respects the methodology constraints declared in -# agent_instructions/methodology.a2ml and the proof discipline in -# .machine_readable/6a2/META.a2ml § current-practices. +# Checks that agent work respects the echo-types proof discipline +# (--safe --without-K, zero postulates, All.agda coverage, kernel cone). +# The former .a2ml record checks (STATE, ANCHOR, coverage) were removed +# with the .a2ml records themselves; see the retirement PR. # # Usage: k9 validate methodology-guard @@ -69,27 +70,6 @@ let methodology_guard = { check_type = "external-script", script = "scripts/kernel-guard.sh", }, - - state_not_template = { - description = "STATE.a2ml must not contain template placeholders", - severity = "warning", - file = ".machine_readable/6a2/STATE.a2ml", - reject_patterns = ["{{PLACEHOLDER}}", "{{PROJECT}}", "rsr-template-repo"], - }, - - anchor_clade_not_fabricated = { - description = "ANCHOR.a2ml clade/uuid must stay TODO until a gv-clade-index assignment exists", - severity = "warning", - file = ".machine_readable/anchors/ANCHOR.a2ml", - require_pattern = "TODO: assign via gv-clade-index registry", - }, - - coverage_updated = { - description = "coverage.a2ml should be updated within 30 days", - severity = "info", - file = ".machine_readable/agent_instructions/coverage.a2ml", - staleness_days = 30, - }, }, } in methodology_guard diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml deleted file mode 100644 index 0941bef..0000000 --- a/0-AI-MANIFEST.a2ml +++ /dev/null @@ -1,15 +0,0 @@ -; SPDX-License-Identifier: MPL-2.0 -; 0-AI-MANIFEST.a2ml — echo-types - -[ai-contract] -purpose = "Constructive Agda formalisation of echo types — proof-relevant fibers / loss-with-residue. Foundation library." -agent-may = "edit proofs/agda/, docs/, CHANGELOG.md, contractiles/, .machine_readable/6a2/" -agent-may-not = "edit LICENSE / SECURITY.md / [security.signing] without explicit user confirmation; introduce believe_me/assert_total/postulate/sorry/Admitted/unsafeCoerce/Obj.magic; reopen EI-2 under any framing in .machine_readable/6a2/STATE.a2ml § forbidden-rebrandings; rename ModeGraded -> ModeGrade (the trailing d is canonical)" -agent-must-after = "code-edit -> 'just verify'" - -[escalation] -breaking-changes = "open ADR; respect META.a2ml § architecture-decisions" -ei-2-mention = "Run PLAYBOOK.a2ml § on-EI-2-mention. Cite from STATE; do not paraphrase." -banned-pattern-relapse = "Hard reject. Discharge the proof properly or open ADR." -naming-trap-relapse = "Hard reject. Match the canonical naming." -schema-drift-in-6a2 = "Open issue against hyperpolymath/standards; do not silently reshape this repo's 6a2 files." diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 44579c0..375471d 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -7,6 +7,15 @@ Changelog]. === [Unreleased] +==== Removed (2026-09-30) + +* _The 27 `+.a2ml+` machine-readable records._ Removed by owner ruling: +the `+.a2ml+` surface is retired in favour of `+.deed+` records. The last tree holding them is commit `+39a7a99+`; +`+.github/CONTRIBUTING.md+` now points at that frozen copy for the EI-2 +fence and the naming traps. The three K9 methodology-guard checks that +targeted the deleted files were removed with them. Conversion to +`+.deed+` is tracked in rsr-template-repo#209. + ==== Added (2026-06-13) * _`+EchoDeniability.agda+` — residue deniability as a first-class echo diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml deleted file mode 100644 index 427a85a..0000000 --- a/audits/assail-classifications.a2ml +++ /dev/null @@ -1,34 +0,0 @@ -;; SPDX-License-Identifier: MPL-2.0 -;; Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -;; -;; Assail Classifications — echo-types -;; See panic-attack/.claude/CLAUDE.md § "User-Classification Registry". -;; -;; First populated 2026-05-30 in response to the Track-C panic-attack -;; sweep tracked at echo-types#113. One real-path finding classified; -;; ten path-duplicates flagged at `.claude/worktrees/*` paths are -;; scan-artefact noise (those paths are gitignored and not present in -;; the committed tree) and are not enumerated below. -;; -;; The 2026-05-26 sweep also flagged `arghda-core/src/lint/orphan_module.rs` -;; UnboundedAllocation (and 5 stale `.claude/worktrees//arghda-core/...` -;; path-duplicates). That file no longer lives in echo-types — arghda-core -;; was extracted to its own repo at https://github.com/hyperpolymath/arghda-core -;; on 2026-05-30 per echo-types#159. Re-classification of that finding, -;; if needed, belongs in the new repo's own assail-classifications. - -(assail-classifications - (metadata - (version "1.0.0") - (project "echo-types") - (last-updated "2026-05-30") - (entries 1) - (status "active") - (notes "Ten additional findings on .claude/worktrees//* paths from the 2026-05-26 sweep are excluded as scan artefacts: .claude/ is gitignored, those subtrees are not in the committed repo, the scanner picked up the developer's local worktree state. Future scans against the committed tree should not re-raise them; if they do, the panic-attack scanner is reading workspace state outside the repo and the carve-out belongs upstream in panic-attack. The arghda-core/src/lint/orphan_module.rs finding also from that sweep moved to the standalone arghda-core repo per echo-types#159.")) - - (classification - (file "flake.guix") - (category "SupplyChain") - (classification "flake-lock-present-tag-and-sha-pins") - (audit "echo-types#113 triage 2026-05-30") - (rationale "Scanner flagged 'inputs without narHash, rev pinning, or sibling flake.lock'. As of main HEAD: (a) flake.lock exists adjacent to flake.guix; (b) nixpkgs is locked in flake.lock with rev + narHash; (c) agda-stdlib input declares flake = false with tag pin github:agda/agda-stdlib/v2.3; (d) absolute-zero input declares flake = false with explicit commit SHA pin 3ff5cee7f3fd002378089cd02f0c90a3747b45f0. The CI workflow .github/workflows/agda.yml additionally re-pins absolute-zero by SHA at runtime with an explicit ABSZ_REF check, which would fail on any drift. The finding was correct on the 2026-05-26 scan date if flake.lock was absent or had fewer locked nodes at that time; it is stale at current main."))) diff --git a/proofs/agda/EchoHaplotypeCollapsing.agda b/proofs/agda/EchoHaplotypeCollapsing.agda index fb5d05e..225cd1a 100644 --- a/proofs/agda/EchoHaplotypeCollapsing.agda +++ b/proofs/agda/EchoHaplotypeCollapsing.agda @@ -150,13 +150,21 @@ clone-count-aggregation G = aggregation-as-fold G example-clones : List Clone example-clones = clone₁ ∷ clone₂ ∷ [] -example-count : aggregate-values countAggregator example-clones ≡ 2 +example-count : aggregate-values {K = Haplotype} countAggregator example-clones ≡ 2 example-count = refl -- Count clones per haplotype via monoid fold (the GROUP BY analogue). -- In production: groupByKey + fold, not filter + length, to stay O(n). +-- +-- `K` (the group-by key) is genuinely phantom in `GroupAggregator`/ +-- `countAggregator` (issue #175's `agg` field never mentions it), so +-- nothing here forces Agda's unifier to solve it from `V`, `M`, or the +-- result type — it must be supplied. `Haplotype` is the key this +-- aggregator is used to group by in this module (the GROUP BY +-- analogue the comment above names), so it is also the semantically +-- honest choice, not just a syntactically convenient one. count-clones-per-haplotype : List Clone → ℕ -count-clones-per-haplotype cs = aggregate-values countAggregator cs +count-clones-per-haplotype cs = aggregate-values {K = Haplotype} countAggregator cs ------------------------------------------------------------------------ -- 5. Choreographic framing: Raw ⊑ Collapsed