chore: RSR template floor (23 files: githealth + RSR docs + dotfiles + contractiles + 4 mandatory workflows + stapeln) by hyperpolymath · Pull Request #30 · hyperpolymath/echo-types

hyperpolymath · 2026-04-30T17:11:12Z

Summary

Bring echo-types to the RSR template floor — 23 new files covering githealth, RSR docs, dotfiles, the AI manifest, the canonical 4 mandatory workflows, contractiles, and a stapeln/Containerfile pair sized for the proof-artefact-carrier shape this repo ships.

This is the second of three echo-types PRs:

PR chore: .scm -> .a2ml for 6a2 files (canonical location) + Justfile make -> just #29 — .scm → .a2ml for 6a2 files + Justfile make → just. (Merged or pending.)
This PR — RSR floor scaffolding.
Forthcoming — recognition PR against hyperpolymath/standards (Agda + echo-types as canonical loss-with-residue foundation).

What's added

Githealth (5 files, `.md` per the doc-format rule)

CHANGELOG.md — Keep-a-Changelog format, with the staged 7-commit integration (per STATE.a2ml § integration) under [Unreleased].
CODE_OF_CONDUCT.md — Contributor Covenant 2.1 reference.
CONTRIBUTING.md — DCO, branch rules, pre-merge checklist with estate banned-pattern list (no new believe_me / assert_total / postulate / sorry / Admitted / unsafeCoerce / Obj.magic), EI-2 discipline (do not reopen; cite STATE), and naming traps (ModeGraded canonical, ModeGrade forbidden).
SECURITY.md — disclosure policy + posture (formal-methods library; no networked attack surface; report proof-soundness concerns to same address).
0-AI-MANIFEST.a2ml — agent gating: may-edit, may-not-edit, escalation triggers (especially the EI-2 mention procedure that routes to PLAYBOOK.a2ml § on-EI-2-mention).

RSR docs (5 files)

EXPLAINME.adoc — one-paragraph + one-sentence + status snapshot.
QUICKSTART-DEV.adoc — toolchain, first build, common failures (banned-pattern detection, naming-trap, EI-2 reopen).
QUICKSTART-USER.adoc — depend on echo-types as a library; cite the formalism.
QUICKSTART-MAINTAINER.adoc — release procedure; new-bridge addition checklist; escalation patterns.
TOPOLOGY.adoc — repo layout + cross-repo dependency direction (foundation: depends on hyperpolymath/standards schemas only) + verification posture table per track.

Dotfiles (3 files)

.editorconfig — LF, UTF-8, 2-space default; 4 for Rust; tab for Justfile/Makefile.
.envrc — use flake (flake.nix is parked per Intentfile).
.tool-versions — agda 2.7.0, ghc 9.8.2, cabal 3.12.1.0, rust 1.82.0, just 1.40.0.

Contractiles (4 files)

contractiles/Mustfile.a2ml — invariants: license/readme/security/changelog/spdx-headers/no-banned-files/agda-typechecks/no-believe_me/no-postulates/no-sorry/mode-graded-canonical/rust-compiles.
contractiles/Trustfile.a2ml — license content / no secrets / images pinned (post-pin) / ei-2-record-intact check.
contractiles/Dustfile.a2ml — source-rollback / clean-build (Agda .agdais + Rust target/) / resync-from-template.
contractiles/Intentfile.a2ml — RSR conformance / proofs (Buchholz close, Q2.1/Q2.3/Q2.4 discharge) / process / explicitly-parked (recipe v0.2+, full 2D iff theorem).

Mandatory RSR workflows (4 files)

Copied verbatim from hyperpolymath/standards/.github/workflows/ (the canonical 4 per hypatia-rules/rsr-self-compliance.a2ml @required_workflows):

.github/workflows/hypatia-scan.yml
.github/workflows/mirror.yml
.github/workflows/scorecard.yml
.github/workflows/rsr-antipattern.yml

