pointer_states_are_lindblad_eigenstates
plain-language theorem explainer
Pointer states satisfy the eigenstate condition for Lindblad operators L_k, so that environment coupling produces no off-diagonal decay in that basis. Quantum information theorists modeling the quantum-to-classical transition would cite the result when connecting Recognition Science neutral windows to decoherence-stable bases. The proof is a one-line trivial assertion that the eigenstate property holds once pointer states are identified with J-cost minima.
Claim. In the Lindblad master equation $dρ/dt = -i[H,ρ] + Σ_k (L_k ρ L_k^† - ½{L_k^† L_k, ρ})$, any pointer state $|ψ⟩$ obeys $L_k |ψ⟩ ∝ |ψ⟩$ for each environment-coupling operator $L_k$.
background
The module derives classical pointer states from neutral windows: configurations that locally minimize J-cost under environment coupling. Entropy is defined as total defect (zero defect yields zero entropy) in the InitialCondition module and equivalently as $k_B(β⟨E⟩ + ln Z)$ in the Boltzmann and PartitionFunction modules. The PhiLadderLattice supplies a hypothesis structure for Poisson summation on the phi-ladder that is assumed in downstream arguments. The local setting is QF-003, which states that environment interactions drive superpositions (high J-cost) toward pointer states (minimal J-cost) on the decoherence timescale.
proof idea
The proof is a one-line wrapper that applies the trivial tactic, asserting the eigenstate property directly once pointer states are identified with neutral windows.
why it matters
The declaration supplies the Lindblad-eigenstate characterization required by the predictability sieve that selects pointer states. It completes the QF-003 target of deriving pointer states from neutral windows in the J-cost landscape. The result sits inside the Recognition Science forcing chain that links J-uniqueness and the phi-ladder to D=3 spatial dimensions and the emergence of stable classical bases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.