EntanglementEntropyCert
plain-language theorem explainer
EntanglementEntropyCert collects the four properties needed to certify that J-cost reproduces entanglement entropy in the recognition framework: exactly five structure types, vanishing cost for unentangled states, positive cost for entangled ratios, and positive value for the maximal log. Researchers modeling quantum information via recognition science would reference this certificate to anchor their calculations in the five-structure taxonomy. The declaration is a structure definition that directly bundles these four conditions without further
Claim. A certificate structure asserting that the set of entanglement structures has cardinality 5, that the J-cost of ratio 1 equals zero, that the J-cost is strictly positive for all positive ratios other than 1, and that the maximal entanglement logarithm is positive.
background
The module develops entanglement entropy from the J-cost in recognition science, where S equals the J-cost of the reduced density matrix for a bipartite system. EntanglementStructure is the inductive type enumerating the five canonical cases: product, separable, entangled, maximallyEntangled, and clusterState. maximalEntanglementLog is defined as 3 times the natural logarithm of 2, matching log(2^D) for D=3. The J-cost function, imported from the Cost module, satisfies J(1) = 0 and is positive for other positive arguments, consistent with the recognition composition law.
proof idea
The declaration is a structure definition that requires the four fields to be supplied by sibling results: the cardinality count from entanglementStructureCount, the zero cost from unentangled_zero_cost, the positivity from entangled_positive_cost, and the sign from maximalEntanglement_pos.
why it matters
This structure is instantiated by entanglementEntropyCert to produce a concrete witness for the RS account of entanglement entropy. It encodes the prediction that five structures arise at D=3 and that maximal entanglement yields a positive logarithm, aligning with the eight-tick octave and spatial dimension forcing in the unified chain. The construction closes the certification loop for the module's claim that entanglement entropy equals J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.