One arena: the field arena is Σ, up to the index of its configurations

Category: 3-Local (CV; the bridge BACKLOG #133 is about). BACKLOG #133, and the last structural gap in #131.

#131 asks for four properties "within the same dynamical model". Three of them — Born weights, record stability, no-signalling, and the CHSH violation — are statements about LF4.KSigma 16. The fourth, causal separation (TwoWingCone.lean), is a statement about FibredFieldArena 4 2. Those are the same space: FieldConfig 4 2 = Fin 4 → Fin 2 has 16 elements. But "the same space" was, until now, a remark — there was no map, because Projectivization.map has no inverse and the corpus had no equivalence of projectivizations.

Congr.lean supplies that, and this file uses it.

• configEquiv K N — FieldConfig K N ≃ Fin (N ^ K), the index change, from Fintype.equivFinOfCardEq;
• fieldSpaceEquiv K N — the induced linear isometry of the state spaces, through LinearIsometryEquiv.piLpCongrLeft, so norms and inner products are untouched;
• ★★★ arenaEquiv K N : FieldArena K N ≃ LF4.CPN (N ^ K) — the field arena and LF4's projective space are one arena, with ★ continuous_arenaEquiv and ★ measurable_arenaEquiv;
• ★★★ fibredArenaEquiv K N : FibredFieldArena K N ≃ LF4.KSigma (N ^ K) — and so are the fibred arena and Σ. The fibre needs no transport at all: CV.RecordFibre and LF4.KTorus are the same type;
• twoWingArenaEquiv : FibredFieldArena 4 2 ≃ LF4.KSigma 16 — the instance #131 needs;
• sigmaRecordStroke, sigmaFibredKick — the CV record write and the CV mode-local intervention, transported to Σ, with ★★★ sigmaRecordStroke_comm_sigmaFibredKick_twoWing: a B-wing intervention cannot steer A's record write, as a statement about Σ, at every period count.

What this buys, stated exactly

⚠️ The transported operations are defined through the equivalence, so sigmaRecordStroke_comm_sigmaFibredKick_twoWing is TwoWingCone's theorem conjugated, and no new mathematics is in it. What it buys is the one thing #131 was missing: all four properties are now statements about LF4.KSigma 16, so "within the same dynamical model" is a fact about the corpus rather than a remark about two spaces being isomorphic.

⚠️ It does not identify CV's record write with the record layer's own. recordStroke is a base-dependent shift of the fibre read through an arena observable; RecordLayer.sigmaShift is a constant translation of the record coordinate. They are different maps and this file does not claim otherwise — sigmaRecordStroke is the former, carried across.

⚠️ No measure preservation is claimed. measurable_arenaEquiv says the identification is measurable, not that it carries fsMeasure to fsMeasure or epistemicMeasure to epistemicMeasure. The transported statements here are pointwise, which is why they need nothing more; a measure-theoretic statement crossing the bridge would need that lemma first, and it is not in this file.

▸ The CV arena API was generalised 2026-10-12 (ArenaBridge.lean): arenaObs, arenaDM and arenaKick read over any finite index through GenArena, so the CV notions are now stated on Σ rather than transported wholesale. That is not done here — and the transport section below closes the row's remaining half, so "one arena" and "one API" are no longer different things. ⚠️ SupportedOn is the exception and cannot be generalised: its content is that an operator leaves the modes outside a region alone, which needs the index to be a function space. Nothing below is stated for it.

References: Congr.lean (Projectivization.congr, the piece this needed), TwoWingCone.lean (recordStroke_comm_kick_twoWing, the statement transported), FibredArenaBridge.lean (FibredFieldArena, RecordFibre, recordStroke, fibredKick), ArenaBridge.lean (FieldArena), FieldModes.lean (FieldConfig), LF4/KahlerInstance.lean (CPN, KSigma, KTorus); specs/BACKLOG.md #133, #131; specs/two-wing-experiment-scoping.md §3.

The index change

noncomputable def CSD.CV.configEquiv (K N : ℕ) : FieldConfig K N ≃ Fin (N ^ K)

The configuration space is a Fin (N ^ K): there are N ^ K ways to assign one of N levels to each of K modes.

Equations

• CSD.CV.configEquiv K N = Fintype.equivFinOfCardEq ⋯

noncomputable def CSD.CV.fieldSpaceEquiv (K N : ℕ) : EuclideanSpace ℂ (FieldConfig K N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin (N ^ K))

The induced linear isometry of state spaces. An index change is an isometry, so norms and inner products — and therefore every Born weight — are untouched by it.

Equations

• CSD.CV.fieldSpaceEquiv K N = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (CSD.CV.configEquiv K N)

One arena

noncomputable def CSD.CV.arenaEquiv (K N : ℕ) : FieldArena K N ≃ LF4.CPN (N ^ K)

★★★ The field arena and LF4's projective space are one arena. The equivalence is the index change, lifted to the projectivization by Projectivization.congr.

Equations

• CSD.CV.arenaEquiv K N = Projectivization.congr (CSD.CV.fieldSpaceEquiv K N).toLinearEquiv

theorem CSD.CV.continuous_arenaEquiv (K N : ℕ) : Continuous ⇑(arenaEquiv K N)

theorem CSD.CV.measurable_arenaEquiv (K N : ℕ) : Measurable ⇑(arenaEquiv K N)

noncomputable def CSD.CV.fibredArenaEquiv (K N : ℕ) : FibredFieldArena K N ≃ LF4.KSigma (N ^ K)

★★★ And the fibred arena is Σ. The fibre needs no transport whatever: CV.RecordFibre and LF4.KTorus are the same type, both AddCircle 1 × AddCircle 1.

Equations

• CSD.CV.fibredArenaEquiv K N = (CSD.CV.arenaEquiv K N).prodCongr (Equiv.refl CSD.CV.RecordFibre)

theorem CSD.CV.measurable_fibredArenaEquiv (K N : ℕ) : Measurable ⇑(fibredArenaEquiv K N)

noncomputable def CSD.CV.twoWingArenaEquiv : FibredFieldArena 4 2 ≃ LF4.KSigma 16

The two-wing experiment's arena: FieldConfig 4 2 has 2 ^ 4 = 16 configurations, so the CV arena of four modes at two levels is Σ = ℂℙ¹⁵ × T².

Equations

• CSD.CV.twoWingArenaEquiv = CSD.CV.fibredArenaEquiv 4 2

The cone theorems, as statements about Σ

noncomputable def CSD.CV.sigmaRecordStroke (A : Matrix (FieldConfig 4 2) (FieldConfig 4 2) ℂ) (g : ℝ → RecordFibre) (y : LF4.KSigma 16) : LF4.KSigma 16

The CV record write, transported to Σ.

Equations

• CSD.CV.sigmaRecordStroke A g y = CSD.CV.twoWingArenaEquiv (CSD.CV.recordStroke A g (CSD.CV.twoWingArenaEquiv.symm y))

noncomputable def CSD.CV.sigmaFibredKick (W : ↥(Matrix.unitaryGroup (FieldConfig 4 2) ℂ)) (y : LF4.KSigma 16) : LF4.KSigma 16

A CV mode-local intervention, transported to Σ.

Equations

• CSD.CV.sigmaFibredKick W y = CSD.CV.twoWingArenaEquiv (CSD.CV.fibredKick W (CSD.CV.twoWingArenaEquiv.symm y))

theorem CSD.CV.sigmaRecordStroke_comm_sigmaFibredKick_twoWing (τ lam : ℝ) (gc : Fin 4 × Fin 4 → Fin 2 → Fin 2 → ℝ) {A : Matrix (FieldConfig 4 2) (FieldConfig 4 2) ℂ} (hA : SupportedOn wingAModes A) {W : ↥(Matrix.unitaryGroup (FieldConfig 4 2) ℂ)} (hW : SupportedOn wingBModes ↑W) (n : ℕ) (g : ℝ → RecordFibre) (y : LF4.KSigma 16) : sigmaRecordStroke (heisenberg (graphInteractingU 4 2 τ lam twoWingGraph gc ^ n) A) g (sigmaFibredKick W y) = sigmaFibredKick W (sigmaRecordStroke (heisenberg (graphInteractingU 4 2 τ lam twoWingGraph gc ^ n) A) g y)

★★★ A B-wing intervention cannot steer A's record write — on Σ. This is recordStroke_comm_kick_twoWing carried across the arena identification, and it is the statement #131 needed: the causal-separation property now lives on LF4.KSigma 16, the same space as the Born weights, the record stability bound and the CHSH violation.

⚠️ The transported operations are defined through twoWingArenaEquiv, so this contains no new mathematics. What it establishes is that the four properties of #131 are about one space.

Transport along an index equivalence

#133's second half, and the piece that turns "one arena" into "one reading". ArenaBridge.lean's GenArena made the CV vocabulary index-generic, so a reading can be stated over either index. What follows lets it be carried: an index equivalence transports rays (idxArenaEquiv), operators (Matrix.reindex) and unitaries (idxUnitary), and the arena observable is invariant under the transport, so a number read on one arena is the same number on the other rather than a number related to it.

The specific equivalence of the previous section is an instance of this one on the nose: arenaEquiv K N = idxArenaEquiv (configEquiv K N) by rfl (★ arenaEquiv_eq_idxArenaEquiv), which is what makes the generic lemmas apply to the field-arena-is-Σ identification without a second construction.

noncomputable def CSD.CV.idxSpaceEquiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) : EuclideanSpace ℂ ι ≃ₗᵢ[ℂ] EuclideanSpace ℂ κ

