complementarityPrinciple
plain-language theorem explainer
The declaration defines the complementarity principle as the statement that no single observer experiences both the exterior and infalling descriptions of a black hole horizon. Quantum gravity researchers addressing the AMPS firewall paradox would cite it as the Recognition Science resolution via non-local ledger mediation. The definition is a direct string assignment with no computational reduction or tactic steps.
Claim. In the Recognition Science ledger framework, the complementarity principle states that no single observer experiences both the exterior description (particle never crosses the horizon) and the infalling description (smooth horizon crossing).
background
The module addresses the firewall paradox (AMPS 2012) as a trilemma among unitarity of Hawking radiation, smooth horizon for infalling observers, and locality outside the horizon. Recognition Science resolves it by making the ledger fundamentally non-local, so that ledger connections span the horizon and support both descriptions simultaneously. The supplied doc-comment states: 'Different observers, different slicings: Outside observer: Never sees particle cross horizon; Infalling observer: Smoothly crosses horizon; Both descriptions are valid (complementarity). In RS: The ledger supports BOTH descriptions!' Upstream results supply supporting structures such as vantage projection (Vantage.get) and ledger edge definitions, but the declaration itself is a pure string constant.
proof idea
The declaration is a one-line definition that directly assigns the string value 'No single observer experiences both descriptions'. No lemmas are applied and no tactics are used.
why it matters
It supplies the explicit statement of complementarity that the module uses to close the firewall trilemma, allowing unitarity and no-drama to coexist because the ledger is non-local. The module doc positions this as the core of a potential Nature paper on firewall resolution. It sits alongside sibling declarations such as ledger_resolves_firewall and er_equals_epr_from_ledger, completing the RS account of horizon smoothness without invoking drama. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.