max_entanglement_entropy
plain-language theorem explainer
The theorem states that the entanglement entropy of a 2-qubit Bell pair equals log(2). Researchers deriving quantum correlations from ledger structure in Recognition Science would cite this result when specializing the general entropy formula to Bell pairs. The proof is a term-mode reflexivity that matches the definition of bellPairEntropy directly to Real.log 2.
Claim. For a 2-qubit Bell pair the von Neumann entropy satisfies $S = log(2)$.
background
The module QF-005 treats entanglement as shared ledger entries between particles created together, which produce non-local correlations while preserving no-signaling. This rests on upstream structures such as LedgerFactorization.of, which equips the positive reals under multiplication with the calibrated J-cost, and IntegrationGap.A, which fixes the active edge count per fundamental tick at 1. PrimitiveDistinction.from supplies the seven-axiom foundation that reduces to four structural conditions plus definitional facts, while PhiForcingDerived.of encodes the J-cost structure used throughout the ledger.
proof idea
The proof is a one-line term-mode reflexivity that equates bellPairEntropy to Real.log 2 by definition.
why it matters
This supplies the concrete Bell-pair case that feeds the general max_entanglement_entropy theorem in the EntanglementEntropy module, which in turn relates to the Ryu-Takayanagi formula. It fills the QF-005 paper proposition on quantum nonlocality from ledger structure and aligns with the framework's shared-ledger account of Bell violation. The result touches the T5 J-uniqueness and T7 eight-tick octave landmarks by grounding maximal entropy in the same ledger factorization used for D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.