SigmaLayer/PointerRotation: the fixed-outcome pointer rotation (brick 1)

Category: dynamical measurement — the smooth-Hamiltonian witness route (specs/pointer-witness-plan.md brick 1).

The generator for outcome j is the Hermitian plane-swap hⱼ = |f₀⟩⟨f_{j+1}| + |f_{j+1}⟩⟨f₀| (pointerH, pointerH_isHermitian). Its rotation family

pointerRot θ j = 1 + (cos θ − 1)•Pⱼ − (i sin θ)•hⱼ, Pⱼ = |f₀⟩⟨f₀| + |f_{j+1}⟩⟨f_{j+1}|

is a continuous one-parameter unitary group — machine-checked as: the group law (pointerRot_add), the identity at 0 (pointerRot_zero), unitarity (pointerRot_mem_unitaryGroup, via the closed form (pointerRot θ)ᴴ = pointerRot (−θ)), and continuity in θ, both into the unitary group (continuous_pointerRotU) and through the projective action (continuous_pointerRotU_smul). At the quarter turn it transports the ready vertex to the record vertex, projectively:

pointerRotU (π/2) j • readyState = recordState j (pointerRotU_pi_div_two_ready),

and every pointerRotU θ j preserves the pointer Fubini–Study measure (pointerRotU_measurePreserving — FS unitary invariance, the same one-liner as joinSwap_measurePreserving). This is the map the torus register provably could not give as any continuous flow slice (shearEvolve_not_continuous): here record transport is a continuous curve of unitaries, no seams, no flux.

⚠️ Honest scope. The identification pointerRot θ j = exp(−iθ hⱼ) — the generation statement — is brick 5 of the plan, not this module; here the family is given in closed trigonometric form and its group properties are proved directly (the closed form and the exponential agree because both solve the same linear recursion, but that identification is not formalised yet, and nothing below cites it). What brick 1 delivers is exactly: a continuous one-parameter unitary group on the pointer, with Hermitian infinitesimal data pointerH, transporting ready → record and preserving Liouville. The selector-modulated coupling (bump-weighted sums of the pointerH j — which do not commute pairwise, since all planes share f₀) is brick 2 and will need the exponential route, not this closed form.

References

specs/pointer-witness-plan.md (bricks 1, 2, 5); specs/BACKLOG.md (the ★ L row); specs/future-work.md. Reused corpus API: Matrix.single algebra (Mathlib), smul_mk_eq_mk_toEuclideanLin + orbit_map_continuous (Mathlib/LinearAlgebra/Projectivization/{TransitionProbability,FubiniStudy}.lean staging), fubiniStudyMeasure_smul_invariant (ibid.), readyState/recordState (SigmaLayer/PointerArena.lean).

The generator and its plane

def CSD.RecordLayer.pointerPlane {K : ℕ} (j : Fin K) : Matrix (Fin (K + 1)) (Fin (K + 1)) ℂ

The plane projector Pⱼ = |f₀⟩⟨f₀| + |f_{j+1}⟩⟨f_{j+1}| onto the ready–record plane.

Equations

• CSD.RecordLayer.pointerPlane j = Matrix.single 0 0 1 + Matrix.single j.succ j.succ 1

def CSD.RecordLayer.pointerH {K : ℕ} (j : Fin K) : Matrix (Fin (K + 1)) (Fin (K + 1)) ℂ

The Hermitian generator hⱼ = |f₀⟩⟨f_{j+1}| + |f_{j+1}⟩⟨f₀|: the plane swap between the ready direction and the j-th record direction.

Equations

• CSD.RecordLayer.pointerH j = Matrix.single 0 j.succ 1 + Matrix.single j.succ 0 1

theorem CSD.RecordLayer.succ_ne_zero' {K : ℕ} (j : Fin K) : j.succ ≠ 0

theorem CSD.RecordLayer.pointerPlane_mul_self {K : ℕ} (j : Fin K) : pointerPlane j * pointerPlane j = pointerPlane j

theorem CSD.RecordLayer.pointerH_mul_self {K : ℕ} (j : Fin K) : pointerH j * pointerH j = pointerPlane j

theorem CSD.RecordLayer.pointerPlane_mul_pointerH {K : ℕ} (j : Fin K) : pointerPlane j * pointerH j = pointerH j

theorem CSD.RecordLayer.pointerH_mul_pointerPlane {K : ℕ} (j : Fin K) : pointerH j * pointerPlane j = pointerH j

theorem CSD.RecordLayer.single_one_conjTranspose {K : ℕ} (a b : Fin (K + 1)) : (Matrix.single a b 1).conjTranspose = Matrix.single b a 1

theorem CSD.RecordLayer.pointerPlane_conjTranspose {K : ℕ} (j : Fin K) : (pointerPlane j).conjTranspose = pointerPlane j

