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.

Tests and benchmark status

Test and benchmark dashboard records the results by category and their history: 9 core rejection controls, 2 actual sibling comparisons, 6 sibling rejection controls with independently checked prefixes, 11 explorer tests and correspondence over 546 configurations. Proof run 41674253389 passed for PR head 6fe57a2, whose code tree matches merged main 69a4637. Performance benchmarks have no measured baseline; these are correctness checks, not latency, throughput or memory measurements.

Estate audit findings and scope explains the repository checks, outstanding shared-check defects and the separate scanner startup blocker. Maintainer and project references are in humans.txt and trust.txt.

The repository’s canonical name is hyperpolymath/residual-evidence-types. The imported assessment uses the earlier proposed name residual-evidence; its historical content is preserved in the migrated AsciiDoc source document.

Imported material

Both source files were copied unchanged from the author’s Windows Downloads folder on 2026-09-09. The assessment’s formatting was migrated to AsciiDoc on 2026-11-03, preserving its wording, citations, equations, table and code example. Its provenance note links the original Markdown at the immutable import commit. The explorer remains unchanged.

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

2026-10-12: the expected outcome of the family-or-view question is family. The mirror proves that dependence (which assumptions a verdict rests on) is not a function of the candidate set; this result still needs to be re-proved against this repository’s own record. See docs/DECISION-002-family-or-view.adoc. Holds, the verdicts and the thesis sentence are a view on Epistemic over Echo. Dependence is the proposed additional interface.

2026-11-03: the sibling comparisons now include composition and coarsening over Echo.Echo, and non-vacuity, retraction and revision through the actual Epistemic SoundWarrant interface. These extensions and all six sibling rejection controls passed hosted run 41671834379 for PR head 05a92c2; Proof status records the exact checkout, matching code tree and scope. They address nextgen-typing#115, AC2 and AC3. Transporting these operations does not establish that every residual law is an instance of a sibling law or settle the family-or-view decision.

The imported assessment’s content is preserved through its format migration; the explorer remains unchanged. The assessment reports a separate starter archive that has not been recovered here. The src/ core and tests/ comparisons are new work. Their verified scope and exact revisions are recorded against Agda 2.6.4.3 in the hosted receipts. Receipts before the --cubical-compatible profile was adopted were made under --safe --without-K and are historical evidence for that profile only. They do not reproduce or authenticate the missing archive’s claimed results.

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

The optional Epistemic comparison also relates source identification on an inhabited joint visible/residue fibre to the sibling’s partial recovery interface. The converse construction explicitly requires an image decision procedure; projecting a case’s consistency witness does not implement recovery from the pair. See the separate local partial-recovery inventory in the proof status.

just check
just check-siblings

The core check needs Agda and Just, and uses only Agda’s builtins. just check-siblings fetches the pinned sibling sources and runs their positive comparisons and rejection controls. just check-all combines the core and sibling checks. just correspondence separately needs bun. The individual positive integration recipes also accept 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).