entangled_positive_cost
plain-language theorem explainer
Entangled states carry strictly positive J-cost for any positive real ratio parameter not equal to one. Researchers deriving entanglement entropy from the recognition basis would cite this to confirm that off-equilibrium configurations incur positive recognition cost. The argument is a direct term application of the general positivity lemma for the J-cost function.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
The module equates entanglement entropy $S = -Tr(ρ log ρ)$ with the J-cost of the reduced density matrix in the recognition basis. Product states map to $J(1) = 0$ while entangled states map to $J(r) > 0$ for $r ≠ 1$. The J-cost is the off-equilibrium cost obeying the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ and the explicit form $J(x) = (x + x^{-1})/2 - 1$.
proof idea
The declaration is a one-line term wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module, supplying the hypotheses $0 < r$ and $r ≠ 1$ directly.
why it matters
This result supplies the entangled_cost field inside the EntanglementEntropyCert definition that assembles the five canonical entanglement structures. It supports the RS identification of entanglement entropy with off-equilibrium J-cost, consistent with T5 J-uniqueness and the prediction that entanglement at rung k scales with k log φ. It closes the positivity requirement for the entanglement construction without addressing dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.