entanglementEntropyCert
plain-language theorem explainer
This definition assembles the EntanglementEntropyCert structure that certifies the Recognition Science identification of entanglement entropy with J-cost. It records that exactly five entanglement structures exist, that J vanishes on the unentangled state, is strictly positive on entangled states, and that the maximal-entanglement logarithm is positive. A physicist deriving QFT entanglement measures from the RS forcing chain would cite the certificate to anchor the formula S = J(ρ_A). The construction is a direct record instantiation that wires
Claim. The certificate EntanglementEntropyCert is the structure whose fields are set to: the cardinality of the type of entanglement structures equals 5, J-cost of the unit element equals 0, J-cost of any positive real not equal to 1 is positive, and the logarithm of maximal entanglement is positive.
background
In the Recognition Science treatment of entanglement entropy the von Neumann entropy S = -Tr(ρ log ρ) for a bipartite system is identified with the J-cost J(ρ_A) that quantifies off-equilibrium deviation between subsystems. The module works in the setting where five canonical structures (product, separable, entangled, maximally entangled, cluster state) match the configuration dimension at spatial dimension D = 3, and where maximal entanglement yields S = log(2^D) = D log 2. Upstream results supply the supporting facts: entanglementStructureCount proves the cardinality equals 5 by decision, unentangled_zero_cost proves Jcost 1 = 0 from the unit property of J, entangled_positive_cost proves Jcost r > 0 whenever r > 0 and r ≠ 1, and maximalEntanglement_pos proves the logarithm is positive by direct multiplication and logarithm positivity.
proof idea
The definition constructs the EntanglementEntropyCert record by direct field assignment: five_structures receives the value of entanglementStructureCount, unentangled receives unentangled_zero_cost, entangled_cost receives entangled_positive_cost, and max_entanglement_pos receives maximalEntanglement_pos. This is a one-line wrapper that packages the four supporting theorems into the required structure.
why it matters
This definition supplies the complete certificate required by the RS derivation of entanglement entropy from J-cost, closing the module with zero sorry statements. It directly implements the prediction that entanglement entropy scales with rung index times log φ and that five structures arise at D = 3. The certificate stands ready for use in higher-level statements linking RS to QFT entanglement measures, though no downstream theorems yet reference it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.