mutualInformationProperties
plain-language theorem explainer
mutualInformationProperties enumerates the information-theoretic features of entanglement under Recognition Science ledger consistency: nonzero mutual information between parties yet zero signaling capacity. A quantum foundations researcher would cite it when reconciling Bell violations with no faster-than-light communication. The definition is a direct list construction of three descriptive strings with no lemmas or computation.
Claim. The mutual information properties are: $I(A:B|setting)>0$ (nonzero correlation from shared ledger entries), $I($Alice's choice$:Bob's outcome$)=0$ (no signaling), where entanglement supplies shared randomness but requires a classical channel for correlation extraction.
background
Module Quantum.NonlocalityNoSignaling treats QF-006: nonlocality without signaling from ledger consistency. Entangled particles share ledger entries (nonlocality) while local access to any entry leaves the distant party's view unchanged (no signaling). The ledger maintains global consistency outside spacetime, but reading remains constrained by local physics.
proof idea
This is a direct definition that constructs a List String by enumerating three fixed properties. No lemmas from the depends_on list are applied; the body is a static literal list with no tactics or reductions.
why it matters
The definition supports the module's core claim that ledger consistency yields Bell correlations without communication channels. It clarifies the distinction between shared randomness and signaling, preserving special relativity while allowing nonlocal correlations. No downstream uses are recorded; it serves as documentation for the no-signaling explanation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.