entanglementStructureCount
plain-language theorem explainer
The Recognition Science framework enumerates exactly five canonical entanglement structures for bipartite systems at D=3. Researchers modeling entanglement entropy via J-cost would cite this count to fix the dimension of the configuration space. The proof is a one-line decision procedure that exhausts the Fintype instance generated by the five constructors of the inductive type.
Claim. The finite set consisting of the five cases product, separable, entangled, maximally entangled, and cluster state has cardinality 5.
background
EntanglementStructure is the inductive type whose five constructors are product, separable, entangled, maximally entangled, and cluster state; it derives Fintype, DecidableEq, Repr, and BEq. The module develops entanglement entropy as the J-cost of the reduced density matrix for bipartite systems, stating that five canonical structures equal configDim at D=3, with maximal entanglement giving S = log(8) and the unentangled case giving S = 0 = J(1). The sole upstream result is the inductive definition itself, which supplies the Fintype instance.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute the cardinality of the Fintype instance generated by the five-constructor inductive type.
why it matters
This theorem supplies the five_structures field to the EntanglementEntropyCert definition, which certifies zero cost for the unentangled case and positive cost for entangled cases. It anchors the configuration dimension at five, consistent with D=3 from forcing-chain step T8 and the eight-tick octave. The result closes the enumeration step in the entanglement-entropy derivation inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.