complementarityPrinciple
plain-language theorem explainer
The declaration defines the complementarity principle as the assertion that no single observer experiences both horizon descriptions. Physicists resolving the AMPS firewall paradox would cite it when reconciling unitarity with smooth horizons inside Recognition Science. The definition is realized as a direct string assignment.
Claim. Different observers experience distinct horizon slicings: an outside observer never sees a particle cross the horizon while an infalling observer crosses smoothly, with both descriptions valid under the ledger.
background
The module addresses the firewall paradox (AMPS 2012) as a trilemma among unitarity, no drama at the horizon, and locality. Recognition Science resolves it by making the ledger non-local, so that ledger connections span the horizon and support both an outside description (no crossing) and an infalling description (smooth crossing). The supplied doc-comment states the key point: different observers use different slicings, yet the ledger sustains both.
proof idea
The declaration is a direct string literal assignment with no lemmas or tactics applied.
why it matters
This definition supplies the verbal anchor for the RS resolution of the firewall paradox inside the Quantum.Firewall module. It feeds the claim that the ledger mediates information transfer while preserving both unitarity and horizon smoothness, aligning with the Nature paper proposition mentioned in the module documentation. It touches the open question of how ledger non-locality quantitatively replaces locality without violating the eight-tick octave or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.