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

Category: 3-Local (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. mode-disjoint commutation (CV-8; the Haag–Kastler analogue on mode sets, not the axiom — see CV/ModeLocality.lean), 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. Matrix.norm_toEuclideanLin_of_isom restates LF5's Matrix.norm_toEuclideanLin_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.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 index-generic layer

▸ Generalised 2026-10-12 (BACKLOG #133). Everything from here to the statics section is about an arbitrary finite index ι, not about FieldConfig K N. The mathematics never used the mode structure — only that the index is a finite type with decidable equality — and keeping it special-cased is what made FieldArena K N and LF4.CPN M two different arenas with no shared vocabulary. GenArena ι is the generic arena and FieldArena K N is its instance at the configuration space, so every statement elsewhere in the corpus reads unchanged.

⚠️ SupportedOn is not here and cannot be: its content is that an operator does not move the modes outside a region, which is a statement about the index being a function space. The statics and light-cone sections below therefore stay FieldConfig-indexed, and that is not a gap.

@[reducible, inline]

abbrev CSD.CV.GenArena (ι : Type u_1) : Type u_1

The generic arena: the projectivisation of a finite-dimensional state space over any finite index. FieldArena K N is this at ι := FieldConfig K N.

Equations

• CSD.CV.GenArena ι = Projectivization ℂ (EuclideanSpace ℂ ι)

The rank-one density of a ray

noncomputable def CSD.CV.unitVec {ι : Type u_1} [Fintype ι] (v : EuclideanSpace ℂ ι) : ι → ℂ

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 {ι : Type u_1} [Fintype ι] (v : EuclideanSpace ℂ ι) : Matrix ι ι ℂ

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 {ι : Type u_1} [Fintype ι] (v : EuclideanSpace ℂ ι) (i j : ι) : dmVec v i j = unitVec v i * star (unitVec v j)

theorem CSD.CV.dmVec_posSemidef {ι : Type u_1} [Fintype ι] (v : EuclideanSpace ℂ ι) : (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' {ι : Type u_1} [Fintype ι] {v : EuclideanSpace ℂ ι} (i j : ι) : 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 {ι : Type u_1} [Fintype ι] {v : EuclideanSpace ℂ ι} (hv : v ≠ 0) : (dmVec v).trace = 1

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

theorem CSD.CV.dmVec_smul {ι : Type u_1} [Fintype ι] {c : ℂ} (hc : c ≠ 0) {v : EuclideanSpace ℂ ι} (hv : v ≠ 0) : dmVec (c • v) = dmVec v

Scale invariance: the density depends only on the ray.

noncomputable def CSD.CV.arenaDM {ι : Type u_1} [Fintype ι] (p : GenArena ι) : Matrix ι ι ℂ

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 {ι : Type u_1} [Fintype ι] (p : GenArena ι) : (arenaDM p).PosSemidef

theorem CSD.CV.arenaDM_trace {ι : Type u_1} [Fintype ι] (p : GenArena ι) : (arenaDM p).trace = 1

theorem CSD.CV.arenaDM_mk {ι : Type u_1} [Fintype ι] {v : EuclideanSpace ℂ ι} (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 {ι : Type u_1} [Fintype ι] (A : Matrix ι ι ℂ) (p : GenArena ι) : ℝ

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 {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (A B : Matrix ι ι ℂ) (p : GenArena ι) : |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

noncomputable def CSD.CV.arenaKick {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (p : GenArena ι) : GenArena ι

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.arenaKick_mk {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) {v : EuclideanSpace ℂ ι} (hv : v ≠ 0) : arenaKick U (Projectivization.mk ℂ v hv) = Projectivization.mk ℂ ((Matrix.toEuclideanLin ↑U) v) ⋯

The kick of mk v is the ray of U v: the rep choice washes out, exactly as it does for arenaDM_mk. Generalised from CompositeArena.lean's FieldConfig-indexed copy 2026-10-12 (#133), which had recorded that it was "general-K API, placed here as its first consumer".

theorem CSD.CV.toEuclideanLin_coord {ι : Type u_1} [Fintype ι] [DecidableEq ι] (M : Matrix ι ι ℂ) (v : EuclideanSpace ℂ ι) (i : ι) : ((Matrix.toEuclideanLin M) v).ofLp i = M.mulVec (fun (j : ι) => v.ofLp j) i

Coordinates of the kicked representative: matrix-vector multiplication.

theorem CSD.CV.arenaDM_kick {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (p : GenArena ι) : 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_conj {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : ↥(Matrix.unitaryGroup ι ℂ)) (A : Matrix ι ι ℂ) (p : GenArena ι) : arenaObs A (arenaKick U p) = arenaObs (star ↑U * A * ↑U) p

★ The bridge identity, index-generically: Schrödinger on the arena IS conjugation on the operator. Stated with the conjugation written out, because heisenberg itself is FieldConfig-indexed (its companion lemmas are about mode support); arenaObs_kick below is this in heisenberg form.

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

★★ Mode-disjoint commutation on the arena (statics; the Haag–Kastler analogue, on mode sets rather than spacetime regions): 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).