RecordLayer/ArenaTorus: the conserved-quantity torus acting on the pointer arena

Category: 7-SigmaLayer (dynamical measurement) — specs/BACKLOG.md §A (joint-arena lift), the kinematic half of the joint lift RecordLayer/JointLift.lean builds.

What this is

The arena PointerArena N N = (ℂℙ^{N-1} × T²) × ℂℙ^{N-1} carries an (N+1)-torus of symmetries that fix every quantity the measurement stroke reads:

• phaseUnitary g, g : Fin N → AddCircle 1, is the diagonal unitary diag (e^{2πi g₀}, …, e^{2πi g_{N-1}}). It rotates the base point along its moment fibre — the moment map is exactly |ψⱼ|²/‖ψ‖², which does not see the phases (momentMap_phaseUnitary_smul).
• the last circle translates the register's conjugate coordinate θ₂, leaving the register θ₁ (what the weights read) alone.

torusAct is the resulting action of ArenaTorus N := (Fin N → AddCircle 1) × AddCircle 1 on the arena. It is jointly continuous, hence jointly measurable (continuous_torusAct, measurable_torusAct), it composes (torusAct_add), and every torusAct g preserves the arena Liouville measure pointerLiouville p₀ q₀ (torusAct_measurePreserving) — the Fubini–Study factor by fsMeasure_smul_invariant, the torus factors by translation invariance of Haar measure.

Why it exists

A back-reacting joint flow moves the base — but by how much and where is governed by conservation: the moments and the register are constants of motion (IsJointLift), so the base can only move along this torus. The joint lift is therefore a twist of the fibrewise witness by a torus element that depends on the conserved data alone, and the general fact that such twists preserve measure is MeasurePreserving.vadd_twist_of_invariant (Mathlib/MeasureTheory/InvariantTwist.lean). This module supplies every hypothesis of that lemma for the arena.

ContextField.TorusInvariant names the one condition on a context field that the construction needs — rates constant along base phase rotations — and momentContext has it.

References

specs/frozen-base-obstruction-scoping.md (brick 3, joint lift); specs/future-work.md; RecordLayer/JointLift.lean (the consumer); RecordLayer/JointFlowTransfer.lean (IsJointLift); Mathlib/LinearAlgebra/Projectivization/FubiniStudy.lean (fsMeasure_smul_invariant); Mathlib/LinearAlgebra/Projectivization/ FubiniStudyUnique.lean (instContinuousSMul_projectivization); Mathlib/LinearAlgebra/Projectivization/TransitionProbability.lean (smul_mk_eq_mk_toEuclideanLin).

The diagonal phase unitary

@[reducible, inline]

noncomputable abbrev CSD.RecordLayer.circlePhase (g : AddCircle 1) : ℂ

The unit-modulus phase e^{2πi g} of a point g : AddCircle 1, as a complex number.

Equations

• CSD.RecordLayer.circlePhase g = ↑g.toCircle

theorem CSD.RecordLayer.norm_circlePhase (g : AddCircle 1) : ‖circlePhase g‖ = 1

theorem CSD.RecordLayer.circlePhase_add (a b : AddCircle 1) : circlePhase (a + b) = circlePhase a * circlePhase b

@[simp]

theorem CSD.RecordLayer.circlePhase_zero : circlePhase 0 = 1

theorem CSD.RecordLayer.continuous_circlePhase : Continuous circlePhase

noncomputable def CSD.RecordLayer.phaseUnitary {N : ℕ} (g : Fin N → AddCircle 1) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The diagonal unitary diag (e^{2πi g₀}, …, e^{2πi g_{N-1}}), as an element of the unitary group. This is the base torus of the joint lift: it rotates every coordinate of a state vector by its own phase, and so moves a projective point along its moment fibre.

Equations

• CSD.RecordLayer.phaseUnitary g = ⟨Matrix.diagonal fun (j : Fin N) => CSD.RecordLayer.circlePhase (g j), ⋯⟩

@[simp]

theorem CSD.RecordLayer.phaseUnitary_val {N : ℕ} (g : Fin N → AddCircle 1) : ↑(phaseUnitary g) = Matrix.diagonal fun (j : Fin N) => circlePhase (g j)

theorem CSD.RecordLayer.phaseUnitary_add {N : ℕ} (a b : Fin N → AddCircle 1) : phaseUnitary (a + b) = phaseUnitary a * phaseUnitary b

The phase unitaries form a homomorphic image of the torus.

@[simp]

theorem CSD.RecordLayer.phaseUnitary_zero {N : ℕ} : phaseUnitary 0 = 1

theorem CSD.RecordLayer.continuous_phaseUnitary {N : ℕ} : Continuous phaseUnitary

theorem CSD.RecordLayer.toEuclideanLin_phaseUnitary_apply {N : ℕ} (g : Fin N → AddCircle 1) (v : EuclideanSpace ℂ (Fin N)) (j : Fin N) : ((Matrix.toEuclideanLin ↑(phaseUnitary g)) v).ofLp j = circlePhase (g j) * v.ofLp j

The coordinates of a phase-rotated vector are the rotated coordinates.

theorem CSD.RecordLayer.norm_toEuclideanLin_phaseUnitary_apply {N : ℕ} (g : Fin N → AddCircle 1) (v : EuclideanSpace ℂ (Fin N)) (j : Fin N) : ‖((Matrix.toEuclideanLin ↑(phaseUnitary g)) v).ofLp j‖ = ‖v.ofLp j‖

