This is the shared reading guide for the six research families in the map. It coordinates vocabulary and ownership; the owning repositories define their formal interfaces and carry their proof evidence.
Read every dashed arrow as a conceptual use or a proposed research task. An arrow does not assert a package dependency, a checked bridge, an equivalence, or a theorem. Residual Evidence Types now has a checked minimal Agda core, two narrow interface comparisons, and a certified finite checker proved to agree with its explorer, described below with proof receipts. Those results do not discharge every obligation represented by an arrow.
| Family and owner | Question and object | Boundary |
|---|---|---|
Which possible origins lie over an output after a transformation?
|
An output need not identify its actual origin. A numeric measure of a residue does not determine the residue’s structure. |
|
From which standpoint is a claim available, and with what evidence?
|
Possessing evidence is not automatically a proof of its claim. Belief, knowledge and a sound warrant have different interfaces. |
|
How do resource bounds compose? A declared resource algebra supplies
operations and laws: max-plus can combine alternatives with |
The algebra and cost semantics must be stated. A bound is neither a probability nor the identity of an information residue. |
|
Which worlds satisfy both an observation and its evidence constraints?
|
The world is not recovered just by constructing a candidate. Real-world soundness also needs the premise that the actual world is admissible. The formal library is work in progress. |
|
What happens to retained distinctions, resource bounds and warrants when a global interaction protocol is projected to local participants? |
The general K-CUT result is open in the reviewed project description. A causal-order frontier called a cut is not Gentzen cut-elimination; it is also not a statistical causal-identification result. |
|
Which value flows does a confidentiality label permit, and what may a
lower-cleared observer learn from an output? A |
A label is not cryptography and not an epistemic standpoint: |
These are complementary research questions, not successive ranks in a universal hierarchy of type-system strength. They may be expressible using ordinary dependent, refinement, modal or graded constructions. A name alone does not establish a new primitive type or a novelty claim.
| Term | Meaning in this guide |
|---|---|
Observation |
The result of a declared observation function. Keeping only its sign or magnitude changes that function and can merge distinctions. |
Fibre / fiber |
Origins paired with evidence that the observation function maps them to the specified output. The two spellings mean the same thing. |
Candidate world |
One world with evidence of observation compatibility and the declared constraints. It is an admissible explanation, not an assertion that this world actually occurred. |
Residual |
A discrepancy relative to a declared model. In the imported
example it is |
Residue |
Information retained after a transformation. An Echo residue is not synonymous with a numerical residual or an error term. |
Evidence constraint |
A predicate restricting candidate worlds. Choosing a bound in an explorer does not establish that real observations obey it. |
Standpoint |
The agent, observer or evidence state from which a claim is available. It is an explicit index, not necessarily a probability. |
Warrant |
Evidence for a claim from a standpoint. Soundness needs a separate map from that evidence to the specified claim meaning. |
Soundness |
A stated guarantee connecting evidence or a successful check to the meaning of a claim, under explicit premises. |
Presence |
Every admissible world has a nonzero contribution. A meaningful case also requires evidence that at least one world is admissible. |
Value identification |
The queried contribution has the same value in every admissible world. This does not identify a source or its causal role. |
Confounding |
A prospective causal specialisation, requiring a causal model and its identification assumptions. An unresolved additive contribution alone does not establish a confounder. |
Inconsistency |
No candidate satisfies the declared model and constraints. The explorer reports a conflict and issues no presence or identification claim; it does not use an empty candidate set as a useful warrant for every claim. |
Resource grade |
An element of a declared resource algebra used for compositional usage or cost accounting. Which operations compose which behaviours is explicit. |
Echo index |
An index of retained information or allowed degradation. It is distinct from a resource grade and from a numerical measure of a residue. |
Residue measure |
An observation of retained information into a measuring domain. Equal measured values need not mean equal retained information. |
| Connection | Conceptual relationship | Evidence needed for a stronger claim |
|---|---|---|
Echo → Residual Evidence |
Refine the observation fibre with the evidence predicate |
The first core checks an encoding into |
Epistemic → Residual Evidence |
Make the meaning and evidence obligations of candidate-wide claims explicit. |
The first core checks a |
Echo → Choreographic |
Track the distinctions retained by projection to participants. |
A projection model and correspondence theorem. An informal loss number cannot stand in for the structure of an Echo residue. |
Epistemic → Choreographic |
Transport warrants with declared standpoint and soundness conditions. |
The relevant K-CUT-WARRANT statement and its proof, including its side conditions. |
Tropical → Choreographic |
Compose bounds for interactions using a stated resource algebra. |
A grading semantics and a projection theorem. A result in another proof assistant needs a proved correspondence or a port with its laws re-proved. |
The Choreographic README reviewed for this guide uses the phrase "echo loss-grade". The Echo foundation contract explicitly separates Echo indices, residue measures and resource grades. This map preserves that distinction; reconciling the choreographic interface is an open coordination task, not an equivalence asserted here.
-
nextgen-typing: this map, the shared glossary, ownership routing, comparisons and explicitly cross-project integration obligations. -
residual-evidence-types: the residual model, research plan, explorer, Agda core, and tests or proofs specific to that model. -
echo-types,epistemic-types,tropical-types,choreographic-types: each family’s definitions, implementations and own proof evidence. -
secret-types: the confidentiality-label and information-flow specification: its question, boundary, first two-level model and review checklist. It is specification-stage — noSecrettype, information-flow calculus, declassification rule or noninterference theorem exists there yet — so this guide asserts no connection obligation for it, and a documentation link is not a mechanised dependency. -
kategoria: language-development experiments. It is a separate project from the oldkatagoriarepository name, which GitHub now resolves toideas-to-alphas. -
typell: verification-kernel implementation;typed-wasm: target and ABI work;panll: the consuming environment. A conceptual connection in this guide does not establish that any family is integrated into these projects.
The machine-readable ownership rules are in placement.a2ml.
The first argument is presence without identification. In natural numbers,
u+n=2 alone admits both (0,2) and (2,0). Adding n≤1 proves u≠0,
but (1,1) and (2,0) still disagree on the value of u. Adding u=0
then makes the constraints inconsistent, so no inhabited case can be built.
The new core also checks ordinary evidence-refined fibre round trips,
conditional actual-world soundness, and claim transport under evidence
refinement. Three deliberately invalid modules must be rejected by Agda.
Both actual sibling interfaces are imported by the comparison modules:
Echo’s fibre packaging round-trips, and Epistemic’s SoundWarrant requires
explicit actual-world premises.
The proof record
lists the theorem names, commands, pinned sibling revisions and standard-library
warnings. The hosted Agda proof job
passed the core, all three rejection controls and both comparisons on 2026-09-22
for commit 938a7a5764ac18f08b1b7f332378b4d29c32aa37, with the sibling pins at
the current echo-types (9c4b72b5) and epistemic-types (dd948fbd) heads,
inside a digest-pinned Debian 13 container with Agda 2.6.4.3 and no third-party
action. The first receipt, run 34400282291 on 2026-09-09, checked the same core
at the original pins.
This is newly written work; the separate starter archive mentioned in the
imported assessment has not been recovered.
Causal specialisations and probability adapters require their own models and obligations.
The second milestone adds contexts of assumptions with thinnings,
dependency-preserving composition and coarsening, constructive evidence
revision and retraction, a certified finite checker over the explorer’s signed
-6..6 model, and a proved correspondence between that checker and the
JavaScript explorer: Correspondence.checker-matches-explorer states
Checker.table ≡ ExplorerTable.expected over all 546 configurations and is
proved by refl. Nine deliberately invalid modules must now be rejected.
The updated proof record
lists the theorem names and boundaries. The
hosted proof job
passed on 2026-09-30 for commit befdf9641c1bc6ecf58946e5ccbd0c630f4fc4c3:
the core, all nine rejections, both comparisons, and the explorer
correspondence (bun 1.3.14 verified by SHA-256 and SHA-512, 11 harness tests,
byte-for-byte table drift check, and the refl proof), in the same
digest-pinned Debian 13 container with Agda 2.6.4.3.
The limit matters: the correspondence certifies the finite checker against
the explorer, not the natural-number core against the explorer. The two
sibling comparisons still cover the first milestone only; whether composition
and revision need an interface beyond Echo.Echo and SoundWarrant is the
open question for the next milestone.
Reviewed on 2026-09-09: the local README files for the six type-set projects
echo-types, epistemic-types, tropical-types, choreographic-types,
kategoria and typell; the imported residual assessment and explorer; and
the coordination repository’s placement, architecture and roadmap documents.
The residual core and its two direct comparison modules were checked locally
and in the linked hosted job with Agda 2.6.4.3 under --safe --without-K.
This is a bounded result: the complete constituent proof suites were not
rerun, and unrelated local Epistemic work is outside the receipt.
The Secret Types row was added on 2026-10-05 from that repository’s reviewed
and merged scope statement (secret-types PR #4, merged 2026-10-04, with the
2026-10-04 owner confirmation and rulings D153 and D154 recorded there). The
row registers the family on its stated boundary; it is not an implementation
claim. The scope statement itself records that no Secret type,
information-flow calculus, declassification rule or noninterference theorem
exists yet, that its review checklist has not been completed item by item, and
that no consumer or frontier item is selected, so no connection obligation is
asserted for it in this guide.
Primary project entry points:
GitHub repository API lookups on that date resolved tropical-resource-typing
to tropical-types and katagoria to ideas-to-alphas, while kategoria
resolved to its own repository. The historical pipeline documents retain
the katagoria spelling; do not silently conflate it with kategoria.
The graphic is a checked-in SVG so it displays in the AsciiDoc README without
JavaScript or a diagram service. Its editable source is
type-connections.dot. Rebuild it with
just type-map (Graphviz required).