pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Quantum.Firewall

show as:
view Lean formalization →

Quantum.Firewall formalizes the AMPS paradox for old black holes in Recognition Science. It encodes the conflict where unitarity requires late radiation to entangle with early radiation for purification, no-drama requires entanglement with the interior partner, and monogamy forbids both. Physicists examining black hole information cite this module before turning to ledger resolutions. The module organizes the trilemma through definitions rather than executing a single proof.

claimFor a black hole past Page time the AMPS trilemma asserts that unitarity (late radiation maximally entangled with early radiation) together with no-drama (late radiation maximally entangled with its interior partner) and locality violate monogamy of entanglement, yielding a contradiction.

background

The module sits in the quantum domain of Recognition Science and imports the fundamental time quantum τ₀ = 1 tick from Constants together with cost accounting from Cost. It adopts the standard black-hole evaporation setting in which an old black hole has passed Page time, so that the emitted radiation must purify the state. The supplied doc-comment states the three horns explicitly: unitarity demands maximal entanglement with early radiation, no drama demands maximal entanglement with the partner mode behind the horizon, and monogamy of entanglement prohibits a single qubit from satisfying both.

proof idea

This is a definition module with no proofs. It introduces AMPSTrilemma and Resolution as organizing objects, then lists concrete resolution paths such as ledger_resolves_firewall, er_equals_epr_from_ledger, and information_preserved without applying any lemmas or tactics.

why it matters in Recognition Science

The module supplies the AMPS paradox setup that the sibling resolutions (ledger_resolves_firewall, er_equals_epr_from_ledger, singularity_resolved) discharge. It marks the point where Recognition Science confronts the firewall issue inside the broader forcing chain, linking quantum information preservation to the ledger transfer mechanism.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)