P1: the arena bridge — operator locality carried onto the record arena

Category: CV (continuous variables — the bridge from mode-local operators to the projective record arena).

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

The CV chain states locality as an operator notion: SupportedOn S A, commutators, the Lieb-Robinson cone. The record layer's arenas are projective spaces, where locality is a measure-and-set notion. Nothing translated between the two categories, and on 2026-08-10 that gap made a Lieb-Robinson bound on record redundancy unstatable (specs/eft-pillars-plan.md, P1 — the twice-observed bottleneck). This module is the translation.

• FieldArena K N — ℙ ℂ (EuclideanSpace ℂ (FieldConfig K N)), the epistemic base over the K-mode field.
• arenaDM p — the rank-one density of a ray: positive semidefinite (arenaDM_posSemidef), trace one (arenaDM_trace).
• arenaObs A p = re tr(ρ_p A) — a matrix observable read as a function on the arena. arenaObs_sub_le: arena observables are 1-Lipschitz in the operator norm — this is CR-1's Hölder-lite bound (QuantumInfo.abs_re_trace_mul_le) doing the category translation.
• arenaKick U p — a unitary as an arena self-map, constructed directly through Projectivization.mk (no MulAction instance needed at this index).
• arenaObs_kick — the bridge identity: arenaObs A (kick U p) = arenaObs (heisenberg U A) p. Schrödinger on the arena IS Heisenberg on the operator, so every operator-norm estimate about Heisenberg evolution becomes a sup-norm estimate about functions on the arena.
• ★ arenaObs_kick_of_disjointSupport — statics: an arena observable of mode set S is exactly invariant under any kick supported on disjoint T. Haag–Kastler locality (CV-8), restated as a fact about functions on the arena.
• ★★ arena_lightcone — the previously unstatable theorem: under a graph-local skew generator, a kick supported outside the graph d-ball of R changes any region-R arena observable after time t by at most 2·(2‖S‖t)^d/d! · ‖A‖. The Lieb-Robinson cone (CV-20), now a statement at the record-arena level: far-away interventions cannot reach the epistemic regions faster than the cone.

⚠️ Honest scope: the base arena — this arc is the transport layer. Both halves it originally deferred have since landed, closing P1: the definitional half (a field-structured flow as a structure with a locally-decomposed generator) in CV/FieldStructuredFlow.lean (2026-08-20), and the fibre-active extension (records written into the T² fibre by base-dependent strokes inherit the cone) in CV/FibredArenaBridge.lean (2026-08-20). What stays true of this module: its statements concern the base factor, and the fibred module consumes them through arenaObs. euclidean_norm_map_of_isom restates LF5's toEuclideanLin_norm_map_of_isom (same proof) to keep CV free of an LF5 import — rule-of-two note: unify in Mathlib staging when next touched.

References

specs/arena-bridge-plan.md (the feasibility record this executes); specs/eft-pillars-plan.md (P1); CV/ModeLocality.lean (commute_of_disjointSupport); CV/LiebRobinson.lean (heisenbergFlow, norm_commutator_spatial_factorial_le); Mathlib/QuantumInfo/UnitaryPerturbation.lean (CR-1); Mathlib/Analysis/Matrix/TrotterProduct.lean (exp_mem_unitaryGroup_of_skew); LF2/BornWrapper.lean (the outerProduct pattern this generalises).

The arena

@[reducible, inline]

abbrev CSD.CV.FieldArena (K N : ℕ) : Type

The field arena: the projective space of the K-mode field Hilbert space — the epistemic base on which records are read.

Equations

• CSD.CV.FieldArena K N = Projectivization ℂ (EuclideanSpace ℂ (CSD.CV.FieldConfig K N))

