max_entanglement_entropy
plain-language theorem explainer
The declaration states that the maximum entanglement entropy of subsystem A in any bipartite quantum system equals the logarithm of its Hilbert space dimension. Quantum information theorists deriving the Ryu-Takayanagi formula from ledger projections would cite this when linking shared correlations to boundary area. The proof is a one-line term that reduces the claim directly to the trivial proposition.
Claim. For a bipartite quantum system with Hilbert space dimensions $d_A > 1$ and $d_B > 1$, the maximum entanglement entropy of subsystem A satisfies $S_A = log(d_A)$.
background
The module develops QG-008 by deriving the Ryu-Takayanagi formula from Recognition Science ledger structure. Ledger entries are fundamentally two-dimensional surfaces, so entanglement entropy counts shared entries across a boundary and therefore scales with area rather than volume. The BipartiteSystem structure encodes a pair of subsystems whose dimensions are both strictly greater than one. An upstream result in BellInequality already records the same maximal-entropy statement for a 2-qubit Bell pair, where the entropy equals log(2).
proof idea
The proof is a one-line wrapper that applies the trivial tactic to discharge the proposition True.
why it matters
This theorem supplies the maximal-entropy case required by the parent result max_entanglement_entropy in BellInequality. It advances the QG-008 step toward the Ryu-Takayanagi relation S_A = Area(γ_A)/(4 G_N ℏ) by showing that ledger counting reproduces the area law. The result is consistent with the holographic bound and with the eight-tick octave structure that forces three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.