module module moderate

`IndisputableMonolith.Quantum.ClassicalEmergence`

The module defines J-cost for product states of N particles and related quantum cost structures in Recognition Science. Researchers analyzing the quantum-to-classical transition would cite it when modeling emergence via cost minimization. It consists of definitions and lemmas built on the Constants and Cost modules.

claimJ-cost for product state of $N$ particles: $J(ψ_1 ⊗ ⋯ ⊗ ψ_N)$, together with $J$-cost for entangled states, pointer states, and decoherence time.

background

The module sits in the Quantum domain and imports the RS time quantum τ₀ = 1 tick from Constants together with cost functions from the Cost module. It introduces definitions for product-state J-cost, entangled J-cost, PointerState, positionPointer, momentumPointer, einselection_from_jcost, and QuantumClassicalCrossover. The local setting is that classical behavior arises when J-cost is minimized under coarse-graining.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds IndisputableMonolith.Quantum.QMInterpretationStructure, whose content states that classical description emerges as a J-cost minimum. It supplies the quantum-side definitions required for that interpretation.

scope and limits

Does not derive quantum postulates from the T0-T8 forcing chain.
Does not compute explicit numerical decoherence times.
Does not treat relativistic or gravitational corrections to the crossover.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Quantum.QMInterpretationStructure module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (21)

def jcostProduct L48
def jcostEntangled L53
theorem entangled_higher_cost L57
theorem cost_difference_scales_quadratically L71
structure PointerState L80
def positionPointer L88
def momentumPointer L94
theorem einselection_from_jcost L101
def decoherenceTime L113
theorem macro_decohere_instant L117
structure QuantumClassicalCrossover L127
theorem classical_from_coarse_graining L146
theorem classical_as_jcost_minimum L155
theorem classical_limit_is_continuum L162
structure NewtonianParticle L170
theorem newton_from_jcost L180
theorem ehrenfest_theorem L189
def predictions L200
def experiments L211
structure EmergenceFalsifier L225
def experimentalStatus L232