feat(rsr): echo-types RSR Bronze (58% -> ~83%) + PROOF-STATUS doc

claude · hyperpolymath · commit b68c14ecec3f · 2026-06-18T12:47:46.000+01:00
echo-types end-to-end. Its Agda proofs are already green and postulate-free, so this is the governance/docs layer plus an honest proof-status document (no proofs changed; All.agda + Smoke.agda remain green, verified 2026-06-18). - PROOF-STATUS.adoc — honest status: proved (composition iso; Establishment Pillars A-D; the Tier-1/2/3 canonical-identity modules; the sound-carrier ordinal WF wf-<b2 + wf-<brf2 + e0) vs open (the Bachmann-Howard milestone psi0(Omega_omega); the 2 isolated Fidelity postulates; the cubical-island (epi,mono) truncation; Pillar E paper [EXPAND] tags). - .well-known/{security.txt,ai.txt,humans.txt} (RFC 9116 + AI policy + attribution). - Justfile: `validate` recipe (full verify + kernel-guard). - README: explicit Installation + Usage headings. - CONTRIBUTING: Tri-Perimeter Contribution Framework (TPCF) + fork workflow. - CODE_OF_CONDUCT: inline harassment + enforcement procedures (was a bare Contributor Covenant link). RSR self-audit (via the de-brittled rsr-audit.sh): 57.58% -> 80.56% BRONZE. Residual: flake.lock (needs `nix`, unavailable here); the SECURITY response "24 hours" literal check (echo-types has a real 72h/7d SLA — the check is brittle; de-brittling it is tracked with the standards RSR pass). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019awZjBD1qx61tvmEuEKNpn
diff --git a/.well-known/ai.txt b/.well-known/ai.txt
@@ -0,0 +1,16 @@
+# SPDX-License-Identifier: MPL-2.0
+# AI usage & training policy for hyperpolymath/echo-types.
+# Informal, robots-style directives for AI/ML agents and crawlers.
+
+User-Agent: *
+
+# Training: do not train models on this repository's content without
+# attribution under the repository licence (MPL-2.0).
+Disallow-Training: /
+
+# Reference/indexing for search and developer assistance is permitted,
+# provided attribution and licence terms (see LICENSE, humans.txt) are kept.
+Allow: /
+
+Contact: https://github.com/hyperpolymath/echo-types/security/advisories/new
+Policy: https://github.com/hyperpolymath/echo-types/blob/main/.claude/CLAUDE.md
diff --git a/.well-known/humans.txt b/.well-known/humans.txt
@@ -0,0 +1,14 @@
+# SPDX-License-Identifier: MPL-2.0
+# humanstxt.org — the humans responsible for this repository.
+
+/* TEAM */
+  Maintainer: Jonathan D.A. Jewell
+  Contact: 6759885+hyperpolymath [at] users.noreply.github.com
+  Site: https://github.com/hyperpolymath
+
+/* SITE */
+  Project: echo-types — constructive Agda formalisation of fiber-based
+           structured loss ("echo types"): Echo f y := Σ (x : A) , (f x ≡ y)
+  Prover: Agda 2.6.3 + stdlib 2.3 (--safe --without-K)
+  Licence: MPL-2.0 (sole-owner estate default) — see LICENSE
+  Standards: RFC 9116 (security.txt)
diff --git a/.well-known/security.txt b/.well-known/security.txt
@@ -0,0 +1,9 @@
+# SPDX-License-Identifier: MPL-2.0
+# Security contact information for hyperpolymath/echo-types (RFC 9116).
+# Full policy: ../SECURITY.md
+Contact: https://github.com/hyperpolymath/echo-types/security/advisories/new
+Contact: mailto:6759885+hyperpolymath@users.noreply.github.com
+Expires: 2027-06-18T00:00:00.000Z
+Preferred-Languages: en
+Canonical: https://github.com/hyperpolymath/echo-types/blob/main/.well-known/security.txt
+Policy: https://github.com/hyperpolymath/echo-types/blob/main/SECURITY.md
diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md
@@ -2,6 +2,27 @@
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 # Code of Conduct
 
