diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml index d9b09e6..ba3375c 100644 --- a/.machine_readable/6a2/META.a2ml +++ b/.machine_readable/6a2/META.a2ml @@ -22,7 +22,7 @@ author = "Jonathan D.A. Jewell (hyperpolymath)" build-tool = "just" container-runtime = "podman" ci-platform = "github-actions" -package-manager = "guix" # guix | nix | cargo | mix +package-manager = "guix" # guix | guix | cargo | mix [maintenance-axes] scoping-first = true @@ -46,7 +46,7 @@ perfective-source = "axis-1 honest state after corrective/adaptive updates" [axis-3-audit-rules] audit-focus = "systems in place, documentation explains actual state, safety/security accounted for, observed effects reviewed" compliance-focus = "seams/compromises/exception register, bounded exceptions, anti-drift checks" -drift-risk-example = "single exception broadening into policy violation (e.g. ReScript->TypeScript spread)" +drift-risk-example = "single exception broadening into policy violation (e.g. AffineScript->TypeScript spread)" effects-evidence = "benchmark execution/results and maintainer status dialogue/review" [design-rationale] diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/6a2/PLAYBOOK.a2ml index 676ec4c..cdaebfd 100644 --- a/.machine_readable/6a2/PLAYBOOK.a2ml +++ b/.machine_readable/6a2/PLAYBOOK.a2ml @@ -63,7 +63,7 @@ enforcement-workflow = ".github/workflows/estate-rules.yml" # .github/ CONTRIBUTING.md, CODE_OF_CONDUCT.md, SECURITY.md, workflows/ # .machine_readable/ AI manifests (0.1-AI-MANIFEST.a2ml), 6a2/ checkpoints, # contractiles/, configs/, anchors/, policies/, scripts/, svc/ -# build/ contractile.just, flake.nix, guix.scm, Containerfile, +# build/ contractile.just, flake.guix, guix.scm, Containerfile, # just/*.just (Justfile section imports) # docs/ onboarding/, status/, architecture/, governance/ (all .adoc) # session/ dispatch.sh, custom-checks.k9, local-hooks.sh @@ -103,7 +103,7 @@ enforcement-workflow = ".github/workflows/estate-rules.yml" # build/just/groove.just Groove protocol setup (after zig removed) # # Daily-use recipes (BUILD, TEST, LINT, RUN, DEPS, DOCS, CONTAINER, CI, -# SECURITY, STATE, GUIX/NIX, MATRIX, VERSION CONTROL, UTILITIES, SESSION) +# SECURITY, STATE, GUIX/GUIX, MATRIX, VERSION CONTROL, UTILITIES, SESSION) # stay in the root Justfile where users expect to find them. # === 5-PR cleanup pattern === diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index a76d8dd..e24912c 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -32,7 +32,7 @@ milestones = [ { name = "Phase 1e: Trustfile / contractiles", completion = 100 }, { name = "Phase 2: Container ecosystem templates (stapeln)", completion = 100 }, { name = "Phase 3: Multi-forge sync hardening", completion = 0 }, - { name = "Phase 4: Nix/Guix reproducible shells", completion = 50 }, + { name = "Phase 4: Guix/Guix reproducible shells", completion = 50 }, ] [blockers-and-issues] @@ -43,7 +43,7 @@ actions = [ "Container templates complete — test with `just container-init`", "Validate container templates across wolfi-base and static Chainguard images", "Harden multi-forge sync for GitLab/Bitbucket mirroring edge cases", - "Expand Nix/Guix development shell templates", + "Expand Guix/Guix development shell templates", ] [maintenance-status] diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index 2db3d94..a339fff 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -88,7 +88,7 @@ build *args: # cargo build {{args}} # Rust # mix compile {{args}} # Elixir # zig build {{args}} # Zig - # deno task build {{args}} # Deno/ReScript + # deno task build {{args}} # Deno/AffineScript @echo "Build complete" # Build in release mode with optimizations @@ -559,7 +559,7 @@ state-phase: @grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/STATE.a2ml 2>/dev/null | head -1 || echo "unknown" # ═══════════════════════════════════════════════════════════════════════════════ -# GUIX & NIX +# GUIX & GUIX # ═══════════════════════════════════════════════════════════════════════════════ # Enter Guix development shell (primary) @@ -570,9 +570,9 @@ guix-shell: guix-build: guix build -f guix.scm -# Enter Nix development shell (fallback) -nix-shell: - @if [ -f "flake.nix" ]; then nix develop; else echo "No flake.nix"; fi +# Enter Guix development shell (fallback) +guix-shell: + @if [ -f "flake.guix" ]; then guix develop; else echo "No flake.guix"; fi # ═══════════════════════════════════════════════════════════════════════════════ # HYBRID AUTOMATION diff --git a/.machine_readable/root-allow.txt b/.machine_readable/root-allow.txt index 0e6395d..e701242 100644 --- a/.machine_readable/root-allow.txt +++ b/.machine_readable/root-allow.txt @@ -1 +1 @@ -flake.nix +flake.guix diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc new file mode 100644 index 0000000..1c0a7a6 --- /dev/null +++ b/ARCHITECTURE.adoc @@ -0,0 +1,48 @@ +== Architecture + +=== Overview + +This repository follows a modular, maintainable architecture designed +for clarity, scalability, and long-term sustainability. + +=== Directory Structure + +.... +. +├── src/ # Source code +├── tests/ # Test suites +├── docs/ # Documentation +├── scripts/ # Utility scripts +├── config/ # Configuration files +├── LICENSE # License file +├── LICENSES/ # Full license texts +└── README.adoc # Project documentation +.... + +=== Design Principles + +* *Separation of Concerns*: Each module has a single responsibility +* *Testability*: Code is written to be easily testable +* *Documentation*: All public APIs are documented +* *Configuration*: Environment-specific settings are externalized + +=== Dependencies + +* External dependencies are minimized and clearly declared +* Version pinning is used for reproducibility + +=== Security Considerations + +* Sensitive data is never committed to the repository +* Secrets are managed through environment variables or secure vaults +* Regular dependency audits are performed + +=== Maintainability + +* Code follows consistent style guidelines +* Pull requests require review and CI checks +* Issues and discussions are tracked transparently + +''''' + +_Last updated: 2026-07-18_ diff --git a/ARCHITECTURE.md b/ARCHITECTURE.md deleted file mode 100644 index 607e3d8..0000000 --- a/ARCHITECTURE.md +++ /dev/null @@ -1,47 +0,0 @@ -# Architecture - -## Overview - -This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability. - -## Directory Structure - -``` -. -├── src/ # Source code -├── tests/ # Test suites -├── docs/ # Documentation -├── scripts/ # Utility scripts -├── config/ # Configuration files -├── LICENSE # License file -├── LICENSES/ # Full license texts -└── README.adoc # Project documentation -``` - -## Design Principles - -- **Separation of Concerns**: Each module has a single responsibility -- **Testability**: Code is written to be easily testable -- **Documentation**: All public APIs are documented -- **Configuration**: Environment-specific settings are externalized - -## Dependencies - -- External dependencies are minimized and clearly declared -- Version pinning is used for reproducibility - -## Security Considerations - -- Sensitive data is never committed to the repository -- Secrets are managed through environment variables or secure vaults -- Regular dependency audits are performed - -## Maintainability - -- Code follows consistent style guidelines -- Pull requests require review and CI checks -- Issues and discussions are tracked transparently - ---- - -*Last updated: 2026-07-18* diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..065ccd9 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,75 @@ +== Contributing to EchoTypes.jl + +Thanks for your interest. This repository follows the Hyperpolymath +estate standards defined in +https://github.com/hyperpolymath/standards[hyperpolymath/standards]. + +=== Licence + +This project is licensed under *MPL-2.0*. By contributing you agree that +your contributions are licensed under the same terms. Every source file +carries an `+SPDX-License-Identifier+` header; keep it when editing, and +add one to any new file. + +=== Development environment + +A pinned dev shell is provided: + +[source,sh] +---- +guix develop # toolchain: just julia-bin +---- + +Estate policy is Guix primary / Guix fallback; this repo currently ships +the Guix fallback. A `+guix.scm+` is welcome if you prefer the primary +tier. + +=== Build and test + +This repo uses https://just.systems[`+just+`] (the estate uses +Justfiles, never Makefiles). Recipes available here: + +[source,sh] +---- +just # list recipes +just fmt # format +just fmt-check # check formatting +just lint # lint +just test-all # run the full suite +just doctor # environment diagnostics +---- + +=== Machine-readable artefacts + +This repo carries `+.machine_readable/+` A2ML files (`+STATE.a2ml+`, +`+META.a2ml+`, `+ECOSYSTEM.a2ml+`, `+AGENTIC.a2ml+`, `+NEUROSYM.a2ml+`, +`+PLAYBOOK.a2ml+`). If your change alters project state, architecture, +or operational steps, update the corresponding file in the same PR — CI +validates them. + +=== Language policy + +The estate restricts which languages may be used. In particular Python, +Go, TypeScript, AffineScript, V-lang, Java/Kotlin, Swift and Makefiles +are *not* accepted in new code; AffineScript, Rust/SPARK, Zig, Deno, +Gleam, Elixir, Haskell, Idris2, Agda, Julia and OCaml are. CI enforces +this, so check the policy in `+hyperpolymath/standards+` before +introducing a new language. + +=== Documentation format + +Docs are AsciiDoc (`+.adoc+`) by default, including `+README.adoc+`. The +GitHub-required community-health files stay Markdown: `+SECURITY.md+`, +`+CONTRIBUTING.md+`, `+CODE_OF_CONDUCT.md+`, `+CHANGELOG.md+`. Do not +add a `+.md+` duplicate of a doc that already exists as `+.adoc+`. + +=== Pull requests + +[arabic] +. Branch from `+main+` — do not push to `+main+` directly; branch +protection requires review and passing checks. +. Keep the change focused, and explain _why_ in the PR body. +. Make sure governance CI is green. It checks documentation presence, +packaging policy, secrets, licence consistency and workflow security. +. Security issues: follow `+SECURITY.md+` — report privately, never in a +public issue. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index eb86aee..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,72 +0,0 @@ - - - -# Contributing to EchoTypes.jl - -Thanks for your interest. This repository follows the Hyperpolymath estate -standards defined in [hyperpolymath/standards](https://github.com/hyperpolymath/standards). - -## Licence - -This project is licensed under **MPL-2.0**. By contributing you agree that -your contributions are licensed under the same terms. Every source file -carries an `SPDX-License-Identifier` header; keep it when editing, and add -one to any new file. - -## Development environment - -A pinned dev shell is provided: - -```sh -nix develop # toolchain: just julia-bin -``` - -Estate policy is Guix primary / Nix fallback; this repo currently ships the -Nix fallback. A `guix.scm` is welcome if you prefer the primary tier. - -## Build and test - -This repo uses [`just`](https://just.systems) (the estate uses Justfiles, -never Makefiles). Recipes available here: - -```sh -just # list recipes -just fmt # format -just fmt-check # check formatting -just lint # lint -just test-all # run the full suite -just doctor # environment diagnostics -``` - -## Machine-readable artefacts - -This repo carries `.machine_readable/` A2ML files (`STATE.a2ml`, -`META.a2ml`, `ECOSYSTEM.a2ml`, `AGENTIC.a2ml`, `NEUROSYM.a2ml`, -`PLAYBOOK.a2ml`). If your change alters project state, architecture, or -operational steps, update the corresponding file in the same PR — CI -validates them. - -## Language policy - -The estate restricts which languages may be used. In particular Python, Go, -TypeScript, ReScript, V-lang, Java/Kotlin, Swift and Makefiles are **not** -accepted in new code; AffineScript, Rust/SPARK, Zig, Deno, Gleam, Elixir, -Haskell, Idris2, Agda, Julia and OCaml are. CI enforces this, so check the -policy in `hyperpolymath/standards` before introducing a new language. - -## Documentation format - -Docs are AsciiDoc (`.adoc`) by default, including `README.adoc`. The -GitHub-required community-health files stay Markdown: `SECURITY.md`, -`CONTRIBUTING.md`, `CODE_OF_CONDUCT.md`, `CHANGELOG.md`. Do not add a `.md` -duplicate of a doc that already exists as `.adoc`. - -## Pull requests - -1. Branch from `main` — do not push to `main` directly; branch protection - requires review and passing checks. -2. Keep the change focused, and explain *why* in the PR body. -3. Make sure governance CI is green. It checks documentation presence, - packaging policy, secrets, licence consistency and workflow security. -4. Security issues: follow `SECURITY.md` — report privately, never in a - public issue. diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index e41020d..9b836fb 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,162 +1,60 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= Governance Model -:toc: preamble +== Governance -This document describes the governance model for this repository. +=== Overview -== Overview +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. -This repository follows a **Sole Maintainer Governance Model**: +=== Roles and Responsibilities -* Single maintainer (@hyperpolymath) has full authority over the project -* All contributions are welcome and reviewed by the maintainer -* Decisions are made transparently through GitHub issues and discussions -* The project adheres to the hyperpolymath estate policies where applicable +==== Maintainers -== Core Principles +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support -[cols="1,2"] -|=== -| Principle | Description +==== Contributors -| **Benevolent Dictatorship** | Maintainer has final decision authority but seeks community input +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed -| **Meritocracy** | Contributions are judged on technical merit, not contributor identity +=== Decision Making -| **Transparency** | All significant decisions are documented publicly +==== Minor Changes -| **Consensus-Seeking** | Maintainer prefers consensus but will decide when necessary +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates -| **Open Contribution** | Anyone can contribute via fork and pull request +==== Major Changes -|=== +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers -== Roles and Permissions +==== Breaking Changes -[cols="1,2,2"] -|=== -| Role | Permissions | Assignment +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide -| **Maintainer** | Write access, merge rights, admin | @hyperpolymath -| **Contributors** | Read access, fork, submit PRs | All GitHub users -| **Users** | Use the software, report issues | All GitHub users +=== Code of Conduct -|=== +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. -== Decision Making Framework +=== Communication -=== Routine Decisions +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions -* Bug fixes -* Documentation improvements -* Minor feature additions -* Dependency updates +=== Licensing -**Process**: Maintainer reviews and merges PRs that meet quality standards. +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. -=== Significant Changes +''''' -* New major features -* API changes -* Architecture modifications -* Breaking changes - -**Process**: -. Open issue describing the change -. Discuss with community (minimum 72 hours) -. Maintainer makes final decision -. Document rationale in issue/PR - -=== Structural Decisions - -* Repository purpose/renaming -* License changes -* Ownership transfer -* Deprecation/archival - -**Process**: -. Extended discussion (minimum 1 week) -. Maintainer makes final decision -. Document in CHANGELOG and governance docs - -== Contribution Lifecycle - -[cols="1,2"] -|=== -| Stage | Process - -| **Ideation** | Open issue, discuss feasibility - -| **Development** | Fork, implement, test thoroughly - -| **Review** | Submit PR, maintainer reviews within 7 days - -| **Merge** | Maintainer merges or requests changes - -| **Release** | Maintainer publishes according to project conventions - -|=== - -== Conflict Resolution - -In case of disagreements: - -. Discuss in the relevant GitHub issue or PR -. Provide technical justification for positions -. Maintainer mediates and makes final decision -. Decision is documented and can be revisited later - -== Project Policies - -This repository adheres to hyperpolymath estate-wide policies: - -* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) -* **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md -* **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions - -== Repository-Specific Conventions - -[cols="1,2"] -|=== -| Convention | Description - -| **Signing** | All commits must be signed (SSH or GPG) - -| **SPDX Headers** | All source files must have SPDX license identifiers - -| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root - -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ - -| **CI/CD** | GitHub Actions workflows in .github/workflows/ - -|=== - -== Governance Evolution - -As the project grows, this governance model may evolve: - -* **Adding Co-Maintainers**: When contribution volume warrants it -* **Forming a Team**: For complex multi-maintainer projects -* **Adopting TPCF**: For large, multi-repository projects (see rhodium-standard-repositories) - -Changes to this document require the same process as Significant Changes above. - -== See Also - -* link:MAINTAINERS.adoc[Maintainers] -* link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:CONTRIBUTING.adoc[Contributing Guide] -* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] -* link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] - -== Changelog - -[cols="1,1,1"] -|=== -| Date | Change | By - -| 2026-06-07 | Initial governance model established | @hyperpolymath -|=== +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/Justfile b/Justfile index 2db3d94..a339fff 100644 --- a/Justfile +++ b/Justfile @@ -88,7 +88,7 @@ build *args: # cargo build {{args}} # Rust # mix compile {{args}} # Elixir # zig build {{args}} # Zig - # deno task build {{args}} # Deno/ReScript + # deno task build {{args}} # Deno/AffineScript @echo "Build complete" # Build in release mode with optimizations @@ -559,7 +559,7 @@ state-phase: @grep -oP 'phase\s*=\s*"\K[^"]+' .machine_readable/STATE.a2ml 2>/dev/null | head -1 || echo "unknown" # ═══════════════════════════════════════════════════════════════════════════════ -# GUIX & NIX +# GUIX & GUIX # ═══════════════════════════════════════════════════════════════════════════════ # Enter Guix development shell (primary) @@ -570,9 +570,9 @@ guix-shell: guix-build: guix build -f guix.scm -# Enter Nix development shell (fallback) -nix-shell: - @if [ -f "flake.nix" ]; then nix develop; else echo "No flake.nix"; fi +# Enter Guix development shell (fallback) +guix-shell: + @if [ -f "flake.guix" ]; then guix develop; else echo "No flake.guix"; fi # ═══════════════════════════════════════════════════════════════════════════════ # HYBRID AUTOMATION diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..4422477 --- /dev/null +++ b/README.adoc @@ -0,0 +1,249 @@ +== EchoTypes.jl + +https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/EchoTypes.jl[image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssourcesecurity[OpenSSF +Best Practices]] + +An *executable companion* to the Agda library +https://github.com/hyperpolymath/echo-types[`+hyperpolymath/echo-types+`]. + +It computes the *finite-domain shadow* of theorems that are _mechanised_ +in Agda under `+--safe --without-K+` with zero postulates. It lets you +_run_ the echo / residue / Landauer constructions on concrete finite +data and check their stated laws numerically. + +=== What this is — and is not + +* ✅ *It is* a finite, executable model: enumerate fibres, exercise +functoriality and the composition/cancel isomorphisms, lower echoes to +residues, and compute the finite Landauer/Bennett bound shape. +* ❌ *It is not a proof.* Julia has no proof checker. Every guarantee +lives in the Agda. This package can _falsify_ by counterexample but it +cannot _prove_. +* ❌ *No retracted claims appear here.* Per echo-types +`+docs/retractions.adoc+` *R-2026-05-18*, the graded-comonad, +two-models, universal-property and conservativity framings are +`+[RETRACTED]+` and under upstream earn-back gates. None of that surface +is reproduced here. What _is_ here is the post-retraction honest core: a +loss-graded *reindexing* view (Echo functor + functoriality + +accumulation iso), the *residue* weakening (`+EchoR+`, with its strict +non-recoverability witness), and the *finite-domain* Landauer/Bennett +_bound shapes_. + +=== Semantic fibre in finite domains + +The Agda repository is the formal source of truth. This package is the +executable finite-domain shadow: it lets you compute concrete preimage +fibres and inspect what they would license in examples. + +In this companion, a *semantic fibre* is usually the vector returned by +`+fiber(f, domain, y)+`: the finite set of witnesses `+x+` in `+domain+` +such that `+f(x) == y+`. A value is being used *avec fibre* when that +declared map/domain/output triple accompanies it. A value is *sans +fibre* when it is only known as a target-side value; no source-side +origin constraint follows from the value alone. + +[source,julia] +---- +using EchoTypes + +collapse = isodd +avec = fiber(collapse, -2:2, true) # declared map + domain +Set(w.x for w in avec) == Set([-1, 1]) # possible origins + +target_only = true # just a Bool: sans fibre +---- + +Finite examples can demonstrate nontrivial constraints on possible +origins and can falsify over-specific claims by counterexample. They do +not establish proof obligations; those belong upstream in Agda. + +=== Source of truth + +The Agda. This release mirrors `+hyperpolymath/echo-types+` at +`+origin/main+` commit `+eed42503a1a4c54ec0a347ebef3440b4d4db30c9+` +(2026-05-28 head, after the Tier-3 audience-facing spine landed — +EchoProvenance, EchoSecurity, EchoProbabilisticSupport, +EchoDifferential, EchoLLEncoding, plus the EchoCanonicalIdentitySuite +re-export bundle): + +[width="100%",cols="50%,50%",options="header",] +|=== +|Julia surface |Mirrors Agda module / lemmas +|`+EchoWitness+`, `+echo_intro+`, `+fiber+`, `+map_over*+`, +`+comp_iso_*+`, `+cancel_iso_*+` |`+Echo.agda+` (kernel — also re-pinned +via `+EchoKernel.agda+` upstream) + +|`+EchoR+`, `+echo_to_residue+`, `+residue_strictly_loses+` +|`+EchoResidue.agda+` (`+echo-to-residue+`, +`+strict-weakening-collapse+`) + +|`+fiber_size+`, `+flog2+`, `+landauer_bound+`, `+fiber_erasure_bound+`, +`+bennett_reversible+`, `+landauer_collapse+` |`+EchoFiberCount.agda+` + +`+EchoThermodynamics.agda+` + +|*v0.2.0* `+encode+`, `+decode+`, `+*_roundtrip+`, +`+f_factors_via_projection+` |`+EchoTotalCompletion.agda+` (`+A↔ΣEcho+`, +the slogan-unlock) + +|*v0.2.0* `+echo_factorisation+`, `+fibre_of_proj1_*+`, +`+projection_fibre_roundtrips+`, `+ofs_witness+` +|`+EchoOrthogonalFactorizationSystem.agda+` (factorisation existence + +projection-fibre identification — funext-qualified clauses NOT mirrored) + +|*v0.2.0* `+image+`, `+image_factor_*+`, `+is_surjective+`, +`+is_injective+`, `+injective_fibres_proj_unique+` +|`+EchoImageFactorization.agda+` + +|*v0.2.0* `+no_section_of_collapsing_map+`, +`+no_section_when_non_injective_at+` |`+EchoNoSectionGeneric.agda+` + +|*v0.2.0* `+HasInverse+`, `+equiv_fibre_center+`, +`+equiv_implies_injective+`, `+equiv_fibre_proj_unique+`, `+const_fun+`, +`+const_fibre_section+` |`+EchoLossTaxonomy.agda+` (4-case classifier — +EQUIV/INJ/SURJ/CONST K-free skeletons) + +|*v0.2.0* `+collapse_as_fin+`, `+entropy_shadow+`, `+shannon_shadow+`, +`+entropy_shadow_blind+` |`+EchoEntropy.agda+` (discrete Shannon shadow) + +|*v0.2.0* `+LEcho+`, `+EchoMode+`, `+equal_at_mode+`, +`+mode_equality_strictly_finer_at_linear+` +|`+EchoObservationalEquivalence.agda+` (mode-indexed equality) + +|*v0.3.0* `+Provenance+`, `+ProvRecord+`, `+provenance_collapses_at+`, +`+prov_echo_tag1/2+`, `+echoes_distinguish_tag+`, +`+prov_residue_collapses_tags+`, `+bool_over_nat_provenance+` +|`+EchoProvenance.agda+` (Tier-3 audience move 1 — 4 parametric theorems ++ Bool-over-ℕ instance) + +|*v0.3.0* `+Security+`, `+exit_collapses_at+`, `+audit_no_recovery_at+`, +`+region_exit_audit_instance+` |`+EchoSecurity.agda+` (Tier-3 audience +move 2 — per-region audit no-recovery via the generic no-section gadget) + +|*v0.3.0* `+Sampling+`, `+Sample+`, `+support_collapses_at+`, +`+samp_echo_idx1/2+`, `+echo_carries_which_index+`, +`+samp_residue_loses_index+`, `+bool_indexed_nat_sampling+` +|`+EchoProbabilisticSupport.agda+` (Tier-3 audience move 3 — marginal +loses sampling index) + +|*v0.3.0* `+Sensitivity+`, `+Perturbed+`, +`+blur_collapses_perturbations_at+`, `+diff_echo_pert1/2+`, +`+echo_carries_perturbation+`, `+diff_residue_loses_perturbation+`, +`+bool_perturbed_nat_sensitivity+` |`+EchoDifferential.agda+` (Tier-3 +audience move 4 — blur loses perturbation tag) + +|*v0.3.0* `+LLShallowEncoding+`, `+trivial_encoding+`, +`+trivial_encoding_has_section+`, `+ll_encoding_gap+`, +`+source_no_section_holds+`, `+gap_paired+` |`+EchoLLEncoding.agda+` +(cementing-negative — the LL `+!A := 1+` shadow admits an encoded +section paired with source-side no-section) +|=== + +==== What is intentionally NOT mirrored + +* *Funext-qualified surfaces.* The F5 earn-back gate gave the full OFS +(uniqueness up to iso + diagonal lifting) upstream under funext, and +`+EchoPullbackUnivF4+` gives the strict pullback universal property the +same way. Julia has no funext to take as hypothesis; the conditional +claims would be vacuous. Only the unconditional fragment of +`+ofs-witness+` is mirrored. +* *Retracted surface (R-2026-05-18).* Graded-comonad framing, +two-models, universal-property, conservativity. The mechanised laws +survive upstream (and so does the model-independence theorem), but the +_framing_ is retracted; the companion does not reproduce any of it. +* *Higher type-theoretic structure.* UIP-strength claims (full Σ-pair +equality under injectivity, `+A ↔ Echo(const y0)+`, contractible +fibres), propositional truncation (the (epi, mono) collapse of the image +factorisation), and HoTT identification types beyond decidable equality. +The proof-relevant _upper_ of each pair is what’s mirrored, in line with +the `+--safe --without-K+` discipline upstream. +* *Ordinal-lane work (`+Ordinal/Buchholz/*+`).* The Slice-3 + Slice-4 +rank-mono umbrella, `+RankPow*+`, head-Ω inversion, joint-bplus +scaffolds — all live in echo-types’s ordinal pillar, separate from the +echo functor / residue / thermodynamics core this companion mirrors. +Adding ordinal shadows would require a new `+Bord+` carrier in Julia and +a redesigned scope agreement. Not in v0.3.0; out-of-scope for the +companion’s stated discipline. + +==== Honest-bound discipline (Tier 3) + +The four v0.3.0 audience-facing modules ship explicit "`what is NOT +proved`" lists upstream — `+EchoSecurity+` is type-level no-section, NOT +bytes-zeroed / side-channel-safe / tamper-evident; +`+EchoProbabilisticSupport+` is support tracking, NOT measure theory / +coupling / extraction; `+EchoDifferential+` is perturbation tracking, +NOT ε-DP / Lipschitz / noise calibration. The Julia testsets preserve +this scope in their comments. Consumers should not promote a green test +to a real-world security or privacy claim — those need additional +structure beyond the finite shadow. + +Scope limits are inherited honestly: the thermodynamics is a +*finite-domain bound _shape_* in arbitrary natural units — not +quantitative physics, and not defined over infinite state spaces (the +upstream `+Fin n+` restriction). + +==== Downstream bridges (Valence Shell / Ochránce) + +*No current action.* +https://github.com/hyperpolymath/valence-shell[Valence Shell] and +https://github.com/hyperpolymath/ochrance[Ochránce] may later become +downstream _examples_ of Echo Types applied to shell state transitions +and filesystem receipts — but this package does *not* claim to prove +anything about those systems, and no integration is present here. + +If such a bridge is ever added it will be a *toy finite model of residue +classification only*: a fixed finite set of pre-states mapped to +post-states, with fibres / residues computed to classify recoverable +vs. collapsed information — and *no* filesystem, POSIX, secure-deletion, +GDPR, cryptographic-attestation, filesystem-integrity, or +production-security claim attached. Source of truth remains the Agda; +real-world receipt and security guarantees belong to Valence Shell and +Ochránce, not EchoTypes.jl. + +=== Use + +[source,julia] +---- +julia> using EchoTypes + +julia> f = x -> x % 3; # a lossy map + +julia> fiber(f, 0:8, 1) # the constructive Echo fibre over 1 +3-element Vector{EchoWitness{Int64}}: # x = 1, 4, 7 + +julia> fiber_erasure_bound(_ -> 0, 0:15, 0, 7) # full-collapse Landauer bound +28 # = k·T·⌊log₂ 16⌋ = 1·7·4 +---- + +=== Test + +.... +julia --project=. -e 'using Pkg; Pkg.test()' +.... + +The testsets are finite shadows of named Agda lemmas, plus the small +semantic-fibre vocabulary exercise over the kernel. The suite must stay +green and is the only correctness claim this package makes about itself. + +=== Status + +`+v0.3.0+`, local development. The v0.1.0 surface (`+Echo+`, +`+EchoResidue+`, `+EchoFiberCount+`, `+EchoThermodynamics+`) and the +v0.2.0 Tier-1+Tier-2 canonical-identity spine are preserved unchanged; +v0.3.0 adds executable shadows of the Tier-3 audience-facing spine that +landed upstream on 2026-05-27/28 (`+EchoProvenance+`, `+EchoSecurity+`, +`+EchoProbabilisticSupport+`, `+EchoDifferential+`) plus the +cementing-negative `+EchoLLEncoding+` (LL shallow-encoding gap with +paired source-side no-section). Test suite: *258 passing assertions +across 19 testsets*, organised as finite shadows of named Agda lemmas +plus the semantic-fibre vocabulary exercise over the kernel. Registered +as `+EchoTypes+` in the hyperpolymath professional registry; *not* +registered in the Julia General registry and intentionally *not* part of +the AcceleratorGate→KnotTheory→Skein→KRLAdapter chain — it is a +standalone companion. + +=== Licence + +`+MPL-2.0+`; `+MPL-2.0+` (see link:LICENSE[`+LICENSE+`]) is the +automatic legal fallback until PMPL is formally recognised. The LICENSE +file, this statement, and every source SPDX header agree — one +consistent licence, deliberately not a Project-vs-source split. diff --git a/README.md b/README.md deleted file mode 100644 index 1d9f504..0000000 --- a/README.md +++ /dev/null @@ -1,205 +0,0 @@ - - - -# EchoTypes.jl -[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=openssourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/EchoTypes.jl) - - -An **executable companion** to the Agda library -[`hyperpolymath/echo-types`](https://github.com/hyperpolymath/echo-types). - -It computes the **finite-domain shadow** of theorems that are -*mechanised* in Agda under `--safe --without-K` with zero postulates. -It lets you *run* the echo / residue / Landauer constructions on -concrete finite data and check their stated laws numerically. - -## What this is — and is not - -- ✅ **It is** a finite, executable model: enumerate fibres, exercise - functoriality and the composition/cancel isomorphisms, lower echoes - to residues, and compute the finite Landauer/Bennett bound shape. -- ❌ **It is not a proof.** Julia has no proof checker. Every guarantee - lives in the Agda. This package can *falsify* by counterexample but - it cannot *prove*. -- ❌ **No retracted claims appear here.** Per echo-types - `docs/retractions.adoc` **R-2026-05-18**, the graded-comonad, - two-models, universal-property and conservativity framings are - `[RETRACTED]` and under upstream earn-back gates. None of that - surface is reproduced here. What *is* here is the post-retraction - honest core: a loss-graded **reindexing** view (Echo functor + - functoriality + accumulation iso), the **residue** weakening - (`EchoR`, with its strict non-recoverability witness), and the - **finite-domain** Landauer/Bennett *bound shapes*. - -## Semantic fibre in finite domains - -The Agda repository is the formal source of truth. This package is the -executable finite-domain shadow: it lets you compute concrete -preimage fibres and inspect what they would license in examples. - -In this companion, a **semantic fibre** is usually the vector returned -by `fiber(f, domain, y)`: the finite set of witnesses `x` in `domain` -such that `f(x) == y`. A value is being used **avec fibre** when that -declared map/domain/output triple accompanies it. A value is **sans -fibre** when it is only known as a target-side value; no source-side -origin constraint follows from the value alone. - -```julia -using EchoTypes - -collapse = isodd -avec = fiber(collapse, -2:2, true) # declared map + domain -Set(w.x for w in avec) == Set([-1, 1]) # possible origins - -target_only = true # just a Bool: sans fibre -``` - -Finite examples can demonstrate nontrivial constraints on possible -origins and can falsify over-specific claims by counterexample. They -do not establish proof obligations; those belong upstream in Agda. - -## Source of truth - -The Agda. This release mirrors `hyperpolymath/echo-types` at -`origin/main` commit `eed42503a1a4c54ec0a347ebef3440b4d4db30c9` -(2026-05-28 head, after the Tier-3 audience-facing spine landed — -EchoProvenance, EchoSecurity, EchoProbabilisticSupport, -EchoDifferential, EchoLLEncoding, plus the -EchoCanonicalIdentitySuite re-export bundle): - -| Julia surface | Mirrors Agda module / lemmas | -|---|---| -| `EchoWitness`, `echo_intro`, `fiber`, `map_over*`, `comp_iso_*`, `cancel_iso_*` | `Echo.agda` (kernel — also re-pinned via `EchoKernel.agda` upstream) | -| `EchoR`, `echo_to_residue`, `residue_strictly_loses` | `EchoResidue.agda` (`echo-to-residue`, `strict-weakening-collapse`) | -| `fiber_size`, `flog2`, `landauer_bound`, `fiber_erasure_bound`, `bennett_reversible`, `landauer_collapse` | `EchoFiberCount.agda` + `EchoThermodynamics.agda` | -| **v0.2.0** `encode`, `decode`, `*_roundtrip`, `f_factors_via_projection` | `EchoTotalCompletion.agda` (`A↔ΣEcho`, the slogan-unlock) | -| **v0.2.0** `echo_factorisation`, `fibre_of_proj1_*`, `projection_fibre_roundtrips`, `ofs_witness` | `EchoOrthogonalFactorizationSystem.agda` (factorisation existence + projection-fibre identification — funext-qualified clauses NOT mirrored) | -| **v0.2.0** `image`, `image_factor_*`, `is_surjective`, `is_injective`, `injective_fibres_proj_unique` | `EchoImageFactorization.agda` | -| **v0.2.0** `no_section_of_collapsing_map`, `no_section_when_non_injective_at` | `EchoNoSectionGeneric.agda` | -| **v0.2.0** `HasInverse`, `equiv_fibre_center`, `equiv_implies_injective`, `equiv_fibre_proj_unique`, `const_fun`, `const_fibre_section` | `EchoLossTaxonomy.agda` (4-case classifier — EQUIV/INJ/SURJ/CONST K-free skeletons) | -| **v0.2.0** `collapse_as_fin`, `entropy_shadow`, `shannon_shadow`, `entropy_shadow_blind` | `EchoEntropy.agda` (discrete Shannon shadow) | -| **v0.2.0** `LEcho`, `EchoMode`, `equal_at_mode`, `mode_equality_strictly_finer_at_linear` | `EchoObservationalEquivalence.agda` (mode-indexed equality) | -| **v0.3.0** `Provenance`, `ProvRecord`, `provenance_collapses_at`, `prov_echo_tag1/2`, `echoes_distinguish_tag`, `prov_residue_collapses_tags`, `bool_over_nat_provenance` | `EchoProvenance.agda` (Tier-3 audience move 1 — 4 parametric theorems + Bool-over-ℕ instance) | -| **v0.3.0** `Security`, `exit_collapses_at`, `audit_no_recovery_at`, `region_exit_audit_instance` | `EchoSecurity.agda` (Tier-3 audience move 2 — per-region audit no-recovery via the generic no-section gadget) | -| **v0.3.0** `Sampling`, `Sample`, `support_collapses_at`, `samp_echo_idx1/2`, `echo_carries_which_index`, `samp_residue_loses_index`, `bool_indexed_nat_sampling` | `EchoProbabilisticSupport.agda` (Tier-3 audience move 3 — marginal loses sampling index) | -| **v0.3.0** `Sensitivity`, `Perturbed`, `blur_collapses_perturbations_at`, `diff_echo_pert1/2`, `echo_carries_perturbation`, `diff_residue_loses_perturbation`, `bool_perturbed_nat_sensitivity` | `EchoDifferential.agda` (Tier-3 audience move 4 — blur loses perturbation tag) | -| **v0.3.0** `LLShallowEncoding`, `trivial_encoding`, `trivial_encoding_has_section`, `ll_encoding_gap`, `source_no_section_holds`, `gap_paired` | `EchoLLEncoding.agda` (cementing-negative — the LL `!A := 1` shadow admits an encoded section paired with source-side no-section) | - -### What is intentionally NOT mirrored - -- **Funext-qualified surfaces.** The F5 earn-back gate gave the full - OFS (uniqueness up to iso + diagonal lifting) upstream under - funext, and `EchoPullbackUnivF4` gives the strict pullback - universal property the same way. Julia has no funext to take as - hypothesis; the conditional claims would be vacuous. Only the - unconditional fragment of `ofs-witness` is mirrored. - -- **Retracted surface (R-2026-05-18).** Graded-comonad framing, - two-models, universal-property, conservativity. The mechanised - laws survive upstream (and so does the model-independence - theorem), but the *framing* is retracted; the companion does not - reproduce any of it. - -- **Higher type-theoretic structure.** UIP-strength claims - (full Σ-pair equality under injectivity, `A ↔ Echo(const y0)`, - contractible fibres), propositional truncation (the - (epi, mono) collapse of the image factorisation), and HoTT - identification types beyond decidable equality. The proof-relevant - *upper* of each pair is what's mirrored, in line with the - `--safe --without-K` discipline upstream. - -- **Ordinal-lane work (`Ordinal/Buchholz/*`).** The Slice-3 + Slice-4 - rank-mono umbrella, `RankPow*`, head-Ω inversion, joint-bplus - scaffolds — all live in echo-types's ordinal pillar, separate - from the echo functor / residue / thermodynamics core this - companion mirrors. Adding ordinal shadows would require a new - `Bord` carrier in Julia and a redesigned scope agreement. Not - in v0.3.0; out-of-scope for the companion's stated discipline. - -### Honest-bound discipline (Tier 3) - -The four v0.3.0 audience-facing modules ship explicit "what is -NOT proved" lists upstream — `EchoSecurity` is type-level -no-section, NOT bytes-zeroed / side-channel-safe / tamper-evident; -`EchoProbabilisticSupport` is support tracking, NOT measure -theory / coupling / extraction; `EchoDifferential` is perturbation -tracking, NOT ε-DP / Lipschitz / noise calibration. The Julia -testsets preserve this scope in their comments. Consumers should -not promote a green test to a real-world security or privacy -claim — those need additional structure beyond the finite shadow. - -Scope limits are inherited honestly: the thermodynamics is a -**finite-domain bound *shape*** in arbitrary natural units — not -quantitative physics, and not defined over infinite state spaces (the -upstream `Fin n` restriction). - -### Downstream bridges (Valence Shell / Ochránce) - -**No current action.** [Valence Shell](https://github.com/hyperpolymath/valence-shell) -and [Ochránce](https://github.com/hyperpolymath/ochrance) may later -become downstream *examples* of Echo Types applied to shell state -transitions and filesystem receipts — but this package does **not** -claim to prove anything about those systems, and no integration is -present here. - -If such a bridge is ever added it will be a **toy finite model of -residue classification only**: a fixed finite set of pre-states mapped -to post-states, with fibres / residues computed to classify -recoverable vs. collapsed information — and **no** filesystem, POSIX, -secure-deletion, GDPR, cryptographic-attestation, filesystem-integrity, -or production-security claim attached. Source of truth remains the -Agda; real-world receipt and security guarantees belong to Valence -Shell and Ochránce, not EchoTypes.jl. - -## Use - -```julia -julia> using EchoTypes - -julia> f = x -> x % 3; # a lossy map - -julia> fiber(f, 0:8, 1) # the constructive Echo fibre over 1 -3-element Vector{EchoWitness{Int64}}: # x = 1, 4, 7 - -julia> fiber_erasure_bound(_ -> 0, 0:15, 0, 7) # full-collapse Landauer bound -28 # = k·T·⌊log₂ 16⌋ = 1·7·4 -``` - -## Test - -``` -julia --project=. -e 'using Pkg; Pkg.test()' -``` - -The testsets are finite shadows of named Agda lemmas, plus the small -semantic-fibre vocabulary exercise over the kernel. The suite must stay -green and is the only correctness claim this package makes about -itself. - -## Status - -`v0.3.0`, local development. The v0.1.0 surface (`Echo`, -`EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`) and the -v0.2.0 Tier-1+Tier-2 canonical-identity spine are preserved -unchanged; v0.3.0 adds executable shadows of the Tier-3 -audience-facing spine that landed upstream on 2026-05-27/28 -(`EchoProvenance`, `EchoSecurity`, `EchoProbabilisticSupport`, -`EchoDifferential`) plus the cementing-negative `EchoLLEncoding` -(LL shallow-encoding gap with paired source-side no-section). -Test suite: **258 passing assertions across 19 testsets**, organised as -finite shadows of named Agda lemmas plus the semantic-fibre -vocabulary exercise over the kernel. Registered as -`EchoTypes` in the hyperpolymath professional registry; **not** -registered in the Julia General registry and intentionally **not** -part of the AcceleratorGate→KnotTheory→Skein→KRLAdapter chain — it -is a standalone companion. - -## Licence - -`MPL-2.0`; `MPL-2.0` (see [`LICENSE`](LICENSE)) is the -automatic legal fallback until PMPL is formally recognised. The -LICENSE file, this statement, and every source SPDX header agree — -one consistent licence, deliberately not a Project-vs-source split.