Empirical/CSD: einselection / pointer-basis selection (Build 15a)

Category: 6-Local (the open-system / decoherence stratum of D1; the first einselection result on the LF6-B decoherence machinery).

Glossary: https://glossary.constraintsurfacedynamics.com/pointer-basis/ Plain-language, CSD-role and formal statements of the pointer basis, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Decoherence (LF6-B.1, LF6/Decoherence.lean) does not merely make the system state mixed: it selects a preferred basis. The reduced state decohereReduced ψ = partialTraceRight (V |ψ⟩⟨ψ| Vᴴ) is diagonal in the measurement (pointer) basis {eⱼ} — its off-diagonal coherences vanish there (decoherence_offdiagonal_vanish) — but its coherences persist in a rotated basis. This basis-selectivity is Zurek's einselection: the "why a preferred basis" content.

The qubit computation (concrete witness)

For N = 2, decohereReduced ψ = diagonal (p₀, p₁) with pⱼ = ‖⟨eⱼ,ψ⟩‖² (= ψⱼ · star ψⱼ, decohereReduced_eq_diagonal). Conjugating by the Hadamard qmH rotates into the {(e₀±e₁)/√2} basis:

qmH · diag(p₀,p₁) · qmH = (1/2) · !![p₀+p₁, p₀−p₁; p₀−p₁, p₀+p₁],

so the rotated-basis off-diagonal entry (0,1) equals (p₀ − p₁)/2. This is nonzero whenever p₀ ≠ p₁ (decohere_hadamard_offDiag + decohere_not_diagonal_in_rotated_basis). The pointer basis {e₀,e₁} is genuinely einselected: it is the one basis in which the decohered state is diagonal.

The p₀ ≠ p₁ hypothesis is load-bearing and honest: at p₀ = p₁ the reduced state is the fully mixed (1/2)·I, which is diagonal in every basis, so there is no preferred basis to select. Einselection is the statement that for a generic superposition (distinct Born weights) the diagonalising basis is unique.

Deliverables

• decohere_hadamard_offDiag — the rotated off-diagonal value (qmH · ρ_red · qmH) 0 1 = (ψ₀·star ψ₀ − ψ₁·star ψ₁)/2, every qubit ψ (computed, not asserted).
• decohere_diagonal_in_pointer_basis — ρ_red is Matrix.diagonal in {eⱼ} (restates decohereReduced_eq_diagonal): the pointer basis is special.
• decohere_not_diagonal_in_rotated_basis (THE einselection witness) — for any qubit with p₀ ≠ p₁, the Hadamard-rotated reduced state has a nonzero (0,1) off-diagonal: coherence persists in the rotated basis.
• einselectionWitness — a concrete superposition (2,1) with p₀ = 4 ≠ 1 = p₁ (non-vacuity), and einselectionWitness_offDiag — its rotated off-diagonal is 3/2 ≠ 0. ⚠️ The witness is deliberately UNNORMALISED (‖ψ‖² = 5), so p₀, p₁ are squared moduli, not probabilities, and decohereReduced has trace 5 rather than 1. That is why an off-diagonal of 3/2 appears, which would be impossible for a trace-one density matrix (|ρ₀₁| ≤ ½). Nothing here depends on normalisation — the claims are "diagonal" versus "off-diagonal ≠ 0" — but the values should not be read as Born probabilities.
• einselection (capstone) — diagonal in the pointer basis (off-diag 0) AND off-diagonal 3/2 ≠ 0 in the Hadamard rotation, for the witness.