-This project follows the [Contributor Covenant 2.1](https://www.contributor-covenant.org/version/2/1/code_of_conduct/).
+This project adopts the [Contributor Covenant 2.1](https://www.contributor-covenant.org/version/2/1/code_of_conduct/). The key obligations are summarised inline so they are enforceable directly from this repository.
 
-Reports go to `j.d.a.jewell@open.ac.uk`. Reports are confidential by default.
+## Our Pledge
+
+We pledge to make participation in echo-types a **harassment**-free experience for everyone, regardless of age, body size, visible or invisible disability, ethnicity, sex characteristics, gender identity and expression, level of experience, education, socio-economic status, nationality, personal appearance, race, religion, or sexual identity and orientation.
+
+## Unacceptable Behaviour
+
+Unacceptable behaviour includes: **harassment** in any form, public or private; trolling, insulting, or derogatory comments; personal or political attacks; publishing others' private information without explicit permission; and other conduct which could reasonably be considered inappropriate in a professional setting.
+
+## Enforcement
+
+Instances of abusive, harassing, or otherwise unacceptable behaviour may be reported confidentially to the maintainer at `j.d.a.jewell@open.ac.uk`. All complaints will be reviewed and investigated promptly and fairly. Reports are confidential by default.
+
+### Enforcement procedures
+
+Maintainers follow these Community Impact Guidelines in determining the consequences for any action they deem in violation of this Code of Conduct:
+
+1. **Correction** — a private, written warning for unprofessional conduct.
+2. **Warning** — a warning with consequences for continued behaviour; no interaction with the people involved for a specified period.
+3. **Temporary ban** — a temporary ban from any interaction or public communication with the community.
+4. **Permanent ban** — a permanent ban from any public interaction within the community.
+
+Maintainers who do not follow or enforce this Code of Conduct in good faith may face temporary or permanent repercussions as determined by the project's leadership.
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -31,3 +31,15 @@ git commit -s -m "feat: ..."
 ## Reviews
 
 At least one maintainer review (see MAINTAINERS.adoc). Bridge-module changes (the cross-system bridges in `proofs/agda/Echo*Bridge*.agda`) need attention because they fix the load-bearing distinctness story; flag them for explicit review.
+
+## Contribution model — Tri-Perimeter Contribution Framework (TPCF)
+
+echo-types follows the estate-wide **Tri-Perimeter Contribution Framework (TPCF)** — graduated trust without gatekeeping:
+
+* **Perimeter 1 — Core Systems (maintainers only).** The proof kernel: `proofs/agda/Echo.agda`, the identity-claim spine, the bridge modules, the `All.agda` / `Smoke.agda` wiring, and the guardrail tooling. Direct commits by maintainers only.
+* **Perimeter 2 — Expert Extensions (trusted contributors).** New proof modules, decoration instances, and ordinal-track slices. Apply via issue → review → merge under the relevant `proofs/agda/` path with the build invariant green.
+* **Perimeter 3 — Community Sandbox (open to all).** Docs (`.adoc`), tutorial walkthroughs, wiki pages, `.well-known/` content, and spec proposals.
+
+### Fork workflow
+
+External contributors use the standard **fork**-and-pull-request workflow: fork the repository, branch from `main`, run `just validate` locally (full Agda verify + kernel-guard), and open a PR. Maintainers (Perimeter 1) may commit directly to feature branches. Every PR must keep `All.agda` + `Smoke.agda` green under `--safe --without-K` and introduce no banned constructs (see the pre-merge checklist above).
diff --git a/Justfile b/Justfile
@@ -105,6 +105,10 @@ stability-report:
 kernel-guard:
 	@sh scripts/kernel-guard.sh
 
+# Aggregate compliance gate: full Agda verify + kernel-guard certificate
+validate: verify kernel-guard
+	@echo "validate: proofs verified + kernel guard passed"
+
 # Default target
 default:
 	just verify
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
@@ -0,0 +1,89 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= echo-types — Proof Status
+:toc:
+:sectnums:
+
+[abstract]
+Honest status of the echo-types Agda formalisation: what is *proved*, what is
+*open*, and the build/guardrail invariant. echo-types is a constructive Agda
+development (`--safe --without-K`); the main verified suite (`proofs/agda/All.agda`)
+is *postulate-free*. The single isolated exception (the order-type *Fidelity*
+scaffold) is enumerated explicitly below.
+
+== Build invariant (verified)
+
+* `--safe --without-K` throughout `proofs/agda/**`.
+* `agda proofs/agda/All.agda` (≈200 modules) and `agda proofs/agda/Smoke.agda`
+  exit 0. Last verified 2026-06-18.
+* Guardrails are CI-enforced (`tools/check-guardrails.sh`): every file under
+  `proofs/agda/**` must declare `{-# OPTIONS --safe --without-K #-}`, and
+  `believe_me`, `postulate`, `TERMINATING`, `REWRITE`, `NO_POSITIVITY_CHECK`,
+  `primTrustMe`, etc. are rejected. The main suite is postulate-free.
+
+== Proved (load-bearing, verified)
+
+=== Composition track
+* `Echo-comp-iso` — base accumulation isomorphism.
+* `cancel-iso` — per-fibre cancellation (parameterised by `s-left`/`s-right` +
+  both triangle identities).
+* Pentagon coherence — `Echo-comp-pent-Σ-assoc` (full Σ-associativity iso).
+
+=== Establishment track — Pillars A–D COMPLETE
+* *A* `EchoFiberBridge.agda` — `echo↔fib` definitional bridge (Echo ≡ fibre).
+* *B* `EchoGradedComonad.agda` (graded-comonad laws) + `EchoPullback.agda`
+  (funext-free, K-free terminal-cone universal property).
+* *C* `EchoSeparating.agda` — separating model; characteristic law refuted.
+* *D* `EchoRelModel.agda` — model-independence theorem (`GCLaws` once for any
+  model) + `docs/echo-types/conservativity.adoc` metatheorem.
+
+=== Canonical-identity spine (Tier 1/2/3)
+`EchoTotalCompletion` (`A ≃ Σ B (Echo f)`), `EchoOrthogonalFactorizationSystem`,
+`EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`,
+`EchoResidueTaxonomy`, `EchoDecorationStructure`, `EchoObservationalEquivalence`,
+`EchoEntropy`, `EchoLLEncoding`, the funext-qualified full-OFS gate `F5`
+(`EchoOFSUnivF5*`), the audience moves (`EchoProvenance`, `EchoSecurity`,
+`EchoProbabilisticSupport`, `EchoDifferential`), `EchoCanonicalIdentitySuite`,
+`EchoDeniability`, and `EchoAggregation` (micro→macro aggregation as an Echo
+map; `aggregate-non-injective` + `no-canonical-disaggregation`).
+
+=== Ordinal / Buchholz track (sound carrier)
+* Doubled-ladder relation `_<ᵇ²_` over the 12 core constructors + the umbrella
+  `rank2-mono-<ᵇ²` + `wf-<ᵇ²` (Gate 1 closed *for the sound carrier*).
+* `RecursiveSurfaceSound._<ᵇʳᶠ²_` + its *unbudgeted* `wf-<ᵇʳᶠ²`.
+* `Ordinal/Brouwer/OrdinalExp.agda` — `ω^^_` + the first ε-number `ε₀`
+  (Bachmann–Howard climb rung 1).
+* `Ordinal/Buchholz/BHTarget.agda` — a real `BHNotation` order + its
+  well-foundedness (no postulate).
+
+== Open (honest — NOT proved)
+
+* *Bachmann–Howard milestone* `ψ₀(Ω_ω)` order-type fidelity — *OPEN*
+  (`D-2026-06-14`). ε₀ is astronomically below the target
+  (ε₀ ≪ Γ₀ ≪ … ≪ ψ₀(Ω_ω)); the collapsing-function climb is the multi-session
+  frontier. The headline ordinal milestone is *not* reached.
+* *`Ordinal/Buchholz/Fidelity.agda` — 2 isolated postulates* (`denotation`,
+  `ordinal-upper-bound`). These are the ONLY postulates in the development,
+  quarantined under `Ordinal/Buchholz/` and tracked in `docs/.../proof-debt.md`
+  + `Fidelity-OPEN-postulates.md`. Dischargeable once the target collapse
+  heights exist.
+* *(epi, mono) image truncation* — `∥_∥` is *constructed* only in the
+  `--cubical` island `EchoImageFactorizationPropCubical.agda`; under
+  `--safe --without-K` it remains a shadow (it cannot be built within
+  `--safe --without-K` without HITs).
+* *Unbudgeted global `wf-<ᵇʳᶠ` over native `_<ᵇ_`* — walled: native `_<ᵇ_` is
+  ordinally unsound (documented counterexample), so no rank embedding maps it.
+  The achievable form landed on the sound carrier (`wf-<ᵇʳᶠ²`).
+* *Pillar E paper* (`docs/echo-types/paper.adoc`) — LIVING DRAFT with `[EXPAND]`
+  tags (background, related work, evaluation, ordinal consumer-evidence
+  appendix gated on the BH milestone). Not submitted.
+
+== Discipline
+
+* No `postulate` in load-bearing tracks (the 2 Fidelity postulates are the
+  sole, isolated, documented exception).
+* Every headline theorem is pinned in `Smoke.agda`; every module is wired into
+  `All.agda` (orphan modules that compile but are not in `All.agda` are treated
+  as dead code).
+* The EI-2 integration-recipe-distinctness investigation is *terminated
+  negatively* and must not be reopened (see `.machine_readable/6a2/STATE.a2ml`).
diff --git a/README.md b/README.md
@@ -512,7 +512,7 @@ cd /var/mnt/eclipse/repos/echo-types
 agda -i proofs/agda proofs/agda/All.agda
 ```
 
-### Installing as a library
+## Installation (as a library)
 
 The repo is structured as an Agda library via `echo-types.agda-lib`
 at the repo root. To use `echo-types` from another Agda project,
@@ -532,6 +532,8 @@ depend: standard-library echo-types
 include: src
 ```
 
+## Usage
+
 Consumers can then `open import Echo`, `open import EchoLinear`,
 or `open import tutorial.region_exit_audit.RegionExitAudit` — the
 library's `include:` line covers both `proofs/agda` and the repo
