entangled_higher_cost
plain-language theorem explainer
Entangled states of N>1 particles incur strictly higher J-cost than product states when the entanglement parameter α exceeds zero. Researchers modeling decoherence or the quantum-to-classical transition cite this to show why macroscopic superpositions are suppressed by cost. The argument unfolds the two cost expressions, reduces the difference to the quadratic cross term, and closes via positivity and linarith.
Claim. For natural number $N>1$ and real parameter $α>0$, the entangled J-cost exceeds the product J-cost: $N j_0 + α N(N-1)/2 > N j_0$, where $j_0$ denotes the single-particle J-cost.
background
In the Recognition Science setting of QF-011, classical emergence arises because many-body J-cost penalizes entanglement. The product-state cost is defined as $N$ times the single-particle value. The entangled-state cost augments this by the pairwise cross term $α N(N-1)/2$, with $α$ measuring correlation strength. These definitions rest on the upstream cost function that assigns J-cost to any recognition event via the multiplicative recognizer comparator.
proof idea
Unfold both cost definitions to obtain the difference $α N(N-1)/2$. Establish positivity of $N$ and $N-1$ via Nat.cast_pos and a short omega-linarith block. Apply the positivity tactic to the product with $α>0$. Finish with linarith to obtain the strict inequality.
why it matters
The inequality is invoked directly inside qm_interpretation_structure to embed the QM interpretation inside the ledger. It supplies the central step of the module's classical-emergence argument: for large $N$ the quadratic penalty forces the system onto product states. The construction is consistent with the Recognition Composition Law, which makes cross terms costly and thereby selects the classical basis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.