SigmaLayer/JoinGeneration: the join relocation is generated

Category: dynamical measurement — the positive answer the swap architecture could not give.

RelocationObstruction.lean showed the bank-swap collapse stroke cannot be the time-one map of any flow, in two independent horns: a factor exchange of a product arena is not homotopic to the identity, and the non-permutation repair is not injective. This module shows the join architecture escapes both, and escapes them for a structural reason rather than by luck.

Why the join escapes

The bank arena is a product, (Σ × pointer) × (Fin N → Σ), and pointerBankSwap exchanges two of its factors. The join arena is ℂℙ^{N+N-1}, a single projective space: joinSwap b i p = joinU b i • p is the action of one unitary on one connected space. There are no two arena factors to exchange, so horn one has nothing to act on, and a projective unitary is bijective, so horn two has nothing to act on either.

That is the negative half. The positive half is that the escape is constructive:

• joinMat_mul_self — the join permutation matrix is an involution, and joinMat_conjTranspose says it is Hermitian. So its eigenvalues are ±1.
• joinProj — hence Q = ½(1 - P) is a Hermitian idempotent, the spectral projection onto the -1 eigenspace.
• joinFlowMat — hence U(t) = (1 - Q) + e^{iπt}Q is a one-parameter family of unitaries with U 0 = 1 and U 1 = P.
• ★★ joinFlowMat_hasDerivAt — and it solves the Schrödinger equation U'(t) = (i·H)·U(t) for the explicit Hermitian generator H = π·Q.
• ★★ joinSwap_eq_flowTimeOne — so the join relocation is the time-one map of a Hamiltonian flow.

No matrix exponential is needed: on an idempotent the exponential series collapses to 1 + (e^z - 1)Q, and writing that closed form down directly turns the whole construction into algebra.

What this settles

Collapse can be dynamics. PointerGeneration.lean generated the record-creating stroke; this generates a relocation stroke. The obstruction in RelocationObstruction.lean is therefore genuinely about the swap architecture, exactly as its scope note claimed, and not about collapse-as-dynamics in general.

The design rule it yields is sharp: a generated relocation must be a bijection that is not a factor exchange, and the join route satisfies both by being a unitary on an irreducible arena rather than a permutation of coordinates on a reducible one.

⚠️ Scope. This generates the join swap, which is the relocation half of the degenerate-Lüders witness (JoinLuders.lean). It does not by itself make the whole two-stroke composite a single flow: the composite is still triggered by a readout, and the trigger is where no_everywhere_correlation bites. What is now established is that the relocation is not the obstacle.

References

SigmaLayer/JoinArena.lean (joinMat, joinU, joinSwap, joinSwap_measurePreserving); SigmaLayer/JoinLuders.lean (joinWitness_blockLuders); SigmaLayer/RelocationObstruction.lean (the two horns this escapes); SigmaLayer/PointerGeneration.lean (rampedU_schrodinger, the record-stroke analogue); specs/BACKLOG.md.

The join permutation is a Hermitian involution

