AMPSTrilemma
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the contradiction from the Recognition Composition Law or the forcing chain T0-T8.
- Does not compute explicit entanglement entropies or Page curves.
- Does not select among the five proposed resolutions.
- Does not address higher-dimensional or charged black-hole generalizations.
formal statement (Lean)
57structure AMPSTrilemma where
58 unitarity : Prop -- Hawking radiation is pure
59 no_drama : Prop -- Smooth horizon for infaller
60 locality : Prop -- Physics is local
61 monogamy : Prop -- Entanglement is monogamous
62 contradiction : unitarity ∧ no_drama ∧ locality ∧ monogamy → False
63
64/-! ## Proposed Resolutions -/
65
66/-- Various proposals to resolve the firewall:
67
68 1. **Firewall exists**: Give up "no drama" (AMPS)
69 2. **Complementarity**: Give up locality (Susskind)
70 3. **ER = EPR**: Wormholes connect entangled pairs (Maldacena-Susskind)
71 4. **Fuzzball**: No interior at all (Mathur)
72 5. **RS Resolution**: Ledger non-locality resolves all
73
74 Each has strengths and weaknesses. -/