unentangled_zero_cost
plain-language theorem explainer
The result establishes that the recognition cost vanishes at the unit element, corresponding to unentangled product states having zero entanglement entropy. Quantum information researchers building measures from the Recognition Science cost function would cite this as the base case for product states. The proof is a direct term application of the unit lemma for the cost definition.
Claim. The recognition cost function satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$.
background
The module derives entanglement entropy from the J-cost by setting $S = J(ρ_A)$ for bipartite subsystems in the recognition basis. The cost function is defined as $J(x) = (x-1)^2/(2x)$, which is zero precisely at equilibrium. Upstream results include the equilibrium theorem stating $J = 0$ at the unit element and the Jcost_unit0 lemma proved by simplification on the definition.
proof idea
The proof is a one-line term wrapper that applies the Jcost_unit0 lemma from the Cost module.
why it matters
This supplies the unentangled case inside the EntanglementEntropyCert definition, which bundles the five structures with their respective costs. It anchors the RS prediction that product states carry zero entanglement entropy, consistent with the J-uniqueness property and the composition law. The result closes the zero-cost base in the chain leading to maximal entanglement at $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.