Phase rotation preserves every coordinate norm.

theorem CSD.RecordLayer.momentMap_phaseUnitary_smul {N : ℕ} (g : Fin N → AddCircle 1) (p : LF4.CPN N) (i : Fin N) : Projectivization.momentMap (phaseUnitary g • p) i = Projectivization.momentMap p i

The moment map does not see the base phases. momentMap (phaseUnitary g • p) = momentMap p: the phase torus moves a projective point along its moment fibre.

theorem CSD.RecordLayer.phaseUnitary_smul_mk_ne_of_ne {N : ℕ} (g : Fin N → AddCircle 1) {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) {j k : Fin N} (hj : v.ofLp j ≠ 0) (hk : v.ofLp k ≠ 0) (hg : circlePhase (g j) ≠ circlePhase (g k)) : phaseUnitary g • Projectivization.mk ℂ v hv ≠ Projectivization.mk ℂ v hv

A phase rotation that acts by different phases on two coordinates where the vector is supported moves the projective point. This is the concrete "base-moves" witness the joint lift hands to its consumers.

Torus-invariant context fields

def CSD.RecordLayer.ContextField.TorusInvariant {N : ℕ} (c : ContextField N) : Prop

A context field whose rates are constant along base phase rotations. This is the single condition the joint lift needs of the context: the conserved quantities that steer the twist must not themselves move under the twist.

Equations

• c.TorusInvariant = ∀ (g : Fin N → AddCircle 1) (p : CSD.LF4.CPN N) (j : Fin N), c.rate (CSD.RecordLayer.phaseUnitary g • p) j = c.rate p j

theorem CSD.RecordLayer.momentContext_torusInvariant {N : ℕ} : (momentContext N).TorusInvariant

The moment context is torus-invariant.

The arena torus and its action

@[reducible, inline]

abbrev CSD.RecordLayer.ArenaTorus (N : ℕ) : Type

The (N+1)-torus of conserved-quantity symmetries: N base phases and one translation of the register's conjugate coordinate θ₂.

Equations

• CSD.RecordLayer.ArenaTorus N = ((Fin N → AddCircle 1) × AddCircle 1)

noncomputable def CSD.RecordLayer.torusAct {N K : ℕ} (g : ArenaTorus N) (y : PointerArena N K) : PointerArena N K

The torus action on the arena: rotate the base along its moment fibre, translate θ₂, fix the register θ₁ and the pointer.

Equations

• CSD.RecordLayer.torusAct g y = ((CSD.RecordLayer.phaseUnitary g.1 • y.1.1, y.1.2.1, y.1.2.2 + g.2), y.2)

@[simp]

theorem CSD.RecordLayer.torusAct_fst_fst {N K : ℕ} (g : ArenaTorus N) (y : PointerArena N K) : (torusAct g y).1.1 = phaseUnitary g.1 • y.1.1

@[simp]

theorem CSD.RecordLayer.torusAct_register {N K : ℕ} (g : ArenaTorus N) (y : PointerArena N K) : (torusAct g y).1.2.1 = y.1.2.1

@[simp]

theorem CSD.RecordLayer.torusAct_conjugate {N K : ℕ} (g : ArenaTorus N) (y : PointerArena N K) : (torusAct g y).1.2.2 = y.1.2.2 + g.2

@[simp]

theorem CSD.RecordLayer.torusAct_snd {N K : ℕ} (g : ArenaTorus N) (y : PointerArena N K) : (torusAct g y).2 = y.2

@[simp]

theorem CSD.RecordLayer.torusAct_zero {N K : ℕ} (y : PointerArena N K) : torusAct 0 y = y

theorem CSD.RecordLayer.torusAct_add {N K : ℕ} (a b : ArenaTorus N) (y : PointerArena N K) : torusAct a (torusAct b y) = torusAct (a + b) y

The action law: torusAct a ∘ torusAct b = torusAct (a + b).

theorem CSD.RecordLayer.continuous_torusAct {N K : ℕ} : Continuous (Function.uncurry torusAct)

The action is jointly continuous.

theorem CSD.RecordLayer.measurable_torusAct {N K : ℕ} : Measurable (Function.uncurry torusAct)

The action is jointly measurable — the hypothesis MeasurePreserving.vadd_twist_of_invariant asks for.

theorem CSD.RecordLayer.torusAct_measurePreserving {N K : ℕ} (g : ArenaTorus N) (p₀ : LF4.CPN N) (q₀ : Pointer K) : MeasureTheory.MeasurePreserving (torusAct g) (pointerLiouville p₀ q₀) (pointerLiouville p₀ q₀)

Every torus element preserves the arena Liouville measure. Fubini–Study is unitarily invariant; Haar measure on the register torus is translation invariant; the pointer factor is untouched.

noncomputable def CSD.RecordLayer.torusHaar (N : ℕ) : MeasureTheory.Measure (ArenaTorus N)

Haar measure on the arena torus is the product of the coordinate Haar measures.

Equations

• CSD.RecordLayer.torusHaar N = MeasureTheory.volume.prod MeasureTheory.volume

instance CSD.RecordLayer.instIsAddLeftInvariantArenaTorusTorusHaar {N : ℕ} : (torusHaar N).IsAddLeftInvariant

instance CSD.RecordLayer.instIsProbabilityMeasureArenaTorusTorusHaar {N : ℕ} : MeasureTheory.IsProbabilityMeasure (torusHaar N)