11 Endpoint, audit, and discovery equivalence
On this page · Permalink · Source line 1446
The phrase “the same proof” can refer to several distinct equivalence relations.
Definition 11.1: Endpoint equivalence
Fix a background theory, an interpretation of claim labels, and an admissible inference policy. Within that context, two representations are endpoint equivalent when they certify the same judgment from the same complete assumption context and requested targets. Required premises and any additional admitted assumptions are accounted for in that context. A comparison across different contexts requires an explicitly specified transport of assumptions and judgments, not merely identical displayed labels.
Definition 11.2: Audit equivalence
Two representations are audit equivalent when they preserve equivalent dependency, evidence, provenance, and scope information for checking the declared targets.
Definition 11.3: Discovery equivalence
Two representations are discovery equivalent relative to a declared bridge model when they preserve the same examples, alternatives, boundary cases, candidate routes, and future reach, up to the chosen graph equivalence.
When audit and discovery task families are required to include the endpoint tasks, either equivalence implies endpoint equivalence. Audit and discovery equivalence need not imply one another: a representation may preserve provenance without alternatives, or alternatives without provenance. Their joint task family is stronger than either. Any further hierarchy requires an explicit inclusion of task families. Two perfectly valid certificates can therefore expose different mathematical neighborhoods without differing in validity.
Remark 11.4
These equivalences are task-relative. Discovery equivalence requires a declared bridge model. It is not an assertion that every future use of a proof can be predicted.