theorem CSD.CV.euclidean_norm_map_of_isom {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {A : Matrix κ ι ℂ} (hA : A.conjTranspose * A = 1) (ψ : EuclideanSpace ℂ ι) : ‖(Matrix.toEuclideanLin A) ψ‖ = ‖ψ‖

Norm preservation for isometric matrices through toEuclideanLin. Same proof as LF5's toEuclideanLin_norm_map_of_isom; restated to keep CV free of an LF5 import (rule-of-two note in the module docstring).

theorem CSD.CV.euclid_sum_norm_sq {ι : Type u_1} [Fintype ι] (x : EuclideanSpace ℂ ι) : ∑ i : ι, ‖x.ofLp i‖ ^ 2 = ‖x‖ ^ 2

Coordinate sum of squared norms is the squared Euclidean norm.

The rank-one density of a ray

noncomputable def CSD.CV.unitVec {K N : ℕ} (v : EuclideanSpace ℂ (FieldConfig K N)) : FieldConfig K N → ℂ

The unit representative of a vector, as a plain function: v/‖v‖.

Equations

• CSD.CV.unitVec v i = (↑‖v‖)⁻¹ * v.ofLp i

noncomputable def CSD.CV.dmVec {K N : ℕ} (v : EuclideanSpace ℂ (FieldConfig K N)) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The rank-one density of a vector: |v/‖v‖⟩⟨v/‖v‖|.

Equations

• CSD.CV.dmVec v = Matrix.vecMulVec (CSD.CV.unitVec v) (star (CSD.CV.unitVec v))

theorem CSD.CV.dmVec_apply {K N : ℕ} (v : EuclideanSpace ℂ (FieldConfig K N)) (i j : FieldConfig K N) : dmVec v i j = unitVec v i * star (unitVec v j)

theorem CSD.CV.dmVec_posSemidef {K N : ℕ} (v : EuclideanSpace ℂ (FieldConfig K N)) : (dmVec v).PosSemidef

The rank-one density is positive semidefinite.

theorem CSD.CV.mul_star_self_eq_norm_sq (z : ℂ) : z * star z = ↑(‖z‖ ^ 2)

A complex number times its own star is its squared norm.

theorem CSD.CV.dmVec_apply' {K N : ℕ} {v : EuclideanSpace ℂ (FieldConfig K N)} (i j : FieldConfig K N) : dmVec v i j = (↑(‖v‖ ^ 2))⁻¹ * (v.ofLp i * star (v.ofLp j))

The canonical entry form of the density: normalisation outside, raw coordinates inside.

theorem CSD.CV.dmVec_trace {K N : ℕ} {v : EuclideanSpace ℂ (FieldConfig K N)} (hv : v ≠ 0) : (dmVec v).trace = 1

The rank-one density of a nonzero vector has trace one.

theorem CSD.CV.dmVec_smul {K N : ℕ} {c : ℂ} (hc : c ≠ 0) {v : EuclideanSpace ℂ (FieldConfig K N)} (hv : v ≠ 0) : dmVec (c • v) = dmVec v

Scale invariance: the density depends only on the ray.

noncomputable def CSD.CV.arenaDM {K N : ℕ} (p : FieldArena K N) : Matrix (FieldConfig K N) (FieldConfig K N) ℂ

The density of a ray: arenaDM p = |p⟩⟨p| through the canonical representative — well-defined on the arena by dmVec_smul.

Equations

• CSD.CV.arenaDM p = CSD.CV.dmVec (Projectivization.rep p)

theorem CSD.CV.arenaDM_posSemidef {K N : ℕ} (p : FieldArena K N) : (arenaDM p).PosSemidef

theorem CSD.CV.arenaDM_trace {K N : ℕ} (p : FieldArena K N) : (arenaDM p).trace = 1

theorem CSD.CV.arenaDM_mk {K N : ℕ} {v : EuclideanSpace ℂ (FieldConfig K N)} (hv : v ≠ 0) : arenaDM (Projectivization.mk ℂ v hv) = dmVec v

The density of mk v is the density of v: the rep choice washes out.

Arena observables

noncomputable def CSD.CV.arenaObs {K N : ℕ} (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (p : FieldArena K N) : ℝ

An operator read as a function on the arena: arenaObs A p = re tr(ρ_p A) — the expectation of A in the ray p. This is the object that lives on the record layer's side of the category divide.

Equations

• CSD.CV.arenaObs A p = RCLike.re (CSD.CV.arenaDM p * A).trace

theorem CSD.CV.arenaObs_sub_le {K N : ℕ} [NeZero N] (A B : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (p : FieldArena K N) : |arenaObs A p - arenaObs B p| ≤ ‖A - B‖

★ The Lipschitz transport (CR-1 as the category bridge): arena observables are 1-Lipschitz in the operator norm. Every operator-norm estimate becomes a uniform estimate on arena functions through this single inequality.

Unitary kicks on the arena

theorem CSD.CV.toEuclideanLin_ne_zero {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) {v : EuclideanSpace ℂ (FieldConfig K N)} (hv : v ≠ 0) : (Matrix.toEuclideanLin ↑U) v ≠ 0

A unitary sends nonzero vectors to nonzero vectors.

noncomputable def CSD.CV.arenaKick {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (p : FieldArena K N) : FieldArena K N

A unitary as an arena self-map, constructed directly through Projectivization.mk.

Equations

• CSD.CV.arenaKick U p = Projectivization.mk ℂ ((Matrix.toEuclideanLin ↑U) (Projectivization.rep p)) ⋯

theorem CSD.CV.toEuclideanLin_coord {K N : ℕ} (M : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (v : EuclideanSpace ℂ (FieldConfig K N)) (i : FieldConfig K N) : ((Matrix.toEuclideanLin M) v).ofLp i = M.mulVec (fun (j : FieldConfig K N) => v.ofLp j) i

Coordinates of the kicked representative: matrix-vector multiplication.

theorem CSD.CV.arenaDM_kick {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (p : FieldArena K N) : arenaDM (arenaKick U p) = ↑U * arenaDM p * (↑U).conjTranspose

The kicked density is the conjugated density: ρ_{U•p} = U ρ_p Uᴴ.

theorem CSD.CV.arenaObs_kick {K N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (p : FieldArena K N) : arenaObs A (arenaKick U p) = arenaObs (heisenberg U A) p

★ The bridge identity: Schrödinger on the arena IS Heisenberg on the operator. arenaObs A (U • p) = arenaObs (U† A U) p, with heisenberg the CV chain's own Heisenberg map — so the entire CV estimate stack applies verbatim to functions on the arena.

Statics: exact locality on the arena

theorem CSD.CV.arenaObs_kick_of_disjointSupport {K N : ℕ} [NeZero N] {S T : Finset (Fin K)} (hST : Disjoint S T) {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn S A) {W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} (hW : SupportedOn T ↑W) (p : FieldArena K N) : arenaObs A (arenaKick W p) = arenaObs A p

★★ Haag–Kastler locality on the arena (statics): an arena observable of mode set S is exactly invariant under any unitary kick supported on a disjoint mode set T. Not approximately — exactly: the record layer cannot see disjointly supported interventions at all.

Dynamics: the record-arena light cone

noncomputable def CSD.CV.flowU {m : Type u_1} [Fintype m] [DecidableEq m] {S : Matrix m m ℂ} (hS : S.conjTranspose = -S) (t : ℝ) : ↥(Matrix.unitaryGroup m ℂ)

The flow as an arena kick: exp(t•S) for skew-Hermitian S, packaged as a unitary.

Equations

• CSD.CV.flowU hS t = ⟨NormedSpace.exp (t • S), ⋯⟩

theorem CSD.CV.heisenberg_flowU {K N : ℕ} {S : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hS : S.conjTranspose = -S) (t : ℝ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) : heisenberg (flowU hS t) A = heisenbergFlow S t A

The Heisenberg map of the flow kick is the CV chain's heisenbergFlow.

theorem CSD.CV.arena_lightcone {K N : ℕ} [NeZero N] {E : Finset (Fin K × Fin K)} {G : Fin K × Fin K → Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hG : ∀ e ∈ E, SupportedOn {e.1, e.2} (G e)) (hS : (∑ e ∈ E, G e).conjTranspose = -∑ e ∈ E, G e) {R Y : Finset (Fin K)} {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : SupportedOn R A) {W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)} (hW : SupportedOn Y ↑W) {d : ℕ} (hcone : Disjoint (graphBall E R d) Y) {t : ℝ} (ht : 0 ≤ t) (p : FieldArena K N) : |arenaObs A (arenaKick (flowU hS t) (arenaKick W p)) - arenaObs A (arenaKick (flowU hS t) p)| ≤ 2 * ((2 * ‖∑ e ∈ E, G e‖ * t) ^ d / ↑d.factorial) * ‖A‖

★★ The record-arena light cone — the theorem that was unstatable before the bridge. Under a graph-local skew generator, a unitary kick supported outside the graph d-ball of region R changes any region-R arena observable, after time t, by at most the Lieb-Robinson factorial tail:

|arenaObs A (flow t (kick W p)) − arenaObs A (flow t p)| ≤ 2·(2‖S‖t)^d/d!·‖A‖.

Far-away interventions cannot reach the epistemic regions faster than the cone. The proof is the bridge run end to end: both sides become Heisenberg statements (arenaObs_kick), the difference becomes a commutator through unitarity, the commutator is priced by CV-20 (norm_commutator_spatial_factorial_le), and the price crosses back to the arena through CR-1 (arenaObs_sub_le).