AMPSTrilemma
plain-language theorem explainer
The AMPSTrilemma structure encodes the black hole firewall paradox by packaging four propositions (unitarity of late Hawking radiation, smooth horizon for an infaller, locality of physics, and monogamy of entanglement) together with their mutual inconsistency. Quantum gravity researchers cite this formulation when classifying resolutions such as complementarity or ER=EPR. As a structure definition it simply records the logical trilemma without deriving the contradiction from any deeper axiom or forcing relation.
Claim. The AMPS trilemma consists of the four propositions that late Hawking radiation is pure, an infalling observer encounters a smooth horizon, physics is local outside the horizon, and entanglement is monogamous, together with the assertion that these four propositions cannot hold simultaneously.
background
The module treats the firewall paradox (AMPS 2012) inside Recognition Science, where the ledger is fundamentally non-local. This non-locality permits both unitarity and a smooth horizon because ledger connections span the horizon. The local setting is given by the module documentation: unitarity requires late radiation to purify the state, no-drama requires maximal entanglement with the interior partner, and monogamy forbids a single qubit from being maximally entangled with two distinct systems.
proof idea
This declaration is a structure definition that directly encodes the four physical requirements and their contradiction as fields of a record type. No lemmas are applied and no tactics are used; the incompatibility is stated explicitly as one of the structure fields.
why it matters
The structure sets up the firewall paradox whose resolution via ledger non-locality is proposed in the module and appears among the sibling declarations (ledger_resolves_firewall, er_equals_epr_from_ledger, complementarityPrinciple). It corresponds to the paper proposition on resolving the firewall paradox using RS principles. The declaration touches the open question of which of the five listed resolutions (Firewall, Complementarity, ERisEPR, Fuzzball, RS_Ledger) is realized by the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.