pith. sign in
module module high

IndisputableMonolith.Quantum.Firewall

show as:
view Lean formalization →

The Quantum.Firewall module states the AMPS paradox for black holes past Page time in the Recognition Science setting. Researchers examining black hole information and complementarity would cite it when linking RS to quantum gravity. The module presents the trilemma of unitarity, no-drama, and monogamy without proofs, deferring resolutions to sibling declarations.

claimFor a black hole past Page time, unitarity requires late Hawking radiation maximally entangled with early radiation, no-drama requires maximal entanglement with the interior partner, and monogamy of entanglement forbids one qubit from maximal entanglement with two systems simultaneously, yielding a contradiction.

background

The module sits in the quantum domain and imports the RS time quantum τ₀ = 1 tick from Constants together with cost structures from Cost. It reproduces the standard AMPS argument verbatim in its doc-comment: unitarity demands purification via early-radiation entanglement, no-drama assumes a smooth horizon with partner entanglement, and monogamy of entanglement produces the contradiction.

proof idea

This is a setup module that states the AMPS trilemma; no proofs are present. The argument follows the three listed conditions to a logical contradiction via monogamy, with all formal resolutions located in sibling declarations such as AMPSTrilemma and Resolution.

why it matters in Recognition Science

The module supplies the problem statement addressed by sibling declarations including ledger_resolves_firewall, er_equals_epr_from_ledger, and information_preserved. It positions the firewall issue inside the RS treatment of unitarity and complementarity, feeding the chain that resolves singularities and preserves information.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (13)