Skip to content

Commit 985fc4c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
docs(wiki): add canonical wiki/ source — Home + Exercises + Honest-Bound + Adding-A-New-Shadow (#7)
## Summary - Adds an in-repo `wiki/` directory as canonical source for the EchoTypes.jl wiki — 4 pages (Home + Exercises + Honest-Bound-Discipline + Adding-A-New-Shadow) plus a wiki/README.md documenting the GitHub-wiki sync procedure. - The GitHub wiki at hyperpolymath/EchoTypes.jl/wiki has not yet been web-initialized (fresh wikis need at least one page created via the web UI before the git repo becomes pushable). Until then, this in-repo location is the authoritative source. - Mirrors the upstream-side `echo-types/wiki/Julia-Companion-Exercises` page; same 10 exercises from each repo's perspective. ## Why in-repo - The wiki repo doesn't exist on GitHub yet (404 on `git push`). - Once the user initializes it via the web UI, the content can be one-shot synced (procedure documented in `wiki/README.md`). - In-repo also gives PR review on wiki edits, which the GitHub wiki interface doesn't. ## Pages summary - **Home.md** — entry point + coverage map (15 Agda modules / 18 testsets / 253 passing assertions) + "intentionally NOT mirrored" carve-outs. - **Exercises.md** — 10 hands-on REPL exercises walking through each tier with Agda links + extend-this prompts. - **Honest-Bound-Discipline.md** — category-error catalogue for the 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 proposing new finite shadows of unmirrored echo-types lemmas. ## Test plan - [x] All four pages render as valid GFM markdown. - [x] Cross-links to upstream `echo-types/wiki/Julia-Companion-Exercises` resolve. - [x] Agda-side links point to actual mainline files (verified against echo-types `eed4250`). - [x] `wiki/README.md` sync procedure correctly describes the GitHub-wiki initialization gate. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent a9fe6a3 commit 985fc4c

5 files changed

Lines changed: 741 additions & 0 deletions

File tree

‎wiki/Adding-A-New-Shadow.md‎

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
1+
# Adding a new shadow — submission guide
2+
3+
This guide is for PRs that add a finite shadow of an
4+
echo-types Agda lemma not yet mirrored.
5+
6+
## The bar
7+
8+
Every Julia callable in the package satisfies four invariants. A
9+
new shadow must too:
10+
11+
1. **Named.** It corresponds to a specific Agda module + theorem.
12+
Cite both in the docstring.
13+
2. **Finite-witness-checkable.** The decision procedure terminates
14+
on concrete finite data; no infinitary state, no funext, no
15+
UIP.
16+
3. **K-free.** The Agda module sits under `--safe --without-K`
17+
with zero postulates. (Check the upstream module's first line +
18+
`tools/check-guardrails.sh` clean status.)
19+
4. **Honest-bound documented.** Any matched-negative scope from
20+
the upstream module is preserved in the testset comments.
21+
22+
## What is OUT of scope
23+
24+
These shadow-types are explicitly NOT accepted, even with a
25+
careful implementation:
26+
27+
- **Funext-qualified surfaces** — F5 strict / pullback strict / F4
28+
template anything taking `funext` as a hypothesis. Julia has no
29+
funext primitive; the conditional becomes vacuous.
30+
- **R-2026-05-18 retracted framings** — graded-comonad, universal
31+
property, conservativity, two-models. The mechanised laws survive
32+
upstream under other framings; the retracted *surface* is closed
33+
by policy.
34+
- **HoTT-strength** — UIP-requiring claims (full Σ-pair equality
35+
under injectivity, contractible fibres), propositional
36+
truncation (the (epi, mono) image), HITs.
37+
- **Ordinal-lane work** — Slice 3/4 umbrella, `RankPow*`,
38+
head-Ω inversion, joint-bplus scaffolds. Separate pillar; would
39+
require a new `Bord` carrier in Julia and an explicit scope
40+
agreement before being added. File a discussion first if you
41+
want to pursue this direction.
42+
43+
## PR checklist
44+
45+
The PR description must include:
46+
47+
- [ ] **Agda module + theorem name** the shadow corresponds to.
48+
- [ ] **Finite-shadow-suitability argument** — one sentence on
49+
why this lemma admits a witness-checkable finite form.
50+
- [ ] **Matched-negative block** — what does your test NOT
51+
witness? (Even if the upstream module is silent, list the
52+
obvious non-claims a casual reader might infer.)
53+
- [ ] **Testset added** with at least one passing assertion per
54+
named theorem clause.
55+
- [ ] **README lookup-table row** added under the appropriate
56+
version section.
57+
- [ ] **SoT pin updated** if the upstream commit you're tracking is
58+
newer than the current pin in `src/EchoTypes.jl`'s preamble.
59+
60+
## Suggested template
61+
62+
```julia
63+
# ----------------------------------------------------------------------
64+
# <UpstreamModule>.agda — short description.
65+
#
66+
# Honest scope: <one-line of what's IN>. Out-of-scope per upstream
67+
# matched-negative block: <one-line of what's NOT>.
68+
# ----------------------------------------------------------------------
69+
70+
"""
71+
<julia_callable>(args) -> Bool
72+
73+
`<agda-theorem-name>` (`<UpstreamModule>.agda`): one-line of what
74+
the theorem says. The finite-shadow check returns `true` iff the
75+
witness fires at the supplied data.
76+
"""
77+
function <julia_callable>(args)
78+
# finite computation matching the Agda theorem statement.
79+
end
80+
```
81+
82+
And the testset:
83+
84+
```julia
85+
@testset "<UpstreamModule>: <theorem name>" begin
86+
# HONEST BOUND: <one-line scope reminder>.
87+
88+
@test <julia_callable>(<simple-input>)
89+
90+
# Construction validators fire on misuse.
91+
@test_throws ErrorException <julia_callable>(<deliberately-bad-input>)
92+
end
93+
```
94+
95+
## Review process
96+
97+
Reviews focus on three things:
98+
99+
1. **Does the Agda upstream actually prove what the docstring
100+
claims?** Reviewers will open the Agda module and read the
101+
named theorem. If the docstring drifts from the Agda, the PR
102+
is fixed before merge.
103+
2. **Is the finite shadow faithful?** A shadow that passes for
104+
the wrong reason (e.g., because the test uses an empty
105+
collection) is rejected.
106+
3. **Is the matched-negative block accurate?** If the upstream
107+
module pins explicit non-claims, the PR's testset comments
108+
must reproduce them.
109+
110+
## Examples to study
111+
112+
Existing well-shaped shadows that you can use as templates:
113+
114+
- **Single-headline + worked instance**: `EchoEntropy` / `entropy_shadow`
115+
- **Abstract record + parametric theorems**: `EchoProvenance` /
116+
`Provenance` + `provenance_collapses_at`
117+
- **No-section pattern**: `EchoNoSectionGeneric` /
118+
`no_section_of_collapsing_map`
119+
- **Round-trip identity**: `EchoTotalCompletion` /
120+
`decode_encode_roundtrip`
121+
- **Existence / matched-negative pair**: `EchoLLEncoding` /
122+
`gap_paired`
123+
124+
## Where to ask
125+
126+
- Repo discussions: https://github.com/hyperpolymath/EchoTypes.jl/discussions
127+
- Upstream-side wiki:
128+
[echo-types/wiki/Julia-Companion-Exercises](https://github.com/hyperpolymath/echo-types/wiki/Julia-Companion-Exercises)
129+
- Open an issue if a lemma sits at a scope boundary (HoTT-strength,
130+
funext-qualified) and you want a ruling before opening a PR.

0 commit comments

Comments
 (0)