EntanglementStructure
plain-language theorem explainer
EntanglementStructure enumerates the five canonical bipartite configurations in the Recognition Science model of entanglement entropy. Researchers deriving S = J(ρ_A) from the J-cost functional cite it to classify states before applying cost relations or the Recognition Composition Law. The declaration is a direct inductive enumeration that derives Fintype automatically, enabling the immediate cardinality result that follows.
Claim. The set of entanglement structures consists of five elements: the product configuration, the separable configuration, the entangled configuration, the maximally entangled configuration, and the cluster state configuration.
background
In the Recognition Science treatment of entanglement entropy, S equals the J-cost of the reduced density matrix ρ_A for a bipartite system. J-cost is the functional J(x) = (x + x^{-1})/2 - 1 that quantifies deviation from equilibrium; it vanishes at x = 1 (unentangled product states) and is positive otherwise. The module works at D = 3, where the maximally entangled case yields S = log(8), and posits exactly five canonical structures whose count matches configDim D = 5.
proof idea
The declaration is the inductive definition that lists the five constructors and derives DecidableEq, Repr, BEq, and Fintype in one step. No tactics or lemmas are applied; the Fintype instance is generated automatically by the deriving clause.
why it matters
This definition supplies the finite classification that EntanglementEntropyCert relies on to certify the J-cost properties (zero for unentangled, positive otherwise, and positive maximal entanglement log). It realizes the module's claim that five structures appear at D = 3 and directly supports the downstream cardinality theorem. The construction closes the enumeration step needed before any quantitative entropy calculation from the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.