Merge branch 'main' into license/migrate-to-mpl-2.0

Author: hyperpolymath

.github/ISSUE_TEMPLATE/bug_report.md

@@ -0,0 +1,38 @@
+---
+name: Bug report
+about: Create a report to help us improve
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Describe the bug**
+A clear and concise description of what the bug is.
+
+**To Reproduce**
+Steps to reproduce the behavior:
+1. Go to '...'
+2. Click on '....'
+3. Scroll down to '....'
+4. See error
+
+**Expected behavior**
+A clear and concise description of what you expected to happen.
+
+**Screenshots**
+If applicable, add screenshots to help explain your problem.
+
+**Desktop (please complete the following information):**
+ - OS: [e.g. iOS]
+ - Browser [e.g. chrome, safari]
+ - Version [e.g. 22]
+
+**Smartphone (please complete the following information):**
+ - Device: [e.g. iPhone6]
+ - OS: [e.g. iOS8.1]
+ - Browser [e.g. stock browser, safari]
+ - Version [e.g. 22]
+
+**Additional context**
+Add any other context about the problem here.

.github/ISSUE_TEMPLATE/custom.md

@@ -0,0 +1,10 @@
+---
+name: Custom issue template
+about: Describe this issue template's purpose here.
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+

.github/ISSUE_TEMPLATE/feature_request.md

@@ -0,0 +1,20 @@
+---
+name: Feature request
+about: Suggest an idea for this project
+title: ''
+labels: ''
+assignees: ''
+
+---
+
+**Is your feature request related to a problem? Please describe.**
+A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]
+
+**Describe the solution you'd like**
+A clear and concise description of what you want to happen.
+
+**Describe alternatives you've considered**
+A clear and concise description of any alternative solutions or features you've considered.
+
+**Additional context**
+Add any other context or screenshots about the feature request here.

Project.toml

@@ -6,7 +6,7 @@
 name = "EchoTypes"
 uuid = "a8ca608b-856a-4215-8c3d-f9ffd1705524"
 authors = ["Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>"]
-version = "0.1.0"
+version = "0.3.0"
 
 [compat]
 julia = "1.10"

README.md

@@ -32,24 +32,72 @@ concrete finite data and check their stated laws numerically.
 ## Source of truth
 
 The Agda. This release mirrors `hyperpolymath/echo-types` at
-`origin/main` commit `2ca31220e3efdcf2708e6d2e04869993fbb1e53a`:
+`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) |
+| `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` |
-
-> **Pending upstream (forward-reference, not yet tracked):** the
-> mirrored kernel surface above corresponds to the curated funext-free
-> core being introduced upstream as `proofs/agda/EchoKernel.agda` in
-> echo-types **PR #56** (`foundation/echo-kernel-2026-05-18`, open at
-> time of writing). It is *not* on `origin/main` yet, so the SoT pin
-> deliberately stays at `2ca3122` (canonical `main`). When PR #56
-> merges, this pin bumps to the actual squash-merge commit and the
-> table row gains an explicit `EchoKernel` reference. Until then, this
-> companion tracks `Echo.agda` directly — `EchoKernel` adds no new
-> mathematics, only a curated re-export + a funext-free certificate.
+| **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
@@ -82,11 +130,20 @@ about itself.
 
 ## Status
 
-`v0.1.0`, local development. **Not registered** in the Julia General
-registry and intentionally **not** part of the
-AcceleratorGate→KnotTheory→Skein→KRLAdapter registration chain — it is
-a standalone companion, registered only on its own merit if and when
-that is warranted.
+`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: **253 passing assertions across 18 testsets**, each
+the finite shadow of a named Agda lemma. 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