feat(v0.3.0): mirror Tier-3 audience-facing spine + LL-encoding gap (#6)

## Summary

- Bumps pin: echo-types `e7dded6` (2026-05-27) → `eed4250` (2026-05-28).
- Adds five module-section shadows: `EchoProvenance` + `EchoSecurity` +
`EchoProbabilisticSupport` + `EchoDifferential` (Tier-3 audience-facing
spine) + `EchoLLEncoding` (cementing-negative).
- Each = finite shadow of a named Agda module; testset comments preserve
the upstream honest-bound discipline (Security is type-level no-section
ONLY; Sampling is TYPE-LEVEL support tracking; Differential is
perturbation tracking).
- Test suite: **253 passing assertions across 18 testsets** (was 162 /
13).

## What's intentionally NOT mirrored

- `EchoOFSUnivF5Iso` (F5-3 composition design) — funext-qualified
upstream; package policy excludes funext-conditional surfaces.
- Ordinal-lane work (Slice 3/4 umbrella, `RankPow*`,
`HeadOmegaInversion`, `RankLexJointBplus`) — separate pillar from the
echo functor / residue / thermo core; needs a new `Bord` carrier in
Julia and an explicit scope agreement before being added.

## Test plan

- [x] `julia --project=. -e 'using Pkg; Pkg.test()'` — green, 253
passing.
- [x] All v0.1.0 + v0.2.0 testsets unchanged and still pass.
- [x] README lookup table updated; "intentionally NOT mirrored" section
expanded with funext-qualified + ordinal-lane carve-outs.
- [x] Source provenance pin bumped in `src/EchoTypes.jl` preamble.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

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.2.0"
+version = "0.3.0"
 
 [compat]
 julia = "1.10"

README.md

@@ -32,9 +32,11 @@ concrete finite data and check their stated laws numerically.
 ## Source of truth
 
 The Agda. This release mirrors `hyperpolymath/echo-types` at
-`origin/main` commit `e7dded61bb25b8f86fb6e116f4e2827ca2044bcf`
-(2026-05-27 head, after the Tier-1+Tier-2 spine + F5 full-OFS
-earn-back + EchoProvenance landed):
+`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 |
 |---|---|
@@ -48,6 +50,11 @@ earn-back + EchoProvenance landed):
 | **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
 
@@ -72,6 +79,26 @@ earn-back + EchoProvenance landed):
   *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
@@ -103,13 +130,16 @@ about itself.
 
 ## Status
 
-`v0.2.0`, local development. The v0.1.0 surface (`Echo`,
-`EchoResidue`, `EchoFiberCount`, `EchoThermodynamics`) is preserved
-unchanged; v0.2.0 adds executable shadows of the Tier-1+Tier-2
-canonical-identity spine that landed upstream on 2026-05-27
-(`EchoTotalCompletion`, `EchoOrthogonalFactorizationSystem`,
-`EchoImageFactorization`, `EchoNoSectionGeneric`, `EchoLossTaxonomy`,
-`EchoEntropy`, `EchoObservationalEquivalence`). Registered as
+`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