Epistemic Types — Standpoint-Indexed Modalities and Proof Transport

Constructive Agda prototype for standpoint-indexed epistemic modalities, separating knowledge, belief, and warrant, with proof transport sound relative to an explicit claim meaning.

The query-recovery extension distinguishes answering a query from recovering its source, states observer safety for generated inputs, and characterises sufficient residue relative to already visible information.

Contents

• Overview
• The modality spectrum
• Warrants
• Accessibility and surreal standpoints
  • The surreal bridge
• Store-coherent reads and certified residues
• Applications: the RapidNJ Q-criterion
• Proof transport across trust boundaries
• What is standard and what is ours
• What remains intentionally unformalized
• Build
• Documentation
• License

Overview

When an agent observes a fact, the type of their access matters. Knowledge is factive; belief is not. A warrant records evidence without assuming soundness. Proof transported across a boundary becomes a receipt; a receiving proof requires a successful sound check of the receiver’s claim meaning.

Epistemic types provide a mechanised vocabulary for these distinctions. Given a type of standpoints K (agents, observers, evidence states), the modality E : K → Set ℓ → Set ℓ reads: E κ A is the type of A as epistemically available from standpoint κ.

This repo does not define a complete epistemic logic. It provides Kripke semantics and the minimal interfaces — factive vs. non-factive modalities, warrants, accessibility preorder, and compositional proof transport — and proves the structural laws that hold generically, while making explicit what must be assumed.

The modality spectrum

The base interface treats E as an indexed endofunctor. Stronger structure is added incrementally, each as a separate record:

Interface	Structure added	Intended reading
Modality	E, map	Plain indexed endofunctor
LawfulModality	Functor identity + composition laws	map respects structure
FactiveModality	reflect : E κ A → A	Knowledge (veridical: what is available is true)
BeliefModality	Intentionally no reflect	Belief (non-factive: available does not imply true)
ReturnModality	return : A → E κ A	Strong introduction (internal observation)

Monadic (bind) and comonadic (extract) structure are not provided by default. They are future commitments, not hidden assumptions.

Warrants

A warrant records the type of evidence for a claim without assuming the evidence is valid:

• Warrant K κ A — the type of evidence tokens for A from standpoint κ.

• Epi K κ A — an evidence token paired with its warrant type.

• SoundWarrant — a separate interface adding a soundness map from that warrant’s Evidence to A. Not assumed by default.

This separates "I have a receipt for A" from "A is true."

Accessibility and surreal standpoints

Standpoint access is modelled by a preorder κ ≤κ κ' (read: κ' is at least as informed as κ). Transport increase moves epistemic availability along this order.

The surreal bridge

SurrealBridge enriches the preorder with an instance-supplied access grade. Its laws specify composition; they do not establish a physical cost or an information-loss measure:

magnitude-loss : x ≤♯ y → Grade
loss-refl      : magnitude-loss refl ≡ finite zero
loss-trans     : magnitude-loss (trans p q) ≡ gradePlus (magnitude-loss p) (magnitude-loss q)

Its concrete Echo adapter relaxes a proved upper bound on a residue measure along p : x ≤♯ y, while preserving the retained value:

E x (BoundedEcho C measure r visible)
  → E y (BoundedEcho C measure (gradePlus r (magnitude-loss p)) visible)

The concrete daySurrealAccess instance models the finite birthday tower using Nat standpoints, where the grade is the number of refinement steps. This is a set-sized fragment, not the full Conway proper class of surreals.

Store-coherent reads and certified residues

ReadConsistency now models finite store histories. A ReadView s proves its value equals contents s; a cached read records its source history and ancestry. Writes make existing caches stale. synchronize reads current contents in the model, while preserving evidence across a change requires an explicit proof. The former version-only relabelling and free Sync witness have been removed.

Echo C y carries a residue satisfying the relation specified by Retention C. Source compatibility is explicit in MatchesSource; exact recovery and migration need their respective round-trip and adequacy laws. A checked counterexample shows that discarded distinctions cannot support a migration requiring those distinctions. Resource grades are separate, measured upper bounds.

See the breaking API correction and proof boundaries. The optional integration gate connects the actual sibling EchoResidue.EchoR and EchoFiniteResidue.ExactRecovery records. The recovery adapter preserves the full decoder and supplied round-trip proof, transfers the finite-alphabet bound, and includes certificate, collision and off-image controls. See the contract and reproduction commands. The core remains dependency-free.

Applications: the RapidNJ Q-criterion

The Applications/ tree is where the core interfaces are exercised against algorithmic claims that arrive with their own arithmetic. Its first example is the per-row branch-and-bound rule used by RapidNJ (Simonsen, Mailund, Pedersen 2008) when searching for the neighbour-joining minimum: while scanning a row of distances in increasing order, the row is abandoned as soon as

qBound = (r - 2) * d(i,next) - t(i) - t_max

is at least the incumbent q_min, because no unexamined entry can beat it.

The development is order-generic: Applications.QCriterion.qBound-≤-Q proves the bound for any carrier with monotone addition, antitone negation and a transitive order — no multiplication or division of carrier elements occurs anywhere, and the coefficient (r - 2) enters only as a Nat-indexed repeated sum. A skip certificate carries the sorted-row invariant, the running-maximum invariant and an accepted executable check; Applications.RapidNJSkip then generates a warrant for the skipped quadrant, and its soundness map is exactly the reflect of a FactiveModality:

run data -> skipWarrant -> skip-sound (the bound lemma) -> reflect -> the claim

