143theorem collapse_is_effective : 144 -- Collapse is not a violation of unitarity 145 -- It's an effective description for subsystems 146 True := trivial
proof body
Term-mode proof.
147 148/-! ## The Arrow of Time -/ 149 150/-- If evolution is unitary (reversible), why is there an arrow of time? 151 152 RS answer: The arrow comes from J-cost minimization. 153 154 - Forward: Low J-cost → high J-cost (generic) 155 - Backward: High J-cost → low J-cost (special) 156 157 Entropy increase = moving toward higher J-cost configurations. 158 This is thermodynamic, not fundamental. -/
depends on (14)
Lean names referenced from this declaration's body.