jcostProduct
plain-language theorem explainer
The definition supplies the total J-cost of an uncorrelated product state of N particles as exactly N times the single-particle J-cost. Workers on decoherence and pointer-state selection cite it when they compare additive versus quadratic many-body costs. The definition is a direct one-line scaling that inherits additivity from the underlying J-cost on independent recognition events.
Claim. For a product state of $N$ particles each carrying single-particle J-cost $j$, the total J-cost equals $N j$.
background
In the QF-011 setting, classical behavior emerges once many-body states are ranked by total J-cost; product states minimize this cost while entangled states do not. The single-particle J-cost itself is the value returned by the cost function on a RecognitionEvent, which is obtained from the derivedCost of a MultiplicativeRecognizer comparator. Upstream lemmas establish that J-cost is non-negative and additive under independent recognition, consistent with the Recognition Composition Law and the phi-ladder scaling of physical quantities.
proof idea
The definition is a one-line wrapper that multiplies the particle count by the supplied single-particle J-cost.
why it matters
It supplies the baseline subtracted in the cost-difference theorem and the entangled-higher-cost theorem, both of which feed the QM-interpretation structure asserting that classical descriptions arise as J-cost minima. The construction realizes the module's core claim that product states scale linearly while entangled states scale quadratically, thereby selecting classical pointer states for large N. It closes one half of the many-body comparison required by the Recognition Science account of decoherence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.