The index change as a linear isometry of state spaces, over an arbitrary finite index.

Equations

• CSD.CV.idxSpaceEquiv e = LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e

@[simp]

theorem CSD.CV.idxSpaceEquiv_apply {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (v : EuclideanSpace ℂ ι) (k : κ) : ((idxSpaceEquiv e) v).ofLp k = v.ofLp (e.symm k)

theorem CSD.CV.idxSpaceEquiv_ne_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) {v : EuclideanSpace ℂ ι} (hv : v ≠ 0) : (idxSpaceEquiv e) v ≠ 0

noncomputable def CSD.CV.idxArenaEquiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) : GenArena ι ≃ GenArena κ

★★★ The arena transported along an index equivalence.

Equations

• CSD.CV.idxArenaEquiv e = Projectivization.congr (CSD.CV.idxSpaceEquiv e).toLinearEquiv

theorem CSD.CV.idxArenaEquiv_mk {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) {v : EuclideanSpace ℂ ι} (hv : v ≠ 0) : (idxArenaEquiv e) (Projectivization.mk ℂ v hv) = Projectivization.mk ℂ ((idxSpaceEquiv e) v) ⋯

theorem CSD.CV.idxArenaEquiv_eq_mk {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (p : GenArena ι) : (idxArenaEquiv e) p = Projectivization.mk ℂ ((idxSpaceEquiv e) (Projectivization.rep p)) ⋯

The transported ray, through the canonical representative.

def CSD.CV.idxUnitary {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (U : ↥(Matrix.unitaryGroup ι ℂ)) : ↥(Matrix.unitaryGroup κ ℂ)

The transported unitary: relabel the matrix, which stays unitary.

Equations

• CSD.CV.idxUnitary e U = ⟨(Matrix.reindex e e) ↑U, ⋯⟩

@[simp]

theorem CSD.CV.idxUnitary_val {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (U : ↥(Matrix.unitaryGroup ι ℂ)) : ↑(idxUnitary e U) = (Matrix.reindex e e) ↑U

The density, the observable and the kick

theorem CSD.CV.unitVec_idxSpaceEquiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (v : EuclideanSpace ℂ ι) (k : κ) : unitVec ((idxSpaceEquiv e) v) k = unitVec v (e.symm k)

The unit representative is relabelled, not rescaled: an index change is an isometry, so the normalisation is the same number on both sides.

theorem CSD.CV.dmVec_idxSpaceEquiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (v : EuclideanSpace ℂ ι) : dmVec ((idxSpaceEquiv e) v) = (Matrix.reindex e e) (dmVec v)

★★ The rank-one density is reindexed.

theorem CSD.CV.arenaDM_idxArenaEquiv {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (p : GenArena ι) : arenaDM ((idxArenaEquiv e) p) = (Matrix.reindex e e) (arenaDM p)

★★ The density of a transported ray is the reindexed density.

theorem CSD.CV.arenaObs_reindex {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (A : Matrix ι ι ℂ) (p : GenArena ι) : arenaObs ((Matrix.reindex e e) A) ((idxArenaEquiv e) p) = arenaObs A p

★★★ Arena observables transport. Reading the reindexed operator on the transported ray gives the same real number, so a CV reading is carried between arenas rather than merely stated over either. The proof is the two facts a relabelling has: it is multiplicative (Matrix.reindex_mul) and it fixes the trace (Matrix.trace_reindex).

theorem CSD.CV.toEuclideanLin_reindex {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (M : Matrix ι ι ℂ) (v : EuclideanSpace ℂ ι) : (Matrix.toEuclideanLin ((Matrix.reindex e e) M)) ((idxSpaceEquiv e) v) = (idxSpaceEquiv e) ((Matrix.toEuclideanLin M) v)

The reindexed matrix acting on a transported vector is the transport of the action.

theorem CSD.CV.arenaKick_reindex {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (U : ↥(Matrix.unitaryGroup ι ℂ)) (p : GenArena ι) : arenaKick (idxUnitary e U) ((idxArenaEquiv e) p) = (idxArenaEquiv e) (arenaKick U p)

★★★ Unitary kicks transport. The relabelled kick on the transported ray is the transport of the kick, so a CV intervention and its image on the other arena are one map read two ways.

The field arena, through the generic transport

The previous section's arenaEquiv is the generic one at the configuration index, so the transport lemmas apply to it with no second construction.

theorem CSD.CV.arenaEquiv_eq_idxArenaEquiv (K N : ℕ) : arenaEquiv K N = idxArenaEquiv (configEquiv K N)

★ The two halves of #133 are one construction.

theorem CSD.CV.arenaObs_arenaEquiv (K N : ℕ) (A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ) (p : FieldArena K N) : arenaObs ((Matrix.reindex (configEquiv K N) (configEquiv K N)) A) ((arenaEquiv K N) p) = arenaObs A p

★★★ A CV reading, carried to Σ. The expectation of a field operator in a field ray is the expectation of the relabelled operator in the corresponding ray of LF4.CPN (N ^ K) — the same real number, not a number related to it by an unproved identification.

theorem CSD.CV.arenaKick_arenaEquiv (K N : ℕ) (U : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) (p : FieldArena K N) : arenaKick (idxUnitary (configEquiv K N) U) ((arenaEquiv K N) p) = (arenaEquiv K N) (arenaKick U p)

★★ And a CV intervention, carried to Σ.