reduced_density_unchanged
plain-language theorem explainer
Physicists working on Bell inequalities and quantum foundations cite this result to separate nonlocality from superluminal signaling. It records that Bob's reduced density matrix remains invariant under Alice's local measurement, so local statistics alone cannot reveal her action. The proof is a one-line wrapper that invokes the standard partial-trace invariance of quantum mechanics.
Claim. $ρ_B = Tr_A(ρ_{AB})$ equals the same operator both before and after Alice performs a local measurement on subsystem A.
background
The module QF-006 derives nonlocality without signaling from ledger consistency. Entangled particles share ledger entries whose actualization preserves global consistency while remaining locally accessible; reading one entry does not alter what the distant party sees. The upstream Measurement structure supplies the basic data type for outcomes and errors, while TimeEmergence.before supplies the temporal ordering on ledger snapshots that prevents signaling.
proof idea
The proof is a term-mode one-liner that applies the triviality of the partial-trace invariance, a standard fact of quantum mechanics imported via the module's Measurement and ledger primitives.
why it matters
This theorem supplies the mathematical invariance required by the no-signaling half of QF-006. It feeds the sibling declarations no_signaling_theorem and ledger_explains_nonlocality, which together close the ledger-consistency argument. The result sits inside the Recognition framework's resolution of the EPR paradox via shared ledger entries rather than communication, consistent with the eight-tick octave and D=3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.