Merge pull request #1 from hyperpolymath/claude/add-ordinal-notation-layer-9qhSf

Claude/add ordinal notation layer 9qh sf

Author: hyperpolymath

CLAUDE.md

@@ -0,0 +1,69 @@
+# Ecosystem context
+
+This repo (echo-types) is one node in the hyperpolymath / PanLL ecosystem.
+Adjacent projects, in one line each, for session bootstrapping:
+
+- echo-types — constructive Agda formalization of fiber-based structured
+  loss ("echo types"); `Echo f y := Σ (x : A) , (f x ≡ y)`. Gated
+  identity-claim development; `--safe --without-K` throughout. Current
+  workstream: E (ordinal-notation / Buchholz collapsing layer).
+  https://github.com/hyperpolymath/echo-types
+- PanLL — three-pane cognitive-relief HTI; Ambient/Symbolic/Neural/World panes.
+  https://github.com/hyperpolymath/panll
+- Gossamer — Zig + WebKitGTK webview shell used by PanLL (~5 MB binary).
+- Burble — self-hostable voice-communications platform; Zig-based SIMD
+  audio, IEEE 1588 PTP clock sync, sub-second room joining, browser-based
+  (no downloads / no accounts), configurable topology from single-server
+  to fully distributed mesh. In PanLL, used for team replication via
+  broadcast and as a switchable service alongside Gossamer.
+- Echidna (hyperpolymath) — planned high-assurance interface verification.
+  NOT the Ethereum fuzzer of the same name. Exact repo still to confirm.
+- Ephapax — programming language with a linear type system guaranteeing
+  memory safety for WebAssembly (compile-time "no use-after-free / no
+  memory leaks"). https://github.com/hyperpolymath/ephapax
+- VeriSim / VeriSimDB — identity-state capture with filesystem fallback.
+- VCL-UT (now VCL-total) — next-generation interaction language for
+  VeriSim; designed to satisfy all 10 levels of type safety when
+  proposing, inspecting, and verifying operations in a consonance engine
+  (rather than querying a passive database).
+- Groove protocol — HTTP-based service-discovery mechanism; lets
+  capabilities across the hyperpolymath ecosystem announce themselves
+  for automatic detection and integration (e.g. discipline-specific
+  analyzers becoming visible to PanLL without manual wiring).
+  See GROOVE_PANLL_RESEARCH_SUMMARY.md in panll.
+- ArghDA (planned) — lightweight proof-workspace manager for Agda;
+  triage folders (inbox → working → proven/rejected), linter, DAG view.
+  Split as `arghda-core` (language-agnostic engine) + `arghda-panll`
+  (Gossamer/ReScript presentation). See docs/buchholz-plan.adoc appendix
+  for the motivating proof pipeline.
+
+# This repo
+
+echo-types — constructive Agda formalization of fiber-based structured loss
+("echo types"). Gated identity-claim development per roadmap-gates.adoc.
+
+Current workstream: **E (ordinal-notation / Buchholz collapsing layer)**
+per docs/buchholz-plan.adoc. Aims to land a proof-theoretic collapsing-function
+target — first credible milestone Bachmann–Howard (ψ₀(Ω_ω)), stretch
+target ψ(Ω_Ω) ≈ TFBO.
+
+First landed proof: `C-monotone` in proofs/agda/Ordinal/Closure.agda.
+Next planned: E3 CNF trichotomy, then E4 pedagogical `psi-notin-C`.
+
+# Build
+
+```
+cd /home/user/echo-types
+agda -i proofs/agda proofs/agda/All.agda
+for f in proofs/agda/*.agda proofs/agda/Ordinal/*.agda proofs/agda/Ordinal/Buchholz/*.agda; do
+  [ -f "$f" ] && agda -i proofs/agda "$f"
+done
+```
+
+# Working rules in this repo
+
+- No postulates unless explicitly isolated and justified.
+- `--safe --without-K` throughout.
+- Every edit ends with an Agda compile command and captured output.
+- Every headline theorem must be pinned in Smoke.agda via `using` clause.
+- Branch for ordinal-notation work: claude/add-ordinal-notation-layer-9qhSf.