Residual Evidence Types

Important

Work in progress — early research. A minimal Agda core checks the presence-without-identification example, narrow comparisons with the actual Echo and Epistemic interfaces, dependency-preserving composition, evidence revision and retraction, and a certified finite checker proved to agree with the JavaScript explorer on all 546 configurations. There is no stable API.

Research material for evidence-indexed residual types: representing the alternative explanations compatible with an observation and its declared evidence, and keeping those evidence obligations attached to claims.

The repository’s canonical name is hyperpolymath/residual-evidence-types. The imported assessment uses the earlier proposed name residual-evidence; it is preserved unchanged as a source document.

Imported material

Both source files were copied unchanged from the author’s Windows Downloads folder on 2026-09-09.

File	Contents
Assessment and starting plan	Research judgement, candidate-world formulation, prior-work references, worked example, proof ladder, and proposed implementation direction.
Finite explorer	A standalone HTML/CSS/JavaScript explorer of residual decomposition, presence, value identification, observation coarsening, cancellation, and inconsistent assumptions.

Core idea

For a declared observation function observe, observation r, and evidence predicate E, a candidate is a world w together with evidence that observe(w) = r and E(w) holds. A warranted claim must hold for every admissible candidate. Applying it to reality additionally requires that the actual world belongs to that candidate set.

For example, in the assessment’s natural-number model r = u + n = 2, both (u,n) = (0,2) and (2,0) are initially possible. Assuming n ⇐ 1 establishes that u is nonzero, but leaves (1,1) and (2,0) possible. Presence can therefore be established without identifying a value. Neither conclusion by itself identifies a source or a causal role.

The assessment positions the proposal as a formal library built from ordinary dependent constructions. Its literature-review and novelty judgements are source claims, not independently verified results of this import.

Open the explorer

Open residual-evidence-explorer.html directly in a browser with JavaScript enabled. It is self-contained and requires no package installation or server. Use the five worked-example buttons, then change the residual, noise bound, retained observation, or additional zero-contribution assumption.

The explorer uses signed integers u,n from -6 to 6, whereas the assessment’s small proof example uses natural numbers. Its conclusions are conditional on the declared finite model. Candidate counts are not probabilities.

Current status and limits

The imported assessment and explorer are preserved unchanged. The assessment reports a separate starter archive that has not been recovered here. The src/ core and tests/ comparisons are new work, checked with Agda 2.6.4.3 under --safe --without-K. They do not reproduce or authenticate the missing archive’s claimed results.

Proof status and reproducible commands lists every checked result, the nine expected-rejection controls, exact integration revisions and the standard-library warnings from the Echo comparison.

just check

The core check needs Agda and Just, and uses only Agda’s builtins. just correspondence also needs bun. Optional integration checks take explicit paths to the actual sibling source trees.

The JavaScript explorer is unchanged. just correspondence proves that the certified finite checker in src/ResidualEvidence/Finite agrees with it on every configuration; see the verification record. The source’s references to a starter README, EXPLAINME, and START-HERE describe that separate package.

The assessment’s proposed next research steps (dependency-preserving composition, evidence revision and retraction, and a certified finite checker) are now checked. Confounding types remain a prospective causal specialisation.

Where to start

The research plan starts with presence without identification. That first milestone, its interface comparisons, composition, revision and the certified finite checker now check in CI. Next, decide whether composition and revision add an interface beyond the Echo and Epistemic foundations before expanding the calculus.

nextgen-typing coordinates the shared type-family map and glossary. Residual-specific models, proofs, tests and the explorer belong here.

Licensing

Code, including the Agda modules, shell scripts and the JavaScript explorer, is Mozilla Public License 2.0 (MPL-2.0). Prose documentation, including this README, the assessment and the files under docs/, is CC-BY-SA-4.0. Both texts live in LICENSES/, and the per-file SPDX-License-Identifier headers are authoritative: the imported files keep their original notices (the assessment is CC-BY-SA-4.0, the explorer is MPL-2.0). The GitHub-detected licence is MPL-2.0 (the root LICENSE).