qm_interpretation_structure
plain-language theorem explainer
The result establishes that the QM interpretation structure holds: for every natural number N greater than 1 the entangled J-cost strictly exceeds the product J-cost when both auxiliary parameters equal 1. Researchers deriving classical emergence from quantum states inside the Recognition Science ledger would cite it as the concrete verification of the interpretation Prop. The proof is a one-line wrapper that instantiates the entangled_higher_cost lemma at unit values and discharges the positivity side-condition by norm_num.
Claim. For every natural number $N>1$, the entangled J-cost $jcostEntangled(N,1,1)$ is strictly greater than the product J-cost $jcostProduct(N,1)$.
background
Recognition Science treats the J-cost of a recognition event as the value returned by the cost function on its state; classical descriptions are defined to emerge precisely at minima of this cost. The local module encodes the QM interpretation structure as the proposition that entangled configurations always carry higher J-cost than product configurations for N>1. Upstream, the cost function is the derived cost of a multiplicative recognizer comparator, while entangled_higher_cost supplies the algebraic inequality by expanding both sides and isolating the positive cross term α N (N-1)/2.
proof idea
The proof is a one-line wrapper that applies entangled_higher_cost to the given N and hN, setting both auxiliary parameters to 1 and invoking norm_num to confirm the required positivity hypothesis.
why it matters
The declaration discharges the QM interpretation structure Prop, thereby confirming that classical emergence occurs at J-cost minima inside the quantum ledger. It sits directly beneath the module statement that classical description emerges as a J-cost minimum and supplies the concrete inequality needed for any downstream argument that entangled states are disfavored under the Recognition Composition Law. No open scaffolding remains; the result closes the interpretation interface for the supplied parameter values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.