pith. machine review for the scientific record. sign in
def definition def or abbrev high

mutualInformationProperties

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 176def mutualInformationProperties : List String := [

proof body

Definition body.

 177  "Shared randomness: Alice and Bob get correlated random bits",
 178  "No channel capacity: Cannot send messages via entanglement alone",
 179  "Classical communication still needed to extract correlation"
 180]
 181
 182/-! ## The Role of Relativity -/
 183
 184/-- Special relativity is preserved:
 185
 186    1. No information travels faster than c
 187    2. The "collapse" is not a physical signal
 188    3. Spacelike separated events have no causal order
 189
 190    In RS: The ledger exists outside of spacetime structure,
 191    but ACCESSING the ledger is constrained by local physics. -/

depends on (12)

Lean names referenced from this declaration's body.