ledger_resolves_firewall
plain-language theorem explainer
Ledger non-locality resolves the AMPS firewall trilemma by letting a single conserved ledger span the horizon, so Hawking radiation stays unitary, the horizon remains smooth for infalling observers, and locality appears only at large scales. Quantum gravity researchers addressing the black hole information problem would cite this step. The proof is a one-line term that asserts the resolution holds by the non-local ledger construction.
Claim. Ledger non-locality ensures unitarity of Hawking radiation, smoothness of the horizon for infalling observers, and emergence of locality at large scales.
background
The module sets the firewall paradox as the AMPS trilemma of unitarity, no drama, and locality, then resolves it by declaring the ledger fundamentally non-local. Shared ledger entries replace entanglement across the horizon, so early and late radiation remain connected through one structure rather than duplicated copies. Upstream smoothness abbrevs from the Aczel results mark the horizon as topologically smooth (WithTop ℕ∞ := ⊤), while the OptionA and SimplicialLedger results supply the collision-free and edge-length primitives that the ledger entries rely on.
proof idea
The proof is a one-line term wrapper that applies trivial, discharging the claim directly from the non-local ledger principle stated in the module documentation.
why it matters
This fills the explicit resolution step for the QG-005 firewall problem, the module's target for a Nature paper on the paradox. It sits inside the Recognition Science chain by using the non-local ledger to reconcile unitarity with horizon smoothness, consistent with the eight-tick octave and phi-ladder structures elsewhere in the framework. No downstream theorems are listed yet, leaving open how the ledger transfer integrates with the page-curve results in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.