So skipping a quadrant yields knowledge only through a proved bound, never by assumption, and the same run held without the soundness map is belief. The integer model is discharged in full (Applications.IntegerModel, Applications.RapidNJExamples); the rational case is a stated obligation, not a claim — see the applications note for the rescaling argument and the exact-arithmetic seam.

Proof transport across trust boundaries

ProofTransport is parameterised by agents, claim labels, artefacts, Meaning : Agent → Artifact → Claim → Set, and a certificate Payload : Artifact → Claim → Set. The caller states the meaning being proved.

A CertificateCheck contains an executable Boolean check and a proof that acceptance entails that exact meaning. Evidence carries a payload; possessing it alone proves nothing. A proof constructor also requires runChecker checker evidence ≡ true.

proofSound : View holder a Proof c -> Meaning holder a c

verify evaluates the checking function and returns InvalidEvidence on rejection. transmit produces a receipt at the receiving holder. publicIsPortable requires an explicit implication between the two holders' meanings; it does not silently relabel holder-dependent truths.

The example checks Boolean artefacts and certificates, proves legitimate acceptance, and refutes false claims. It does not claim that a physical action occurred. The older token-only model lacked semantic soundness; the strengthened interface is a breaking correction documented in docs/proof-transport.adoc.

What is standard and what is ours

Concept	Status	Home in this repo
Indexed endofunctor / modality	Standard	EpistemicTypes.Base
Knowledge (factivity) vs. non-factive belief distinction	Standard distinction; this minimal API does not claim S5 or KD45	EpistemicTypes.Base
Warrant types without assumed soundness	Project-specific emphasis	EpistemicTypes.Warrant
Preorder accessibility with transport	Standard	EpistemicTypes.Access
Resource-bound transport on surreal-like standpoints	Project-specific composition; no novelty theorem	EpistemicTypes.SurrealBridge
Proof transport with explicit semantic soundness	Novel formalisation	EpistemicTypes.ProofTransport
Order-generic RapidNJ Q-criterion bound and skip warrants	Transcription of a documented algorithm; no novelty theorem	EpistemicTypes.Applications.QCriterion

What remains intentionally unformalized

Note

2026-10-12: Kripke semantics, the frame-condition correspondences, a non-factive model (Warrant ≠ SoundWarrant witnessed), the residual-evidence frame and the dependence test now live under src/EpistemicTypes/Kripke/; see docs/kripke-status-2026-10-12.adoc. Choreographic-types externally proves soundness for type-determined warrants in its finite binary/plain-merge fragment at the recorded revision d8536184366f4ac4567aa066c5dbcb9220e3607a, with a successful CI type-check; that result is not re-checked or generalised here (E-6). Soundness for data-dependent warrants remains open and is not assumed by this repository.

Caution

This is a prototype, not a complete epistemic logic. The following are intentionally omitted as future commitments, not hidden assumptions:

• Complete epistemic logic

• Graded comonad for echo-type composition

• Proof irrelevance or decidability

• Soundness for data-dependent warrants

• Monadic (bind) or comonadic (extract) structure for E

• A rational (ℚ) instance of the applications layer, and the rescaling transport that would lift the integer certificate to rational input

• Cross-iteration reuse of a skip bound, and the row-insertion update that maintains the scan invariants (Applications.RapidNJSkip.WeakeningObligation)

• Confidentiality labels, secret types, declassification, and noninterference — out of scope for this repository. The standalone home is hyperpolymath/secret-types (D153/D154); the boundary/history note records the decision and the pointer. No Secret API exists here. Issue #32 was closed on 2026-10-05 as delivered here (no transfer; the successor guard is #39); the transition review records the cross-references, and the boundary note’s 2026-10-25 status update records the standalone repository’s proved noninterference theorem.

Build

just check  # policy guard + 31 positive modules + 24 expected rejections + 4 mutation controls

just check calls scripts/check.sh: it uses a local agda when one is on PATH, and otherwise enters the checked-in Guix environment. The explicit forms are:

bash scripts/check.sh
guix shell -D -f build/guix.scm -- bash scripts/check.sh

The repository ships a dev container whose image is pinned to the same Debian 13 base digest as CI and installs the same Agda (agda-bin=2.6.4.3-1+b2); its postCreateCommand runs just check, so a first run either reproduces both gates or reports the failing one. See .devcontainer/README.adoc.

To check a single module or the aggregate directly:

agda --no-libraries --safe --without-K --cubical-compatible \
  --double-check --ignore-interfaces \
  -W error -W noUnsupportedIndexedMatch \
  -i src src/EpistemicTypes/All.agda

Agda 2.6.4.3’s UnsupportedIndexedMatch category is disabled in the strict pass, then rerun without warnings-as-errors and compared with the exact 23-span manifest in tests/check-proofs.sh. A warning at a new location, or a stale manifest entry, fails the gate. The proofs check in safe mode; the repository does not claim that those indexed eliminations compute when applied to Cubical transports. All other warnings remain errors.

Documentation

• EXPLAINME — claim-by-claim receipts and proof ledger

• Proof status / proof needs — current verification grade, trust boundaries, and open proof legs

• Kripke status — exact constructive frame scope and warrant boundary

• Continuity foundations — store coherence, retained information, bounds, and next obligations

• Proof transport — semantic verification across boundaries

• Applications: the RapidNJ Q-criterion — the bound, the skip warrant, the exact-arithmetic obligation

• Secret types — boundary and history — why the two-level information-flow proposal is not implemented here; the standalone home is hyperpolymath/secret-types (D153/D154)

License

SPDX-License-Identifier: MPL-2.0 — see LICENSE.