qm_interpretation_from_ledger
plain-language theorem explainer
The definition asserts that the Recognition Science quantum interpretation requires entangled states of N particles to incur strictly higher J-cost than product states for every N exceeding 1. Researchers deriving classical emergence from ledger-based recognition would cite this as the minimal content of the QM interpretation. It is realized as a direct universal quantification comparing the two J-cost functions imported from the ClassicalEmergence module.
Claim. For every natural number $N>1$, the J-cost of the fully entangled state of $N$ particles exceeds the J-cost of the product state: $N + N(N-1)/2 > N$.
background
In Recognition Science, J-cost quantifies recognition effort for a state. The upstream jcostProduct returns N times the single-particle cost for a separable product state. The upstream jcostEntangled augments this by the quadratic cross-term alpha * N*(N-1)/2, as its doc-comment states that entanglement adds cross-terms scaling quadratically.
proof idea
The definition directly encodes the proposition as a forall statement over natural numbers N. It applies the two J-cost functions from the ClassicalEmergence module and asserts the strict inequality for all N > 1. No additional lemmas or tactics are used; the body is the quantified expression itself.
why it matters
This definition supplies the core proposition for the QM interpretation in the Recognition Science framework. It is invoked by the downstream theorem qm_interpretation_structure to establish the interpretation and by qm_interpretation_implies_cost_gap to extract the cost gap. The doc-comment positions it as realizing classical emergence through J-cost minimization, consistent with the forcing chain where J-uniqueness selects low-cost configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.