Empty Ledger Conservation
Abstract
Complete detection discipline makes an empty open ledger exclude detectable residuals.
Theorem 1.1 (An empty open ledger excludes detectable residuals).
Proof. Machine-checked in Lean as D5/S0/History/EmptyLedgerConservation.empty_ledger_excludes_detectable_residual (✓ std3). ∎
Source. Repository-derived.
Commentary.
Detection discipline requires every residual that can be detected at an object to occur in that object’s open ledger. If the open ledger is empty, a detectable residual would therefore supply an element of the empty set, which is impossible. The conclusion is conditional on the discipline hypothesis; it does not claim that all residuals are detectable or that detection is decidable.
The library search found the exact set-theoretic core in pinned Mathlib as Set.eq_empty_iff_forall_notMem. The formal theorem is a thin honest wrapper: that equivalence converts the empty-ledger hypothesis into pointwise non-membership, while discipline turns a hypothetical detectable residual into the forbidden membership. No separate ledger implementation or detection algorithm is introduced.
References
- Truth anchor:
D5/S0/History/EmptyLedgerConservation.empty_ledger_excludes_detectable_residual