sync from repo wiki/ — replace stub Home + add Exercises + Honest-Bound + Adding-A-New-Shadow Mirrors the canonical in-repo wiki/ source (landed via PR #7 at hyperpolymath/EchoTypes.jl@main). The four pages: * Home.md — replaces stub with full entry point (quick links, coverage map: 15 Agda modules / 18 testsets / 253 passing assertions, intentionally-NOT-mirrored carve-outs). * Exercises.md — 10 hands-on REPL exercises with Agda links + extend-this prompts; mirror of upstream echo-types/wiki/Julia-Companion-Exercises page. * Honest-Bound-Discipline.md — category-error catalogue for Tier-3 audience surfaces (Security ≠ runtime-secure; Sampling ≠ measure theory; Differential ≠ ε-DP; Provenance ≠ K-provenance semiring; LL gap = existence not universal). * Adding-A-New-Shadow.md — PR submission guide for finite shadows of unmirrored echo-types lemmas. Sync procedure for future updates: edit hyperpolymath/EchoTypes.jl/wiki/<page>.md (via PR), then re-run the copy + push from this wiki repo. See wiki/README.md in the main repo. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

hyperpolymath committed May 28, 2026