theorem CSD.RecordLayer.pointerH_isHermitian {K : ℕ} (j : Fin K) : (pointerH j).IsHermitian

The generator is Hermitian — the coupling the smooth witness rotates by is honest Hamiltonian data.

The rotation family

noncomputable def CSD.RecordLayer.pointerRot {K : ℕ} (θ : ℝ) (j : Fin K) : Matrix (Fin (K + 1)) (Fin (K + 1)) ℂ

The pointer rotation at angle θ in the ready–record plane of outcome j: 1 + (cos θ − 1)•Pⱼ − (i sin θ)•hⱼ — the closed form of exp(−iθ hⱼ) (the identification itself is brick 5; nothing here consumes it).

Equations

• CSD.RecordLayer.pointerRot θ j = 1 + (↑(Real.cos θ) - 1) • CSD.RecordLayer.pointerPlane j + -(Complex.I * ↑(Real.sin θ)) • CSD.RecordLayer.pointerH j

theorem CSD.RecordLayer.pointer_combo_mul {K : ℕ} (j : Fin K) (x₁ y₁ x₂ y₂ : ℂ) : (1 + x₁ • pointerPlane j + y₁ • pointerH j) * (1 + x₂ • pointerPlane j + y₂ • pointerH j) = 1 + (x₁ + x₂ + x₁ * x₂ + y₁ * y₂) • pointerPlane j + (y₁ + y₂ + x₁ * y₂ + y₁ * x₂) • pointerH j

The generic product in the rotation plane's algebra: {1, Pⱼ, hⱼ} is closed under multiplication, with the stated structure constants.

theorem CSD.RecordLayer.pointerRot_zero {K : ℕ} (j : Fin K) : pointerRot 0 j = 1

The rotation at angle 0 is the identity.

theorem CSD.RecordLayer.pointerRot_add {K : ℕ} (θ₁ θ₂ : ℝ) (j : Fin K) : pointerRot θ₁ j * pointerRot θ₂ j = pointerRot (θ₁ + θ₂) j

The group law: rotations in a fixed plane compose additively in the angle.

theorem CSD.RecordLayer.pointerRot_conjTranspose {K : ℕ} (θ : ℝ) (j : Fin K) : (pointerRot θ j).conjTranspose = pointerRot (-θ) j

The conjugate transpose of a rotation is the reverse rotation.

theorem CSD.RecordLayer.pointerRot_mem_unitaryGroup {K : ℕ} (θ : ℝ) (j : Fin K) : pointerRot θ j ∈ Matrix.unitaryGroup (Fin (K + 1)) ℂ

Every pointer rotation is unitary.

noncomputable def CSD.RecordLayer.pointerRotU {K : ℕ} (θ : ℝ) (j : Fin K) : ↥(Matrix.unitaryGroup (Fin (K + 1)) ℂ)

The pointer rotation as a unitary-group element.

Equations

• CSD.RecordLayer.pointerRotU θ j = ⟨CSD.RecordLayer.pointerRot θ j, ⋯⟩

theorem CSD.RecordLayer.pointerRotU_add {K : ℕ} (θ₁ θ₂ : ℝ) (j : Fin K) : pointerRotU θ₁ j * pointerRotU θ₂ j = pointerRotU (θ₁ + θ₂) j

The group law at the unitary-group level.

Continuity

theorem CSD.RecordLayer.continuous_pointerRotU {K : ℕ} (j : Fin K) : Continuous fun (θ : ℝ) => pointerRotU θ j

The rotation family is continuous in the angle — with the group law and unitarity, pointerRotU · j is a continuous one-parameter unitary group.

theorem CSD.RecordLayer.continuous_pointerRotU_smul {K : ℕ} (j : Fin K) (q : Pointer K) : Continuous fun (θ : ℝ) => pointerRotU θ j • q

Continuity through the projective action: for every pointer state q, the rotation orbit θ ↦ Uⱼ(θ) • q is a continuous curve on ℂℙ^K.

Liouville preservation and record transport

theorem CSD.RecordLayer.pointerRotU_measurePreserving {K : ℕ} (θ : ℝ) (j : Fin K) (q₀ : Pointer K) : MeasureTheory.MeasurePreserving (fun (q : Pointer K) => pointerRotU θ j • q) (Matrix.UnitaryGroup.fubiniStudyMeasure q₀) (Matrix.UnitaryGroup.fubiniStudyMeasure q₀)

Every pointer rotation preserves the pointer Fubini–Study measure — Liouville preservation is FS unitary invariance, exactly as on the join arena.

theorem CSD.RecordLayer.pointerRotU_pi_div_two_ready {K : ℕ} (j : Fin K) : pointerRotU (Real.pi / 2) j • readyState = recordState j

The quarter turn transports ready to record: Uⱼ(π/2) • [f₀] = [f_{j+1}] (projectively; the representative picks up the phase −i).