Formal Foundations for the Single Source of Truth Principle

Any system encoding facts faces a fundamental constraint: when multiple independent locations encode the same fact, truth becomes indeterminate. We prove that DOF = 1 (Single Source of Truth) is the unique representation guaranteeing coherence, the impossibility of disagreement among encodings. The Core Theorem (Oracle Arbitrariness). In any incoherent encoding system (DOF > 1 with divergent values), no resolution is principled: for ANY oracle claiming to identify the "true" value, there exists an equally-present value that disagrees. This is not about inconvenience. It is about the determinacy of truth. Programming languages instantiate this epistemic structure: encoding systems become codebases, facts become structural specifications (class existence, method signatures), coherence becomes consistency across encoding locations, and DOF = 1 becomes the Single Source of Truth (DRY principle). Encoding systems -> Codebases Facts -> Structural specifications (class existence, method signatures) Coherence -> Consistency across encoding locations DOF = 1 -> Single Source of Truth (DRY principle) We prove that achieving DOF = 1 for structural facts requires specific language features: definition-time hooks AND introspectable derivation. Most mainstream languages (Java, C++, Rust, Go, TypeScript, etc.) lack these features and cannot achieve coherence for structural facts regardless of programmer effort. Four Theorems: Coherence Forcing: DOF = 1 is the unique value guaranteeing coherence. DOF = 0 means the fact is unrepresented; DOF > 1 permits incoherent states. Oracle Arbitrariness: Under incoherence, any resolution is arbitrary, no oracle is justified by the encodings alone. Language Requirements: For structural facts in software, DOF = 1 requires definition-time hooks AND introspection. These are logically forced. Strict Dominance: The coherence restoration complexity gap is unbounded: O(1) vs O(n). Theoretical Foundation. The derivation theory (independence, derivability, axis collapse) is established in previous work (https://zenodo.org/records/18123532). This paper proves the coherence consequences and instantiates them to programming languages. All theorems machine-checked in Lean 4 (9,351 lines, 541 theorems, zero sorry). Language capability claims derived from formalized operational semantics, not declared as flags. Practical demonstration via OpenHCS PR #44: migration from 47 scattered checks to 1 ABC (DOF 47 -> 1).