theorem CSD.RecordLayer.joinMat_conjTranspose {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : (joinMat b i).conjTranspose = joinMat b i

The join permutation matrix is Hermitian: it is real, and the underlying permutation is an involution, so it is its own transpose.

theorem CSD.RecordLayer.joinMat_mul_self {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : joinMat b i * joinMat b i = 1

The join permutation matrix is an involution. Being unitary and Hermitian, it squares to the identity.

The spectral projection onto the -1 eigenspace

noncomputable def CSD.RecordLayer.joinProj {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Matrix (Fin (N + N)) (Fin (N + N)) ℂ

Q = ½(1 - P): the spectral projection onto the -1 eigenspace of the join permutation.

Equations

• CSD.RecordLayer.joinProj b i = (1 / 2) • (1 - CSD.RecordLayer.joinMat b i)

theorem CSD.RecordLayer.joinProj_conjTranspose {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : (joinProj b i).conjTranspose = joinProj b i

theorem CSD.RecordLayer.joinProj_mul_self {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : joinProj b i * joinProj b i = joinProj b i

Q is idempotent, from P² = 1.

theorem CSD.RecordLayer.one_sub_joinProj_mul {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : (1 - joinProj b i) * joinProj b i = 0

The complementary projection annihilates Q.

theorem CSD.RecordLayer.joinProj_mul_one_sub {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : joinProj b i * (1 - joinProj b i) = 0

theorem CSD.RecordLayer.one_sub_joinProj_mul_self {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : (1 - joinProj b i) * (1 - joinProj b i) = 1 - joinProj b i

The flow

noncomputable def CSD.RecordLayer.joinFlowMat {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (t : ℝ) : Matrix (Fin (N + N)) (Fin (N + N)) ℂ

★ The join flow. U(t) = (1 - Q) + e^{iπt}Q, the phase rotation that acts trivially on the +1 eigenspace and by e^{iπt} on the -1 eigenspace.

This is exp(itπQ) in closed form: on an idempotent the exponential series collapses to 1 + (e^z - 1)Q, so no matrix exponential is needed.

Equations

• CSD.RecordLayer.joinFlowMat b i t = 1 - CSD.RecordLayer.joinProj b i + Complex.exp (↑Real.pi * Complex.I * ↑t) • CSD.RecordLayer.joinProj b i

@[simp]

theorem CSD.RecordLayer.joinFlowMat_zero {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : joinFlowMat b i 0 = 1

@[simp]

theorem CSD.RecordLayer.joinFlowMat_one {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : joinFlowMat b i 1 = joinMat b i

★ At time one the flow is the join permutation, because e^{iπ} = -1 turns (1 - Q) - Q = 1 - 2Q back into P.

theorem CSD.RecordLayer.conj_exp_mul_exp (t : ℝ) : (starRingEnd ℂ) (Complex.exp (↑Real.pi * Complex.I * ↑t)) * Complex.exp (↑Real.pi * Complex.I * ↑t) = 1

The scalar factor has modulus one.

theorem CSD.RecordLayer.joinFlowMat_mem_unitaryGroup {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (t : ℝ) : joinFlowMat b i t ∈ Matrix.unitaryGroup (Fin (N + N)) ℂ

★ The flow is unitary at every time.

noncomputable def CSD.RecordLayer.joinFlowU {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (t : ℝ) : ↥(Matrix.unitaryGroup (Fin (N + N)) ℂ)

The join flow as a family of unitaries.

Equations

• CSD.RecordLayer.joinFlowU b i t = ⟨CSD.RecordLayer.joinFlowMat b i t, ⋯⟩

The generator

noncomputable def CSD.RecordLayer.joinGen {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : Matrix (Fin (N + N)) (Fin (N + N)) ℂ

The Hermitian generator H = π·Q of the join flow.

Equations

• CSD.RecordLayer.joinGen b i = ↑Real.pi • CSD.RecordLayer.joinProj b i

theorem CSD.RecordLayer.joinGen_conjTranspose {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : (joinGen b i).conjTranspose = joinGen b i

theorem CSD.RecordLayer.joinGen_isHermitian {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) : (joinGen b i).IsHermitian

theorem CSD.RecordLayer.hasDerivAt_expPath (t : ℝ) : HasDerivAt (fun (s : ℝ) => Complex.exp (↑Real.pi * Complex.I * ↑s)) (↑Real.pi * Complex.I * Complex.exp (↑Real.pi * Complex.I * ↑t)) t

The scalar path's derivative.

theorem CSD.RecordLayer.joinFlowMat_hasDerivAt {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (t : ℝ) : HasDerivAt (joinFlowMat b i) (Complex.I • joinGen b i * joinFlowMat b i t) t

★★ The join flow solves the Schrödinger equation for the explicit Hermitian generator H = π·Q:

`U'(t) = (i·H)·U(t)`.

This is the join-architecture analogue of rampedU_schrodinger, and it is what pointerBankSwap provably cannot have.

The payoff: the join relocation is a flow at time one

theorem CSD.RecordLayer.joinSwap_eq_flowTimeOne {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (p : LF4.CPN (N + N)) : joinSwap b i p = joinFlowU b i 1 • p

★★ The join relocation is the time-one map of a Hamiltonian flow.

joinSwap acts as joinU • p, and joinU is joinFlowU 1 for a flow that starts at the identity and is generated by the Hermitian joinGen. So the collapse stroke of the join architecture is dynamics, in exactly the sense RelocationObstruction.lean proves the bank-swap stroke can never be.

theorem CSD.RecordLayer.joinFlowU_zero_smul {N K : ℕ} (b : Fin N → Fin K) (i : Fin K) (p : LF4.CPN (N + N)) : joinFlowU b i 0 • p = p

The flow starts at the identity, so it genuinely joins id to the relocation.