pith. sign in
theorem

cost_difference_scales_quadratically

proved
show as:
module
IndisputableMonolith.Quantum.ClassicalEmergence
domain
Quantum
line
71 · github
papers citing
none yet

plain-language theorem explainer

The difference between the J-cost of an entangled N-particle state and its product-state counterpart equals α N (N-1)/2. Researchers modeling decoherence via Recognition Science's J-cost framework would cite this identity to show why entangled states become costly for macroscopic N. The proof proceeds by direct substitution of the two explicit cost definitions followed by algebraic simplification.

Claim. Let $J_ {ent}(N, j_{single}, α)$ be the J-cost of a fully entangled state of $N$ particles and $J_{prod}(N, j_{single})$ the J-cost of the corresponding product state. Then $J_{ent}(N, j_{single}, α) - J_{prod}(N, j_{single}) = α N (N-1)/2$.

background

In the module on classical emergence from many-body J-cost, product states have J-cost linear in particle number N while entangled states acquire quadratic cross terms. The J-cost function itself is the derived cost induced by a multiplicative recognizer, measuring the recognition cost of a state. Upstream results supply the explicit forms: jcostProduct sums single-particle contributions while jcostEntangled adds the entanglement penalty α N(N-1)/2. The module states that for large N product states win, driving classical behavior.

proof idea

The proof unfolds the definitions of jcostEntangled and jcostProduct, then applies the ring tactic to perform the algebraic cancellation, yielding the quadratic term directly.

why it matters

This identity supports the core claim of the module that classical behavior emerges because entangled states incur quadratically higher J-cost. It fills the step showing the N² scaling in the many-body J-cost minimization argument. The result aligns with the Recognition Science mechanism where for large N product states minimize total cost, leading to decoherence into pointer states.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.