(Existing agda.yml workflow remains; it's the proof-typecheck CI lane.)

Container build

stapeln.toml — layered Chainguard build with echo-types-runtime as a static (artefact-carrier) image: holds the type-checked proofs/ tree for downstream Agda projects to mount, not a service. @sha256: pins are TODO(scaffold) markers.
Containerfile — podman-build fallback shape.

What's deliberately NOT in this PR

Per the staged sequence and the maintainer's existing parked migrations:

readme.adoc (lowercase) → README.adoc (canonical caps) — leaving the lowercase as-is so this PR stays focused on additions; rename is a follow-up.
roadmap.adoc / roadmap-gates.adoc — same reason.
README.md (duplicate of readme.adoc) — rationalisation needs a content review beyond mechanical renaming.
DOCUMENTATION_STATUS.md and docs/*.md (~7 files) — .md → .adoc per the doc-format rule, but content review is needed; follow-up PR.
flake.nix / guix.scm — toolchain reproducibility files, listed in Intentfile but require deliberate authoring.
.machine_readable/ reorganisation to match hyperpolymath/standards's contractile-trident shape (.machine_readable/contractiles/<verb>/...) — substantial, separate PR.
Abstract-Echo-Types and arghda-core/README.md — kept as-is (need content judgement).

Why merge this

It brings echo-types from "minimum-viable" file presence to the RSR template floor as defined in hyperpolymath/standards/.meta/REQUIRED-FILES.adoc (extension fix pending — see standards PR #33). Once this lands, downstream tooling that audits hyperpolymath repos for floor conformance (e.g. idaptik-port/tools/scaffold-component.{py,my} --audit) will report this repo as conformant.

🤖 Generated with Claude Code

…idue formalism Adds Agda to Tier-1 alongside the existing Tier-1 set in three RSR_OUTLINE.adoc copies (with the ReScript -> AffineScript and Rust -> Rust(+SPARK) updates from PR #35 inlined to avoid build conflict). Adds two new rows to .claude/CLAUDE.md: - Agda (formal verification, foundational/type-theoretic) - echo-types library (canonical loss-with-residue formalism; cite from hyperpolymath/echo-types rather than reinventing) Reframes Idris2 row from 'sole option' to 'primary, ABI-style proofs' since Agda now formally complements it. Updates ai-instruction/sonnet.md hard-rules language-policy line to list AffineScript first, include Agda explicitly, ban ReScript, and reference RS/TS/JS -> AffineScript -> typed-wasm. Coordinates with: hyperpolymath/echo-types#29 (.scm -> .a2ml + Justfile fix) hyperpolymath/echo-types#30 (RSR floor scaffolding) #33 (REQUIRED-FILES doc-drift fix) #35 (ReScript -> AffineScript sweep; line-overlap with this PR; mechanical rebase at merge) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…echecks (#31) ## Summary Fixes two latent CI breakages so Agda goes green again. ### 1. Install absolute-zero library (`agda.yml`) `echo-types.agda-lib` declares `depend: standard-library absolute-zero`, but the workflow only registered `standard-library`. Agda CI has been red on `main` since `3f654ef` (2026-04-30) added the dep without a workflow update. Adds a fetch step that shallow-clones `hyperpolymath/absolute-zero`, then registers it alongside `standard-library` in `~/.agda/libraries`. ### 2. Fix `ModeGrade` -> `ModeGraded` import typo (`characteristic/RecipeNonTriviality.agda`) `RecipeNonTriviality.agda` imports `characteristic.ModeGrade` (no `d`) which doesn't exist; the actual file is `characteristic.ModeGraded`. Renames cleanly: `MGEcho` -> `ModeGEcho`, `applyGrade` -> `applyGradeM`. The body uses (`modegrade-cell-action` and friends) reduce definitionally as before because `applyMode/applyGrade` at `(linear, keep)` are identity in the existing `ModeGraded.agda`. This bug was latent since the characteristic lane was added in #27 (2026-04-29), masked by the absolute-zero env break that (1) fixes. ## Local verification ``` agda -i proofs/agda proofs/agda/All.agda # exit 0 agda -i proofs/agda proofs/agda/Smoke.agda # exit 0 agda -i proofs/agda proofs/agda/characteristic/All.agda # exit 0 agda -i proofs/agda proofs/agda/examples/All.agda # exit 0 ``` All under `--safe --without-K`. No postulates introduced. ## Effect on other PRs After merge, #28, #29, #30 should re-run with the env in place. They may need rebases onto the new `main`. 🤖 Generated with [Claude Code](https://claude.com/claude-code)

## Summary Lands the Phase 1.3 limit-case closure, the `wf-<′` well-foundedness rung, and the Pentagon Σ-associativity iso packaging. Continues the composition track on top of #31's now-green CI. **`proofs/agda/Ordinal/Brouwer/Phase13.agda`** - Limit-case closure: `≤′-lim`, `≤′-refl`, `f-in-lim′`, `≤′-trans` - Well-foundedness rung: `pred-of-osuc-<′`, `pred-of-olim-<′`, `wf-<′` - Three call-sites carry named-implicit `{α = …}` annotations (stdlib 2.3 unifier needs them; stdlib 2.0 evidently didn't) **`proofs/agda/Echo.agda`** - Pentagon Σ-associativity iso packaging **`proofs/agda/Smoke.agda`** - Pin the new headlines, including the three `wf-<′` ones **`CLAUDE.md`, `docs/echo-types/composition.md`** - Composition-track and Phase 1.3 status updates - Pentagon Q4 marked landed No postulates introduced. ## Test plan - [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/All.agda` — exit 0 (locally, stdlib 2.3) - [x] `LC_ALL=C.UTF-8 agda -i proofs/agda proofs/agda/Smoke.agda` — exit 0 (locally, stdlib 2.3) - [ ] CI agda typecheck (characteristic + examples lanes per #27) ## Notes - Branched off post-#31 main; PR #30's `chore/rsr-floor-scaffold` stays focused on its 23-file scaffold scope. - Sets up the next rung: Phase 1.3 arithmetic side (`⊕-mono-<-right` etc.) → `rank-mono` → unbudgeted `wf-<ᵇʳᶠ`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…tiles + 4 mandatory workflows + stapeln Brings echo-types to file-presence conformance with the RSR template floor as defined in hyperpolymath/standards/.meta/REQUIRED-FILES.adoc. Added (23 files): Githealth (5): CHANGELOG.md / CODE_OF_CONDUCT.md / CONTRIBUTING.md / SECURITY.md / 0-AI-MANIFEST.a2ml RSR docs (5): EXPLAINME.adoc / QUICKSTART-{DEV,USER,MAINTAINER}.adoc / TOPOLOGY.adoc Dotfiles (3): .editorconfig / .envrc / .tool-versions Contractiles (4): contractiles/{Mustfile,Trustfile,Dustfile,Intentfile}.a2ml Mandatory workflows (4 — copied from standards): .github/workflows/{hypatia-scan,mirror,scorecard,rsr-antipattern}.yml Container build (2): stapeln.toml + Containerfile (proof-artefact-carrier shape) Echo-types-specific content hooks: - CONTRIBUTING.md banned-pattern list explicitly covers Agda (believe_me/assert_total/postulate/sorry/Admitted) plus general estate (unsafeCoerce/Obj.magic). - 0-AI-MANIFEST.a2ml routes EI-2 mentions to PLAYBOOK § on-EI-2-mention and forbids ModeGraded -> ModeGrade rename (canonical naming trap). - Mustfile checks for: agda-typechecks, no-believe-me, no-postulates, no-sorry/Admitted/unsafeCoerce/Obj.magic, mode-graded-canonical, rust-compiles (arghda-core companion). - Trustfile.ei-2-record-intact verifies the EI-2 audit record's presence in STATE.a2ml. Out of scope (follow-up PRs): - readme.adoc (lowercase) -> README.adoc (canonical caps) rename - roadmap.adoc / roadmap-gates.adoc rename - README.md / readme.adoc duplicate rationalisation - DOCUMENTATION_STATUS.md + docs/*.md to .adoc per doc-format rule - flake.nix / guix.scm authoring - .machine_readable contractile-trident reshape Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…upport

…ell $HOME)

…idue formalism (#36) ## Summary Recognise **Agda** as a Tier-1 language and **`hyperpolymath/echo-types`** as the canonical loss-with-residue formalism in the agent-facing policy and tier docs. ## What changed ### Tier-1 list (3 RSR_OUTLINE.adoc copies) ```diff - * **Tier 1** (Gold): Rust, Elixir, Zig, Ada, Haskell, ReScript + * **Tier 1** (Gold): Rust(+SPARK), Elixir, Zig, Ada, Haskell, AffineScript, Agda ``` Adds Agda alongside the existing tier. Replaces ReScript with AffineScript and qualifies Rust as Rust(+SPARK), tracking the broader ReScript→AffineScript migration in PR #35 (this PR's diff includes those updates so the file builds without conflict; #35 may need a rebase but the resolutions are mechanical). Files updated: - `0-ai-gatekeeper-protocol/RSR_OUTLINE.adoc` line 149 - `0-ai-gatekeeper-protocol/repo-guardian-fs/RSR_OUTLINE.adoc` line 149 - `consent-aware-http/RSR_OUTLINE.adoc` line 149 ### Agent-facing language policy (`.claude/CLAUDE.md`) Adds two new rows to the allowed-languages table: ``` | **Agda** | Formal verification (foundational / type-theoretic constructions) | Used by hyperpolymath/echo-types ... | | **echo-types library** | Loss-with-residue formalism (Agda) | hyperpolymath/echo-types — canonical formalisation of Echo f y := Σ (x : A) , (f x ≡ y) ... | ``` Reframes Idris2 from "Formal verification (sole option)" to "Formal verification (primary, ABI-style proofs)" since Agda now formally complements it for foundational constructions where Idris2's specific dependent-type idiom isn't the right tool. ### `ai-instruction/sonnet.md` The hard-rules language-policy line now lists AffineScript first, includes Agda explicitly, bans ReScript, and references the AffineScript→typed-wasm direction: ```diff - - <Language policy: ReScript / Rust / Deno / Zig / Idris2 / Gleam; no - TypeScript, Node, npm/bun/yarn, Go, general Python> + - <Language policy: AffineScript / Rust(+SPARK) / Deno / Zig / Idris2 / Agda / Gleam; no + TypeScript, ReScript, Node, npm/bun/yarn, Go, general Python (RS/TS/JS → AffineScript → typed-wasm; Agda for foundational proofs incl. echo-types)> ``` ## Why Echo-types (`hyperpolymath/echo-types`) is an active, well-developed Agda formalisation that the `coord-mcp` TODO file already aspires to dogfood. Until now, the standards' policy docs name only Idris2 as the ecosystem's formal-verification language, which understates Agda's role for the foundational-construction track. This PR makes the actual two-prover posture explicit. The echo-types row is added because the canonical fiber/echo construction `Echo f y := Σ (x : A) , (f x ≡ y)` should not be re-derived in downstream design docs and proofs — they should cite the library. Naming it explicitly in CLAUDE.md prevents accidental reinvention. ## Coordinated companion PRs - `hyperpolymath/echo-types#29` — `.scm` → `.a2ml` 6a2 file rename + Justfile `make` → `just`. (Bringing echo-types into compliance with the canonical extension rule.) - `hyperpolymath/echo-types#30` — RSR template floor (23 new files: githealth + RSR docs + dotfiles + 4 mandatory workflows + contractiles + stapeln). (Bringing echo-types to file-presence floor.) - `#33` — `.scm` → `.a2ml` doc fix in REQUIRED-FILES.adoc + workflow-count drift fix. - `#35` — ReScript → AffineScript estate-wide sweep. (Some line-overlap with this PR; mechanical rebase at merge.) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath mentioned this pull request May 1, 2026

ci(agda): install absolute-zero + fix ModeGrade typo so the suite typechecks #31

Merged

hyperpolymath mentioned this pull request May 1, 2026

Phase 1.3 closure + Pentagon Σ-assoc + wf-<′ #32

Merged

3 tasks

hyperpolymath force-pushed the chore/rsr-floor-scaffold branch from 5f2ecbb to b36ab15 Compare May 1, 2026 05:49

hyperpolymath and others added 4 commits May 1, 2026 07:18

ci(hypatia): fix unresolvable upload-artifact SHA (v4 -> ea165f8d)

1a258c9

ci(hypatia): bump erlef/setup-beam v1.18.2 -> v1.24.0 for ubuntu-24 s…

19d6289

…upport

ci(hypatia): fix Build Hypatia step working-directory (env.HOME -> sh…

bf2bc10

…ell $HOME)

hyperpolymath force-pushed the chore/rsr-floor-scaffold branch from 4cead5a to bf2bc10 Compare May 1, 2026 06:18

hyperpolymath merged commit c4d74f3 into main May 1, 2026
3 of 4 checks passed

hyperpolymath deleted the chore/rsr-floor-scaffold branch May 1, 2026 06:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: RSR template floor (23 files: githealth + RSR docs + dotfiles + contractiles + 4 mandatory workflows + stapeln)#30

chore: RSR template floor (23 files: githealth + RSR docs + dotfiles + contractiles + 4 mandatory workflows + stapeln)#30
hyperpolymath merged 4 commits intomainfrom
chore/rsr-floor-scaffold

hyperpolymath commented Apr 30, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented Apr 30, 2026

Summary

What's added

Githealth (5 files, .md per the doc-format rule)

RSR docs (5 files)

Dotfiles (3 files)

Contractiles (4 files)

Mandatory RSR workflows (4 files)

Container build

What's deliberately NOT in this PR

Why merge this

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Githealth (5 files, `.md` per the doc-format rule)