|
Important
|
Work in progress — early research. A new minimal Agda core now checks the presence-without-identification example and narrow comparisons with the actual Echo and Epistemic interfaces. The finite JavaScript explorer remains separate: there is no certified checker, proved explorer correspondence, or 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.
Both source files were copied unchanged from the author’s Windows Downloads folder on 2026-09-09.
| File | Contents |
|---|---|
Research judgement, candidate-world formulation, prior-work references, worked example, proof ladder, and proposed implementation direction. |
|
A standalone HTML/CSS/JavaScript explorer of residual decomposition, presence, value identification, observation coarsening, cancellation, and inconsistent assumptions. |
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 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.
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 three expected-rejection controls, exact integration revisions and the standard-library warnings from the Echo comparison.
just checkThe core check needs Agda and Just, and uses only Agda’s builtins. Optional integration checks take explicit paths to the actual sibling source trees.
In particular, the JavaScript explorer has no proved correspondence to an
Agda implementation in this repository. The source’s references to a starter
README, EXPLAINME, and START-HERE describe that separate package.
The assessment’s proposed next research steps are dependency-preserving composition, evidence revision and retraction, and a certified finite checker. Confounding types are a prospective causal specialisation.
The research plan starts with presence without identification. That first milestone and its narrow interface comparisons now check locally. Next, investigate dependency-preserving composition and evidence revision before expanding the calculus.
nextgen-typing coordinates the shared type-family map and glossary. Residual-specific models, proofs, tests and the explorer belong here.