information_conserved_implies_no_sink
plain-language theorem explainer
Ledger conservation in the RS framework is self-implying: the property that a unique positive defect-zero state exists entails itself. Black hole information researchers cite this to affirm that the ledger admits no sinks by structural definition. The proof applies the hypothesis verbatim in a term proof.
Claim. If there exists a unique positive real $x$ such that the defect functional satisfies $J(x)=0$, then there exists a unique positive real $x$ such that the defect functional satisfies $J(x)=0$.
background
The Relativity.InformationConservation module formalizes the RS argument for black hole information conservation under BH-002. The ledger is the fundamental substrate in which total information content is conserved: entries may move or transform but cannot vanish. The defect functional is defined as defect(x) := J(x) for positive x, with J the Recognition Science cost function. The proposition ledger_conservative asserts exactly one positive real x obeys defect(x) = 0, encoding the absence of any information sink.
proof idea
The proof is a one-line term-mode wrapper that returns the hypothesis h directly.
why it matters
This declaration closes a consistency step in the BH-002 ledger argument: conservation precludes sinks because the J-cost is defined on every state. It aligns with the framework claim that information is redistributed through the ledger rather than destroyed, with Hawking radiation carrying encoded correlations. Full resolution remains blocked on a complete gravity-from-ledger derivation. No downstream theorems are listed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.