Follow-up (#34): the degeneracy boundary + general N

Part A — the degeneracy boundary (qubit). Einselection has a sharp boundary at p₀ = p₁. decohere_hadamard_offDiag_ne_zero_iff makes it crisp: the rotated-basis coherence (p₀ − p₁)/2 is nonzero IFF p₀ ≠ p₁. At the degenerate locus p₀ = p₁ the reduced state is (ψ₀·star ψ₀) • I (decohere_degenerate_scalar), and for unit ψ exactly the maximally mixed (1/2)·I (decohere_degenerate_half, witness degenerateWitness_decohere_half). Being c • I it is invariant under ANY unitary conjugation (decohere_degenerate_basis_invariant), so NO basis is selected: the einselection-FAILS side (einselection_degenerate_boundary).

Part B — general N. The dephasing channel decohereReducedN ρ := diagonal (fun i => ρ i i) zeroes off-diagonal coherences and keeps the diagonal pointer populations for any N (einselectionN); it restricts to the qubit decohereReduced on a pure-state density (decohereReducedN_outerProduct), and genuinely acts (off-diagonal nonzero before, 0 after: decohereReducedN_acts_nontrivial). The degeneracy boundary lifts: equal populations ρ i i = 1/N give (1/N)·I (decohereReducedN_degenerate_scalar, witness decohereReducedN_maximally_mixed), basis-invariant (einselectionN_degenerate).

The pointer basis is the COMPUTATIONAL basis by construction of the dephasing channel; the deeper ontic einselection-from-Σ-dynamics origin stays gated to the entangled tier / D1.

Honest scope and the contrast with #29 (LF4/TypicalityForcing.lean)

Einselection here is the basis selection imposed by the de-isolation / partial-trace in the pointer basis (LF6-B). It contrasts sharply with the typicality layer: fubiniStudy_forced_by_symmetry (#29) shows the Fubini–Study typicality measure is the unique U(N)-invariant probability measure — it is basis-covariant and picks no basis. The preferred basis therefore does not come from the symmetric typicality / sector structure; it comes from the measurement context — which basis the de-isolation couples to and traces in. Einselection is the symmetry-breaking-by-context layered on the symmetric substrate.

This is the QM-validity / open-system reading; the CSD content is the de-isolation reading of which basis is selected. Honest scope: single-system; the pointer basis is the de-isolation's computational basis (the context's choice). Deriving which basis a given physical environment selects (Zurek's predictability-sieve dynamics, a Hamiltonian-level account) is not modelled — here the basis is the de-isolation's by construction, and the theorem is that decoherence is basis-selective (diagonal in exactly one basis up to degeneracy), not that the basis is derived from an environment Hamiltonian. Superseded in part 2026-08-27 (Empirical/CSD/PointerCommutation.lean): the Hamiltonian-level commutation criterion [P, H_int] = 0 is now a theorem — a commuting pointer observable is a constant of the interaction flow, its populations exactly conserved (pointer_basis_of_commuting), while a non-commuting projection is disturbed (einselection_commutation_contrast). Given H_int, the pointer basis is the commutation-selected one; the interaction itself remains an input (the residue).

All exports are foundational-triple-only (off busch_effect_gleason): the result is concrete Matrix arithmetic on Fin 2 over the LF6-B decohereReduced.

The rotated-basis off-diagonal (the core computation)

theorem CSD.Empirical.CSDBridge.Einselection.sqrt_two_inv_sq : (↑√2)⁻¹ * (↑√2)⁻¹ = 1 / 2

((√2)⁻¹)² = 1/2, the Hadamard normalisation squared (cf. qmH_mul_self).

theorem CSD.Empirical.CSDBridge.Einselection.mul_star_normSq (z : ℂ) : z * star z = ↑‖z‖ ^ 2

z · z̄ = (‖z‖ : ℂ)² (the diagonal density entry as the Born weight).

theorem CSD.Empirical.CSDBridge.Einselection.star_ofReal' (r : ℝ) : star ↑r = ↑r

star (↑r) = ↑r for a real scalar embedded in ℂ.

theorem CSD.Empirical.CSDBridge.Einselection.diagonal_const_eq_smul_one {N : ℕ} (c : ℂ) : (Matrix.diagonal fun (x : Fin N) => c) = c • 1

A constant diagonal is a scalar multiple of the identity: diagonal (fun _ => c) = c • 1. The shape of the maximally mixed / degenerate reduced state.

theorem CSD.Empirical.CSDBridge.Einselection.decohere_hadamard_offDiag (ψ : EuclideanSpace ℂ (Fin 2)) : (QM.Gates.qmH * LF6.decohereReduced ψ * QM.Gates.qmH) 0 1 = (ψ.ofLp 0 * star (ψ.ofLp 0) - ψ.ofLp 1 * star (ψ.ofLp 1)) / 2

The Hadamard-rotated off-diagonal of the decohered qubit state. (qmH · decohereReduced ψ · qmH) 0 1 = (ψ₀·star ψ₀ − ψ₁·star ψ₁)/2 = (p₀ − p₁)/2. Computed from decohereReduced_eq_diagonal + concrete Fin 2 matrix arithmetic: qmH = s·!![1,1;1,-1] with s² = 1/2, and !![1,1;1,-1]·diag(p₀,p₁)·!![1,1;1,-1] has (0,1) entry p₀ − p₁.

(1) Diagonal in the pointer basis

theorem CSD.Empirical.CSDBridge.Einselection.decohere_diagonal_in_pointer_basis {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) : LF6.decohereReduced ψ = Matrix.diagonal fun (i : Fin N) => ψ.ofLp i * star (ψ.ofLp i)

The decohered state is diagonal in the pointer basis {eⱼ} (restates decohereReduced_eq_diagonal): decohereReduced ψ = diagonal (j ↦ ψⱼ·star ψⱼ). The off-diagonal coherences vanish (decoherence_offdiagonal_vanish) — the pointer basis is the special, diagonalising basis.

(2) NOT diagonal in the Hadamard-rotated basis (the einselection witness)

theorem CSD.Empirical.CSDBridge.Einselection.decohere_not_diagonal_in_rotated_basis (ψ : EuclideanSpace ℂ (Fin 2)) (hp : ψ.ofLp 0 * star (ψ.ofLp 0) ≠ ψ.ofLp 1 * star (ψ.ofLp 1)) : (QM.Gates.qmH * LF6.decohereReduced ψ * QM.Gates.qmH) 0 1 ≠ 0

THE einselection witness: coherence persists in the rotated basis. For any qubit ψ whose two Born weights differ (p₀ ≠ p₁, i.e. ψ₀·star ψ₀ ≠ ψ₁·star ψ₁), the Hadamard-conjugated reduced state has a nonzero (0,1) off-diagonal (p₀ − p₁)/2. So the decohered state is diagonal in the pointer basis but NOT in the Hadamard-rotated basis: the pointer basis is genuinely selected, not arbitrary. The p₀ ≠ p₁ hypothesis is load-bearing — at p₀ = p₁ the state is fully mixed and diagonal in every basis.

Concrete non-vacuity witness

noncomputable def CSD.Empirical.CSDBridge.Einselection.einselectionWitness : EuclideanSpace ℂ (Fin 2)

A concrete qubit superposition (2, 1) with distinct Born weights p₀ = 4 ≠ 1 = p₁ (unnormalised; the einselection off-diagonal is scale-covariant and its non-vanishing depends only on p₀ ≠ p₁).

Equations

• CSD.Empirical.CSDBridge.Einselection.einselectionWitness = EuclideanSpace.single 0 2 + EuclideanSpace.single 1 1

@[simp]

theorem CSD.Empirical.CSDBridge.Einselection.einselectionWitness_apply_zero : einselectionWitness.ofLp 0 = 2

@[simp]

theorem CSD.Empirical.CSDBridge.Einselection.einselectionWitness_apply_one : einselectionWitness.ofLp 1 = 1

theorem CSD.Empirical.CSDBridge.Einselection.einselectionWitness_weights_ne : einselectionWitness.ofLp 0 * star (einselectionWitness.ofLp 0) ≠ einselectionWitness.ofLp 1 * star (einselectionWitness.ofLp 1)

The witness has distinct Born weights: p₀ = 4 ≠ 1 = p₁. Non-vacuity for decohere_not_diagonal_in_rotated_basis.

theorem CSD.Empirical.CSDBridge.Einselection.einselectionWitness_offDiag : (QM.Gates.qmH * LF6.decohereReduced einselectionWitness * QM.Gates.qmH) 0 1 = 3 / 2

The witness's rotated off-diagonal is 3/2 ≠ 0. Concrete value of the einselection coherence in the Hadamard-rotated basis: (p₀ − p₁)/2 = (4 − 1)/2 = 3/2.

Capstone

theorem CSD.Empirical.CSDBridge.Einselection.einselection : LF6.decohereReduced einselectionWitness 0 1 = 0 ∧ (QM.Gates.qmH * LF6.decohereReduced einselectionWitness * QM.Gates.qmH) 0 1 = 3 / 2 ∧ (QM.Gates.qmH * LF6.decohereReduced einselectionWitness * QM.Gates.qmH) 0 1 ≠ 0

The einselection capstone: decoherence selects the pointer basis {e₀,e₁}. For the witness superposition (distinct Born weights):

1. diagonal in the pointer basis — decohereReduced einselectionWitness 0 1 = 0 (decoherence_offdiagonal_vanish): the pointer basis is the diagonalising one;
2. off-diagonal in the Hadamard rotation — (qmH · ρ_red · qmH) 0 1 = 3/2 (einselectionWitness_offDiag);
3. and it is nonzero — coherence persists in the rotated basis, so the pointer basis is genuinely selected.

This is the "why a preferred basis" result: decoherence is basis-selective. The selected basis is the de-isolation's pointer (computational) basis — the measurement context's choice — NOT the symmetric Fubini–Study typicality (LF4.fubiniStudy_forced_by_symmetry, #29: the unique U(N)-invariant law, basis-COVARIANT, picks no basis). Einselection is symmetry-breaking-by-context on the symmetric substrate. Honest scope: single-system; the basis is posited as the de-isolation's context, not derived from an environment Hamiltonian.

Part A: the degeneracy boundary of einselection (qubit)

decohere_hadamard_offDiag shows the rotated-basis off-diagonal is exactly the populations difference over two, (p₀ − p₁)/2. So einselection has a sharp boundary: it selects the pointer basis iff p₀ ≠ p₁, and degenerates exactly at p₀ = p₁, where the reduced state is the maximally mixed (1/2)·I — a scalar multiple of the identity, invariant under any unitary conjugation, so NO basis is preferred.

theorem CSD.Empirical.CSDBridge.Einselection.decohere_hadamard_offDiag_ne_zero_iff (ψ : EuclideanSpace ℂ (Fin 2)) : (QM.Gates.qmH * LF6.decohereReduced ψ * QM.Gates.qmH) 0 1 ≠ 0 ↔ ψ.ofLp 0 * star (ψ.ofLp 0) ≠ ψ.ofLp 1 * star (ψ.ofLp 1)

The off-diagonal vanishes in the rotated basis iff the populations are equal. Makes the einselection boundary crisp: the rotated-basis coherence (qmH · ρ_red · qmH) 0 1 = (p₀ − p₁)/2 is nonzero exactly when p₀ ≠ p₁.

theorem CSD.Empirical.CSDBridge.Einselection.decohere_degenerate_hadamard_offDiag_zero (ψ : EuclideanSpace ℂ (Fin 2)) (hp : ψ.ofLp 0 * star (ψ.ofLp 0) = ψ.ofLp 1 * star (ψ.ofLp 1)) : (QM.Gates.qmH * LF6.decohereReduced ψ * QM.Gates.qmH) 0 1 = 0

The degenerate case: at p₀ = p₁ the rotated off-diagonal is 0 — the same as the computational basis. So at equal populations the Hadamard-rotated state is also diagonal: the pointer basis is not distinguished from the rotated one. The einselection-FAILS side (contrast decohere_not_diagonal_in_rotated_basis).

theorem CSD.Empirical.CSDBridge.Einselection.decohere_degenerate_scalar (ψ : EuclideanSpace ℂ (Fin 2)) (hp : ψ.ofLp 0 * star (ψ.ofLp 0) = ψ.ofLp 1 * star (ψ.ofLp 1)) : LF6.decohereReduced ψ = (ψ.ofLp 0 * star (ψ.ofLp 0)) • 1

The degenerate reduced state is a scalar multiple of the identity. At equal populations p₀ = p₁, decohereReduced ψ = (ψ₀·star ψ₀) • 1. Being c • I it is invariant under any unitary conjugation (decohere_degenerate_basis_invariant), so no basis is einselected.

theorem CSD.Empirical.CSDBridge.Einselection.decohere_degenerate_half (ψ : EuclideanSpace ℂ (Fin 2)) (hψ : ‖ψ‖ = 1) (hp : ψ.ofLp 0 * star (ψ.ofLp 0) = ψ.ofLp 1 * star (ψ.ofLp 1)) : LF6.decohereReduced ψ = (1 / 2) • 1

The normalised degenerate state is exactly (1/2)·I (the maximally mixed qubit). For a unit ψ with equal populations p₀ = p₁, the dephased reduced state is (1/2) • 1. (p₀ + p₁ = ‖ψ‖² = 1 and p₀ = p₁ force p₀ = 1/2.)

theorem CSD.Empirical.CSDBridge.Einselection.decohere_degenerate_basis_invariant {N : ℕ} (U : Matrix (Fin N) (Fin N) ℂ) (hU : U * U.conjTranspose = 1) (c : ℂ) : U * c • 1 * U.conjTranspose = c • 1

Basis-invariance of a scalar matrix (general N). U · (c • I) · Uᴴ = c • I for any U with U Uᴴ = 1. This is the einselection-degenerates statement: at the degenerate locus the reduced state is c • I (decohere_degenerate_scalar), so conjugation by ANY unitary leaves it unchanged — no basis is preferred.

Concrete degenerate witness

noncomputable def CSD.Empirical.CSDBridge.Einselection.degenerateWitness : EuclideanSpace ℂ (Fin 2)

A concrete normalised qubit with EQUAL populations p₀ = p₁ = 1/2: (1/√2)(e₀ + e₁). Non-vacuity for the degeneracy boundary.

Equations

• CSD.Empirical.CSDBridge.Einselection.degenerateWitness = ↑(√2)⁻¹ • (EuclideanSpace.single 0 1 + EuclideanSpace.single 1 1)

@[simp]

theorem CSD.Empirical.CSDBridge.Einselection.degenerateWitness_apply_zero : degenerateWitness.ofLp 0 = ↑(√2)⁻¹

@[simp]

theorem CSD.Empirical.CSDBridge.Einselection.degenerateWitness_apply_one : degenerateWitness.ofLp 1 = ↑(√2)⁻¹

theorem CSD.Empirical.CSDBridge.Einselection.degenerateWitness_degenerate : degenerateWitness.ofLp 0 * star (degenerateWitness.ofLp 0) = degenerateWitness.ofLp 1 * star (degenerateWitness.ofLp 1)

The witness has equal populations p₀ = p₁ (the degenerate locus).

theorem CSD.Empirical.CSDBridge.Einselection.degenerateWitness_decohere_half : LF6.decohereReduced degenerateWitness = (1 / 2) • 1

The witness decoheres to (1/2)·I (the maximally mixed qubit). Concrete instance of decohere_degenerate_half, computed not asserted.

theorem CSD.Empirical.CSDBridge.Einselection.einselection_degenerate_boundary : LF6.decohereReduced degenerateWitness = (1 / 2) • 1 ∧ (QM.Gates.qmH * LF6.decohereReduced degenerateWitness * QM.Gates.qmH) 0 1 = 0 ∧ LF6.decohereReduced degenerateWitness 0 1 = 0 ∧ ∀ (U : Matrix (Fin 2) (Fin 2) ℂ), U * U.conjTranspose = 1 → U * LF6.decohereReduced degenerateWitness * U.conjTranspose = LF6.decohereReduced degenerateWitness

The qubit degeneracy-boundary capstone. For the equal-population witness:

1. decohereReduced = (1/2)·I — the maximally mixed scalar state (degenerateWitness_decohere_half);
2. the Hadamard-rotated off-diagonal is 0 — SAME as the computational basis, so the rotated basis is not distinguished (decohere_degenerate_hadamard_offDiag_zero);
3. the computational-basis off-diagonal is 0 (decoherence_offdiagonal_vanish);
4. conjugation by ANY unitary leaves the state unchanged (decohere_degenerate_basis_invariant): no basis is einselected.

This is the einselection-FAILS side, sharply contrasting einselection (where p₀ ≠ p₁ and the pointer basis IS selected). The boundary is exactly p₀ = p₁ (decohere_hadamard_offDiag_ne_zero_iff).

Part B: general-N einselection (lift off the qubit)

The dephasing channel decohereReducedN ρ := diagonal (fun i => ρ i i) zeroes the off-diagonal coherences of any density ρ and keeps the diagonal pointer-basis populations, for any N. The computational basis is the pointer basis. The degeneracy boundary lifts too: if all populations are equal (ρ i i = 1/N), the channel output is (1/N)·I, basis-invariant, einselection degenerates.

noncomputable def CSD.Empirical.CSDBridge.Einselection.decohereReducedN {N : ℕ} (ρ : Matrix (Fin N) (Fin N) ℂ) : Matrix (Fin N) (Fin N) ℂ

The general-N dephasing channel (pointer-basis selection). Zeroes the off-diagonal entries of a density ρ, keeping the diagonal (the pointer populations). The computational basis is the pointer basis by construction.

Equations

• CSD.Empirical.CSDBridge.Einselection.decohereReducedN ρ = Matrix.diagonal fun (i : Fin N) => ρ i i

theorem CSD.Empirical.CSDBridge.Einselection.decohereReducedN_offDiag_zero {N : ℕ} (ρ : Matrix (Fin N) (Fin N) ℂ) {i j : Fin N} (h : i ≠ j) : decohereReducedN ρ i j = 0

Off-diagonals killed (einselection, general N). i ≠ j ⇒ (decohereReducedN ρ) i j = 0.

theorem CSD.Empirical.CSDBridge.Einselection.decohereReducedN_diagonal {N : ℕ} (ρ : Matrix (Fin N) (Fin N) ℂ) (i : Fin N) : decohereReducedN ρ i i = ρ i i

Diagonal preserved (the pointer populations). (decohereReducedN ρ) i i = ρ i i.

theorem CSD.Empirical.CSDBridge.Einselection.einselectionN {N : ℕ} (ρ : Matrix (Fin N) (Fin N) ℂ) : (∀ (i j : Fin N), i ≠ j → decohereReducedN ρ i j = 0) ∧ ∀ (i : Fin N), decohereReducedN ρ i i = ρ i i

General-N einselection. The dephasing channel kills off-diagonals and preserves the diagonal pointer populations: the computational basis is the pointer basis. Note: stated alone this is definitional (decohereReducedN ρ := diagonal (ρ i i), so "off-diagonal of a diagonal is zero"); the einselection CONTENT - that the channel genuinely acts on a coherent state - lives in decohereReducedN_acts_nontrivial (off-diagonal nonzero before, 0 after) and decohereReducedN_outerProduct (the restriction to the derived qubit decohereReduced).

theorem CSD.Empirical.CSDBridge.Einselection.decohereReducedN_outerProduct {N : ℕ} [NeZero N] (ψ : EuclideanSpace ℂ (Fin N)) : decohereReducedN (LF2.outerProduct ψ) = LF6.decohereReduced ψ

The general-N channel restricts to the qubit einselection. decohereReducedN (|ψ⟩⟨ψ|) = decohereReduced ψ: the abstract dephasing channel on the pure-state density reproduces the LF6-B reduced state.

theorem CSD.Empirical.CSDBridge.Einselection.decohereReducedN_acts_nontrivial {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) {i j : Fin N} (hij : i ≠ j) (hi : ψ.ofLp i ≠ 0) (hj : ψ.ofLp j ≠ 0) : LF2.outerProduct ψ i j ≠ 0 ∧ decohereReducedN (LF2.outerProduct ψ) i j = 0

Non-vacuity: the dephasing genuinely acts. For a pure-state density with two nonzero components ψᵢ, ψⱼ (i ≠ j), the off-diagonal (|ψ⟩⟨ψ|) i j = ψᵢ·star ψⱼ is NONZERO before dephasing and exactly 0 after. The channel is not vacuous.

theorem CSD.Empirical.CSDBridge.Einselection.decohereReducedN_degenerate_scalar {N : ℕ} [NeZero N] (ρ : Matrix (Fin N) (Fin N) ℂ) (hdeg : ∀ (i : Fin N), ρ i i = 1 / ↑N) : decohereReducedN ρ = (1 / ↑N) • 1

General-N degeneracy boundary. If all populations are equal (ρ i i = 1/N), the dephased state is (1/N)·I — a scalar multiple of the identity. Einselection degenerates: basis-invariant (einselectionN_degenerate).

theorem CSD.Empirical.CSDBridge.Einselection.decohereReducedN_maximally_mixed {N : ℕ} [NeZero N] : decohereReducedN ((1 / ↑N) • 1) = (1 / ↑N) • 1

Non-vacuity of the degenerate case: the maximally mixed input. The dephasing channel fixes (1/N)·I (the maximally mixed state): decohereReducedN ((1/N)·I) = (1/N)·I. A genuine equal-populations witness, scalar·I in and out.

theorem CSD.Empirical.CSDBridge.Einselection.einselectionN_degenerate {N : ℕ} [NeZero N] (ρ : Matrix (Fin N) (Fin N) ℂ) (hdeg : ∀ (i : Fin N), ρ i i = 1 / ↑N) : decohereReducedN ρ = (1 / ↑N) • 1 ∧ ∀ (U : Matrix (Fin N) (Fin N) ℂ), U * U.conjTranspose = 1 → U * decohereReducedN ρ * U.conjTranspose = decohereReducedN ρ

General-N degeneracy capstone. At equal populations (ρ i i = 1/N):

1. the dephased state is (1/N)·I (decohereReducedN_degenerate_scalar);
2. it is invariant under ANY unitary conjugation U (·) Uᴴ (U Uᴴ = 1): einselection degenerates, no basis preferred (decohere_degenerate_basis_invariant).

The contrast with einselectionN (off this locus a definite diagonal pointer basis IS singled out) is the general-N einselection-selects-vs-degenerates boundary.