BipartiteSystem
plain-language theorem explainer
BipartiteSystem supplies the input type for entanglement entropy calculations by declaring a pair of Hilbert spaces whose dimensions both exceed one. Quantum information researchers deriving the Ryu-Takayanagi formula from ledger projections would cite this structure when formalizing bipartite entanglement in Recognition Science. The declaration is a direct structure with four fields that enforce non-trivial subsystem sizes.
Claim. A bipartite quantum system consists of two Hilbert spaces with dimensions $d_A > 1$ and $d_B > 1$.
background
The module QG-008 derives the Ryu-Takayanagi formula S_A = Area(γ_A)/(4 G_N ℏ) from Recognition Science ledger projections, where ledger entries are fundamentally two-dimensional and entanglement counts shared entries across a boundary. Upstream results supply the entropy definition as total defect (InitialCondition.entropy), the J-cost calibration (PhiForcingDerived.of and DAlembert.LedgerFactorization.of), and the active edge count A (IntegrationGap.A). The structure therefore sits inside the discrete phi-ladder and defect-counting framework that already forces D=3 and the eight-tick octave.
proof idea
The declaration is a structure definition that introduces four fields: natural-number dimensions dim_A and dim_B together with the two positivity hypotheses dim_A_pos and dim_B_pos. No lemmas or tactics are invoked; the object is introduced solely to serve as the domain type for the downstream entanglementEntropy function and its non-negativity and maximality theorems.
why it matters
BipartiteSystem supplies the typed domain for entanglementEntropy, entanglement_entropy_nonneg, and max_entanglement_entropy, thereby advancing the QG-008 target of obtaining the area law from shared ledger entries. It anchors the holographic bound in the same 2D ledger structure that already produces the phi-ladder mass formula and the alpha band. The structure closes one scaffolding step toward a fully ledger-derived Ryu-Takayanagi relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.