information_conserved_implies_no_distinct_zero_defect
plain-language theorem explainer
The theorem shows that ledger conservation implies at most one positive real with vanishing defect. Researchers addressing the black hole information paradox cite it to rule out distinct zero-cost states that could absorb information. The proof extracts the unique minimizer from the conservative hypothesis and derives a contradiction from any assumed pair of distinct zero-defect points.
Claim. If the ledger is conservative, meaning there exists a unique positive real $x_0$ such that the defect of $x_0$ is zero, then there do not exist distinct positive reals $x$ and $y$ both having zero defect.
background
The defect functional equals the cost function J on positive reals, with defect at unity equal to zero. The hypothesis ledger_conservative asserts existence of a unique positive minimizer: there is exactly one positive real whose defect vanishes. This module formalizes BH-002, the black hole information paradox resolution, by treating the ledger as a complete conservative substrate in which information is reorganized rather than destroyed.
proof idea
The proof destructures the ledger_conservative hypothesis to obtain the unique zero-defect point x0 and its uniqueness property. It then assumes two distinct positive x and y with zero defect, applies uniqueness to show both equal x0, and obtains the contradiction that x equals y.
why it matters
The result closes one structural route to information loss in the BH-002 ledger argument. It relies on the uniqueness clause inside ledger_conservative and supports the claim that information is redistributed rather than erased when matter enters a black-hole region. In the Recognition framework it reinforces conservation under the phi-ladder and eight-tick structure, while the full gravity-from-ledger derivation remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.