Correct but Unauditable: Verifying a Single Source of Truth at Intersymbolic Boundaries

Counts differ because each database indexes a different set of publications. We treat OpenAlex as the canonical count; Google Scholar is not shown (no API, and crawling it violates its ToS).

A log and cache can agree on every value while hiding which cell answered. A retriever or neural router can likewise omit the selected record or executed tool. A system can therefore return the correct value while hiding what produced it. We develop an Event-B workflow for auditing this gap. A versioned audit contract identifies the authoritative source, mandatory derivation edges, and execution fact the interface must reveal. The boundary-evidence proof obligation (BEP) checks whether cases with indistinguishable public observations require different evidence. The canonical evidence map retains exactly the distinctions required by the contract. If the interface loses even one, no evidence encoding satisfying that contract permits exact recovery from the same observation. Value agreement is a separate obligation. Standard Event-B obligations can all hold while reachable cases violate BEP. The workflow follows one imported train model through a branch addition: it detects a stale declaration, reuses the abstract evidence proof, constructs the local decoder, and checks the repaired response against model executions. Lean checks the generic implications and finite translation; Rodin proves the generated obligations. ProB and executed AI cases supply collisions, repairs, and rejected false attributions. For finite cases, a tagger that can inspect the completed case and its public observation needs as many tag values as the largest number of required evidence values hidden by one observation. Tags fixed from an earlier, restricted context correspond to proper colorings of a conflict graph. The alphabet gap is unbounded, and the explicit finite-table early-assignment problem is NP-complete.