P2: the composite arena — two sectors compose by mode concatenation, and the algebra forcing transports

Category: CV (continuous variables — composition of sectors at the arena level; eft-pillars-plan.md P2).

Glossary: https://glossary.constraintsurfacedynamics.com/no-signalling/ and https://glossary.constraintsurfacedynamics.com/bell-not-join/ Plain-language, CSD-role and formal statements of no-signalling and the Bell-is-not-a-join theorem, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

The algebra half of composition is landed: compositeAlgReconstruction (SigmaLayer/TensorReconstruction.lean) forces any composite carrying commuting, generating local matrix algebras to BE the tensor product. P2 asked for the arena-side analogue: what the composite of two ontic sectors is, and whether that forcing transports. Scoped first in specs/composite-arena-plan.md.

What the composite is: mode concatenation. The composite of a K₁-mode sector and a K₂-mode sector is the (K₁+K₂)-mode sector — an arena the corpus already has, not a new species. configSplit splits a joint configuration into its two mode blocks, and everything is read through it:

• sectorJoin / arenaJoin — the Kronecker vector in field coordinates (norm_sectorJoin : ‖u ⊗ v‖ = ‖u‖·‖v‖) and the induced Segre map on rays, FieldArena K₁ N → FieldArena K₂ N → FieldArena (K₁+K₂) N.
• leftOp / rightOp — the two local operator algebras (reindexed A ⊗ₖ 1, 1 ⊗ₖ B), with leftHom / rightHom the algebra-hom packagings, and ★ leftOp_supportedOn / rightOp_supportedOn: the local subalgebras are mode-local (SupportedOn their blocks), so every P1 theorem — statics, cones, strokes — applies to the composite arena with zero new proofs.
• Transport along the join: arenaDM_join (ρ_{p⊗q} = ρ_p ⊗ₖ ρ_q), ★ arenaObs_join_left / arenaObs_join_right (marginal readings exact), ★ arenaObs_join_mul (joint expectations of product observables factor — local tomography read on the arena), ★ arenaKick_join (product unitaries restrict along the join to the product action).
• ★★ composite_no_signalling — no-signalling on the composite arena, exactly, for ALL states: a kick built from a right-sector unitary leaves every left-sector arena observable invariant — on entangled points too, because it is an instance of P1's arenaObs_kick_of_disjointSupport, not a consequence of the join.
• ★★ bell_not_join — entanglement is real at the arena level: for N ≥ 2 the Bell ray is not in the image of arenaJoin (exists_bell_witness makes it non-vacuous). The composite arena is strictly larger than the pair of components — the arena-side signature of ⊗ versus ×.
• ★★ composite_generate + compositeArenaForced — the algebra forcing transports: the composite arena's own operator algebra, with its two mode-local subalgebras, satisfies the reconstruction's premises (they commute, leftOp_comm_rightOp, and generate, composite_generate), so the landed compositeAlgReconstruction applies and forces Matrix C₁ ⊗[ℂ] Matrix C₂ ≃ₐ Matrix C₁₂, with compositeArenaForced_tmul pinning the map as A ⊗ₜ B ↦ leftOp A · rightOp B. Consumed from the landed theorem, not re-proved.

⚠️ Honest scope: homogeneous field sectors — both factors share the level count N and compose mode-disjointly, the field-native case the CV chain and P1's arenas are built from. Heterogeneous composites (N₁ ≠ N₂, non-field sectors) are not claimed here; they need the arena API generalised over its index type (rule-of-two note: generalise ArenaBridge when next touched). The fibre side of the composite is the product of record media, with per-sector strokes covered by P1's generic machinery through leftOp_supportedOn; and composite mixed-state theory (reduced states of entangled rays) is CV-26's coarse-graining territory, not this pillar's.

References

specs/composite-arena-plan.md (scoping); specs/eft-pillars-plan.md (P2); specs/future-work.md; SigmaLayer/TensorReconstruction.lean (compositeAlgReconstruction, consumed); SigmaLayer/TensorGeneration.lean (single_eq_smul; the Fin-indexed generation this re-lands arena-natively); CV/ArenaBridge.lean (arenaDM, arenaObs, arenaKick, the P1 statics); CV/ModeLocality.lean (SupportedOn).

Splitting a joint configuration into its mode blocks

def CSD.CV.configSplit {K₁ K₂ N : ℕ} : FieldConfig (K₁ + K₂) N ≃ FieldConfig K₁ N × FieldConfig K₂ N

The mode split: a (K₁+K₂)-mode configuration is a pair of a K₁-mode and a K₂-mode configuration. The composite arena is read through this equivalence.

Equations

• One or more equations did not get rendered due to their size.

def CSD.CV.leftModes (K₁ K₂ : ℕ) : Finset (Fin (K₁ + K₂))

The left mode block of the composite.

Equations

• CSD.CV.leftModes K₁ K₂ = Finset.image (Fin.castAdd K₂) Finset.univ

def CSD.CV.rightModes (K₁ K₂ : ℕ) : Finset (Fin (K₁ + K₂))

The right mode block of the composite.

Equations

• CSD.CV.rightModes K₁ K₂ = Finset.image (Fin.natAdd K₁) Finset.univ

theorem CSD.CV.mem_leftModes {K₁ K₂ : ℕ} {k : Fin (K₁ + K₂)} : k ∈ leftModes K₁ K₂ ↔ ∃ (i : Fin K₁), Fin.castAdd K₂ i = k

theorem CSD.CV.mem_rightModes {K₁ K₂ : ℕ} {k : Fin (K₁ + K₂)} : k ∈ rightModes K₁ K₂ ↔ ∃ (j : Fin K₂), Fin.natAdd K₁ j = k

theorem CSD.CV.natAdd_notMem_leftModes {K₁ K₂ : ℕ} (j : Fin K₂) : Fin.natAdd K₁ j ∉ leftModes K₁ K₂

theorem CSD.CV.castAdd_notMem_rightModes {K₁ K₂ : ℕ} (i : Fin K₁) : Fin.castAdd K₂ i ∉ rightModes K₁ K₂

theorem CSD.CV.disjoint_leftModes_rightModes {K₁ K₂ : ℕ} : Disjoint (leftModes K₁ K₂) (rightModes K₁ K₂)

The two mode blocks are disjoint: left values are < K₁, right values are ≥ K₁.

The join: the Kronecker vector and the Segre map

noncomputable def CSD.CV.sectorJoin {K₁ K₂ N : ℕ} (u : EuclideanSpace ℂ (FieldConfig K₁ N)) (v : EuclideanSpace ℂ (FieldConfig K₂ N)) : EuclideanSpace ℂ (FieldConfig (K₁ + K₂) N)

The sector join: the Kronecker product of two field vectors, in field coordinates.

Equations

• CSD.CV.sectorJoin u v = WithLp.toLp 2 fun (c : CSD.CV.FieldConfig (K₁ + K₂) N) => u.ofLp (CSD.CV.configSplit c).1 * v.ofLp (CSD.CV.configSplit c).2

theorem CSD.CV.sectorJoin_apply {K₁ K₂ N : ℕ} (u : EuclideanSpace ℂ (FieldConfig K₁ N)) (v : EuclideanSpace ℂ (FieldConfig K₂ N)) (c : FieldConfig (K₁ + K₂) N) : (sectorJoin u v).ofLp c = u.ofLp (configSplit c).1 * v.ofLp (configSplit c).2

theorem CSD.CV.euclid_congrFun {ι : Type u_1} [Fintype ι] {x y : EuclideanSpace ℂ ι} (h : x = y) (i : ι) : x.ofLp i = y.ofLp i

Pointwise reading of an equality of Euclidean vectors (congrFun through the WithLp structure).

theorem CSD.CV.sectorJoin_smul_smul {K₁ K₂ N : ℕ} (a b : ℂ) (u : EuclideanSpace ℂ (FieldConfig K₁ N)) (v : EuclideanSpace ℂ (FieldConfig K₂ N)) : sectorJoin (a • u) (b • v) = (a * b) • sectorJoin u v

The join is bilinear on scalars: (a•u) ⊗ (b•v) = (ab) • (u ⊗ v).

theorem CSD.CV.norm_sectorJoin {K₁ K₂ N : ℕ} (u : EuclideanSpace ℂ (FieldConfig K₁ N)) (v : EuclideanSpace ℂ (FieldConfig K₂ N)) : ‖sectorJoin u v‖ = ‖u‖ * ‖v‖

The join norm is multiplicative: ‖u ⊗ v‖ = ‖u‖·‖v‖.

theorem CSD.CV.sectorJoin_ne_zero {K₁ K₂ N : ℕ} {u : EuclideanSpace ℂ (FieldConfig K₁ N)} {v : EuclideanSpace ℂ (FieldConfig K₂ N)} (hu : u ≠ 0) (hv : v ≠ 0) : sectorJoin u v ≠ 0

The join of nonzero vectors is nonzero.

noncomputable def CSD.CV.arenaJoin {K₁ K₂ N : ℕ} (p : FieldArena K₁ N) (q : FieldArena K₂ N) : FieldArena (K₁ + K₂) N

The Segre map: the composite ray of a pair of sector rays.

Equations

• CSD.CV.arenaJoin p q = Projectivization.mk ℂ (CSD.CV.sectorJoin (Projectivization.rep p) (Projectivization.rep q)) ⋯

theorem CSD.CV.arenaJoin_mk {K₁ K₂ N : ℕ} {u : EuclideanSpace ℂ (FieldConfig K₁ N)} (hu : u ≠ 0) {v : EuclideanSpace ℂ (FieldConfig K₂ N)} (hv : v ≠ 0) : arenaJoin (Projectivization.mk ℂ u hu) (Projectivization.mk ℂ v hv) = Projectivization.mk ℂ (sectorJoin u v) ⋯

The Segre map on representatives: the rep choices wash out.

The local operator algebras

noncomputable def CSD.CV.compositeReindex {K₁ K₂ N : ℕ} : Matrix (FieldConfig K₁ N × FieldConfig K₂ N) (FieldConfig K₁ N × FieldConfig K₂ N) ℂ ≃ₐ[ℂ] Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

The composite reindex: matrices over the pair of configuration spaces, read as matrices over the joint configuration space. An algebra equivalence.

Equations

• CSD.CV.compositeReindex = Matrix.reindexAlgEquiv ℂ ℂ CSD.CV.configSplit.symm

theorem CSD.CV.compositeReindex_apply {K₁ K₂ N : ℕ} (M : Matrix (FieldConfig K₁ N × FieldConfig K₂ N) (FieldConfig K₁ N × FieldConfig K₂ N) ℂ) (c d : FieldConfig (K₁ + K₂) N) : compositeReindex M c d = M (configSplit c) (configSplit d)

theorem CSD.CV.compositeReindex_conjTranspose {K₁ K₂ N : ℕ} (M : Matrix (FieldConfig K₁ N × FieldConfig K₂ N) (FieldConfig K₁ N × FieldConfig K₂ N) ℂ) : (compositeReindex M).conjTranspose = compositeReindex M.conjTranspose

theorem CSD.CV.trace_compositeReindex {K₁ K₂ N : ℕ} (M : Matrix (FieldConfig K₁ N × FieldConfig K₂ N) (FieldConfig K₁ N × FieldConfig K₂ N) ℂ) : (compositeReindex M).trace = M.trace

Traces are preserved by the composite reindex.

noncomputable def CSD.CV.leftOp {K₁ K₂ N : ℕ} (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) : Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

A left-sector operator acting on the composite: A ⊗ₖ 1, reindexed.

Equations

• CSD.CV.leftOp A = CSD.CV.compositeReindex (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A 1)

noncomputable def CSD.CV.rightOp {K₁ K₂ N : ℕ} (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) : Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

A right-sector operator acting on the composite: 1 ⊗ₖ B, reindexed.

Equations

• CSD.CV.rightOp B = CSD.CV.compositeReindex (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 B)

theorem CSD.CV.leftOp_mul_rightOp {K₁ K₂ N : ℕ} (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) : leftOp A * rightOp B = compositeReindex (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B)

The local products assemble to the reindexed Kronecker product.

theorem CSD.CV.leftOp_comm_rightOp {K₁ K₂ N : ℕ} (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) : Commute (leftOp A) (rightOp B)

★ The two local algebras commute — locality of the composite.

noncomputable def CSD.CV.kronLeftHom {K₁ K₂ N : ℕ} : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ →ₐ[ℂ] Matrix (FieldConfig K₁ N × FieldConfig K₂ N) (FieldConfig K₁ N × FieldConfig K₂ N) ℂ

A ↦ A ⊗ₖ 1 as an algebra hom into the pair-indexed algebra.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.CV.kronRightHom {K₁ K₂ N : ℕ} : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ →ₐ[ℂ] Matrix (FieldConfig K₁ N × FieldConfig K₂ N) (FieldConfig K₁ N × FieldConfig K₂ N) ℂ

B ↦ 1 ⊗ₖ B as an algebra hom into the pair-indexed algebra.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.CV.leftHom {K₁ K₂ N : ℕ} : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ →ₐ[ℂ] Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

The left embedding as an algebra hom.

Equations

• CSD.CV.leftHom = (↑CSD.CV.compositeReindex).comp CSD.CV.kronLeftHom

noncomputable def CSD.CV.rightHom {K₁ K₂ N : ℕ} : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ →ₐ[ℂ] Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

The right embedding as an algebra hom.

Equations

• CSD.CV.rightHom = (↑CSD.CV.compositeReindex).comp CSD.CV.kronRightHom

theorem CSD.CV.leftHom_apply {K₁ K₂ N : ℕ} (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) : leftHom A = leftOp A

theorem CSD.CV.rightHom_apply {K₁ K₂ N : ℕ} (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) : rightHom B = rightOp B

The local algebras are mode-local: P1 machinery applies for free

theorem CSD.CV.leftOp_supportedOn {K₁ K₂ N : ℕ} (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) : SupportedOn (leftModes K₁ K₂) (leftOp A)

★ The left algebra is supported on the left mode block. With this, every P1 statement — exact statics, the Lieb-Robinson cone, record strokes — applies to composite-arena local observables with zero new proofs.

theorem CSD.CV.rightOp_supportedOn {K₁ K₂ N : ℕ} (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) : SupportedOn (rightModes K₁ K₂) (rightOp B)

★ The right algebra is supported on the right mode block.

State transport: the density of a join is the Kronecker density

theorem CSD.CV.arenaDM_eq_dmVec_rep {K N : ℕ} (p : FieldArena K N) : arenaDM p = dmVec (Projectivization.rep p)

Bridge to the canonical representative (arenaDM is definitionally dmVec ∘ rep, restated as a lemma for cross-module use).

theorem CSD.CV.arenaDM_join {K₁ K₂ N : ℕ} (p : FieldArena K₁ N) (q : FieldArena K₂ N) : arenaDM (arenaJoin p q) = compositeReindex (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (arenaDM p) (arenaDM q))

The density of a join is the Kronecker product of the densities: ρ_{p⊗q} = ρ_p ⊗ₖ ρ_q, read on the composite index.

Observable transport: marginals are exact, products factor

theorem CSD.CV.arenaObs_join_left {K₁ K₂ N : ℕ} (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (p : FieldArena K₁ N) (q : FieldArena K₂ N) : arenaObs (leftOp A) (arenaJoin p q) = arenaObs A p

★ The marginal reading is exact: a left-sector observable read on a join sees exactly the left component. No-signalling on product states, with no hypotheses on A.

theorem CSD.CV.arenaObs_join_right {K₁ K₂ N : ℕ} (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) (p : FieldArena K₁ N) (q : FieldArena K₂ N) : arenaObs (rightOp B) (arenaJoin p q) = arenaObs B q

★ The symmetric right marginal.

theorem CSD.CV.trace_arenaDM_mul_real {K N : ℕ} (p : FieldArena K N) {A : Matrix (FieldConfig K N) (FieldConfig K N) ℂ} (hA : A.conjTranspose = A) : (arenaDM p * A).trace.im = 0

The expectation of a Hermitian observable in any ray is real.

theorem CSD.CV.arenaObs_join_mul {K₁ K₂ N : ℕ} {A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ} (hA : A.conjTranspose = A) (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) (p : FieldArena K₁ N) (q : FieldArena K₂ N) : arenaObs (leftOp A * rightOp B) (arenaJoin p q) = arenaObs A p * arenaObs B q

★ Local tomography on the arena: the joint expectation of a product of local observables factors into the product of local expectations, on every join. (A Hermitian makes its expectation real, which is what lets the real parts factor.)

Dynamics transport: product unitaries restrict along the join

noncomputable def CSD.CV.joinU {K₁ K₂ N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K₁ N) ℂ)) (V : ↥(Matrix.unitaryGroup (FieldConfig K₂ N) ℂ)) : ↥(Matrix.unitaryGroup (FieldConfig (K₁ + K₂) N) ℂ)

The product unitary on the composite: U ⊗ₖ V, reindexed.

Equations

• CSD.CV.joinU U V = ⟨CSD.CV.compositeReindex (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ↑U ↑V), ⋯⟩

theorem CSD.CV.arenaKick_mk {K N : ℕ} (W : ↥(Matrix.unitaryGroup (FieldConfig K N) ℂ)) {v : EuclideanSpace ℂ (FieldConfig K N)} (hv : v ≠ 0) : arenaKick W (Projectivization.mk ℂ v hv) = Projectivization.mk ℂ ((Matrix.toEuclideanLin ↑W) v) ⋯

Kicks on representatives: the rep choice washes out (general-K API, placed here as its first consumer; ArenaBridge inlines the same dance).

theorem CSD.CV.toEuclideanLin_joinU {K₁ K₂ N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K₁ N) ℂ)) (V : ↥(Matrix.unitaryGroup (FieldConfig K₂ N) ℂ)) (u : EuclideanSpace ℂ (FieldConfig K₁ N)) (v : EuclideanSpace ℂ (FieldConfig K₂ N)) : (Matrix.toEuclideanLin ↑(joinU U V)) (sectorJoin u v) = sectorJoin ((Matrix.toEuclideanLin ↑U) u) ((Matrix.toEuclideanLin ↑V) v)

The product unitary acts on join vectors as the pair of local actions.

theorem CSD.CV.arenaKick_join {K₁ K₂ N : ℕ} (U : ↥(Matrix.unitaryGroup (FieldConfig K₁ N) ℂ)) (V : ↥(Matrix.unitaryGroup (FieldConfig K₂ N) ℂ)) (p : FieldArena K₁ N) (q : FieldArena K₂ N) : arenaKick (joinU U V) (arenaJoin p q) = arenaJoin (arenaKick U p) (arenaKick V q)

★ Dynamics restrict along the join: the product unitary's kick on the composite arena is the pair of local kicks.

noncomputable def CSD.CV.rightU {K₁ K₂ N : ℕ} (V : ↥(Matrix.unitaryGroup (FieldConfig K₂ N) ℂ)) : ↥(Matrix.unitaryGroup (FieldConfig (K₁ + K₂) N) ℂ)

A right-sector unitary, acting on the composite. Its matrix is the rightOp of the sector unitary's matrix.

Equations

• CSD.CV.rightU V = CSD.CV.joinU 1 V

theorem CSD.CV.rightU_val {K₁ K₂ N : ℕ} (V : ↥(Matrix.unitaryGroup (FieldConfig K₂ N) ℂ)) : ↑(rightU V) = rightOp ↑V

theorem CSD.CV.composite_no_signalling {K₁ K₂ N : ℕ} [NeZero N] (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (V : ↥(Matrix.unitaryGroup (FieldConfig K₂ N) ℂ)) (x : FieldArena (K₁ + K₂) N) : arenaObs (leftOp A) (arenaKick (rightU V) x) = arenaObs (leftOp A) x

★★ No-signalling on the composite arena — exactly, and for ALL states. A kick built from a right-sector unitary leaves every left-sector arena observable invariant, on every point of the composite arena, entangled points included. This is an instance of P1's exact statics (arenaObs_kick_of_disjointSupport) through the mode-locality of the two subalgebras — not a consequence of the join, which is why it needs no product form on the state.

Entanglement: the composite arena is strictly larger than the pair

noncomputable def CSD.CV.bellVec {K₁ K₂ N : ℕ} (x₀ x₁ : FieldConfig K₁ N) (y₀ y₁ : FieldConfig K₂ N) : EuclideanSpace ℂ (FieldConfig (K₁ + K₂) N)

The Bell vector over a pair of patterns per sector: equal weight on the two aligned configuration pairs, zero elsewhere.

Equations

• CSD.CV.bellVec x₀ x₁ y₀ y₁ = WithLp.toLp 2 fun (c : CSD.CV.FieldConfig (K₁ + K₂) N) => if CSD.CV.configSplit c = (x₀, y₀) ∨ CSD.CV.configSplit c = (x₁, y₁) then 1 else 0

theorem CSD.CV.bellVec_apply {K₁ K₂ N : ℕ} (x₀ x₁ : FieldConfig K₁ N) (y₀ y₁ : FieldConfig K₂ N) (c : FieldConfig (K₁ + K₂) N) : (bellVec x₀ x₁ y₀ y₁).ofLp c = if configSplit c = (x₀, y₀) ∨ configSplit c = (x₁, y₁) then 1 else 0

theorem CSD.CV.bellVec_ne_zero {K₁ K₂ N : ℕ} (x₀ x₁ : FieldConfig K₁ N) (y₀ y₁ : FieldConfig K₂ N) : bellVec x₀ x₁ y₀ y₁ ≠ 0

theorem CSD.CV.bell_not_join {K₁ K₂ N : ℕ} {x₀ x₁ : FieldConfig K₁ N} (hx : x₀ ≠ x₁) {y₀ y₁ : FieldConfig K₂ N} (hy : y₀ ≠ y₁) (p : FieldArena K₁ N) (q : FieldArena K₂ N) : arenaJoin p q ≠ Projectivization.mk ℂ (bellVec x₀ x₁ y₀ y₁) ⋯

★★ Entanglement is real at the arena level: the Bell ray over two distinct patterns per sector is NOT a join. The composite arena is strictly larger than the pair of component arenas — the arena-side signature of the tensor product against the Cartesian one.

theorem CSD.CV.exists_bell_witness {K₁ K₂ N : ℕ} [NeZero K₁] [NeZero K₂] (hN : 2 ≤ N) : ∃ (x₀ : FieldConfig K₁ N) (x₁ : FieldConfig K₁ N) (y₀ : FieldConfig K₂ N) (y₁ : FieldConfig K₂ N), x₀ ≠ x₁ ∧ y₀ ≠ y₁

Two distinct patterns exist in each sector as soon as N ≥ 2 (constant configurations at two distinct levels), so bell_not_join is non-vacuous: entangled rays exist on every composite arena with at least two levels.

The transport: the algebra forcing lands on the composite arena

theorem CSD.CV.single_kronecker_single {K₁ K₂ N : ℕ} (a₁ b₁ : FieldConfig K₁ N) (a₂ b₂ : FieldConfig K₂ N) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Matrix.single a₁ b₁ 1) (Matrix.single a₂ b₂ 1) = Matrix.single (a₁, a₂) (b₁, b₂) 1

Kronecker of unit basis matrices is the joint unit basis matrix (the index-generic form of SigmaLayer.single_prod).

theorem CSD.CV.compositeReindex_single {K₁ K₂ N : ℕ} (x y : FieldConfig K₁ N × FieldConfig K₂ N) : compositeReindex (Matrix.single x y 1) = Matrix.single (configSplit.symm x) (configSplit.symm y) 1

The composite reindex of a unit basis matrix.

theorem CSD.CV.composite_generate {K₁ K₂ N : ℕ} : Algebra.adjoin ℂ (Set.range ⇑leftHom ∪ Set.range ⇑rightHom) = ⊤

★★ The composite arena's local algebras generate — the second premise of the reconstruction, proved arena-natively: every joint operator is a linear combination of products leftOp E · rightOp E' of unit local observables. The composite algebra carries nothing beyond the local algebras and their products.

theorem CSD.CV.fieldConfig_nonempty (N : ℕ) [NeZero N] (K : ℕ) : Nonempty (FieldConfig K N)

Field configuration spaces are nonempty once there is at least one level.

theorem CSD.CV.card_config_neZero (N : ℕ) [NeZero N] (K : ℕ) : NeZero (Fintype.card (FieldConfig K N))

Configuration cardinalities are nonzero once there is at least one level.

theorem CSD.CV.matrix_config_nontrivial (N : ℕ) [NeZero N] (K : ℕ) : Nontrivial (Matrix (FieldConfig K N) (FieldConfig K N) ℂ)

Matrix algebras over configuration spaces are nontrivial.

noncomputable def CSD.CV.leftHomFin (K₁ K₂ N : ℕ) : Matrix (Fin (Fintype.card (FieldConfig K₁ N))) (Fin (Fintype.card (FieldConfig K₁ N))) ℂ →ₐ[ℂ] Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

The left sector algebra through its Fin-index presentation (what the Fin-indexed reconstruction consumes).

Equations

• CSD.CV.leftHomFin K₁ K₂ N = CSD.CV.leftHom.comp ↑(Matrix.reindexAlgEquiv ℂ ℂ (Fintype.equivFin (CSD.CV.FieldConfig K₁ N))).symm

noncomputable def CSD.CV.rightHomFin (K₁ K₂ N : ℕ) : Matrix (Fin (Fintype.card (FieldConfig K₂ N))) (Fin (Fintype.card (FieldConfig K₂ N))) ℂ →ₐ[ℂ] Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

The right sector algebra through its Fin-index presentation.

Equations

• CSD.CV.rightHomFin K₁ K₂ N = CSD.CV.rightHom.comp ↑(Matrix.reindexAlgEquiv ℂ ℂ (Fintype.equivFin (CSD.CV.FieldConfig K₂ N))).symm

theorem CSD.CV.leftHomFin_comm_rightHomFin (K₁ K₂ N : ℕ) (A : Matrix (Fin (Fintype.card (FieldConfig K₁ N))) (Fin (Fintype.card (FieldConfig K₁ N))) ℂ) (B : Matrix (Fin (Fintype.card (FieldConfig K₂ N))) (Fin (Fintype.card (FieldConfig K₂ N))) ℂ) : Commute ((leftHomFin K₁ K₂ N) A) ((rightHomFin K₁ K₂ N) B)

theorem CSD.CV.range_leftHomFin (K₁ K₂ N : ℕ) : Set.range ⇑(leftHomFin K₁ K₂ N) = Set.range ⇑leftHom

theorem CSD.CV.range_rightHomFin (K₁ K₂ N : ℕ) : Set.range ⇑(rightHomFin K₁ K₂ N) = Set.range ⇑rightHom

theorem CSD.CV.composite_generate_fin (K₁ K₂ N : ℕ) : Algebra.adjoin ℂ (Set.range ⇑(leftHomFin K₁ K₂ N) ∪ Set.range ⇑(rightHomFin K₁ K₂ N)) = ⊤

theorem CSD.CV.compositeAlgReconstruction_apply {m n : ℕ} [NeZero m] [NeZero n] {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] [Nontrivial 𝒜] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜) (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hgen : Algebra.adjoin ℂ (Set.range ⇑ιA ∪ Set.range ⇑ιB) = ⊤) (x : TensorProduct ℂ (Matrix (Fin m) (Fin m) ℂ) (Matrix (Fin n) (Fin n) ℂ)) : (SigmaLayer.compositeAlgReconstruction ιA ιB hc hgen) x = (SigmaLayer.reconMap ιA ιB hc) x

The landed reconstruction, applied: it acts as reconMap (definitional; restated for cross-module rewriting).

noncomputable def CSD.CV.compositeArenaForced (K₁ K₂ N : ℕ) [NeZero N] : TensorProduct ℂ (Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) ≃ₐ[ℂ] Matrix (FieldConfig (K₁ + K₂) N) (FieldConfig (K₁ + K₂) N) ℂ

★★ The algebra forcing transports to the composite arena. The composite arena's operator algebra, together with its two mode-local subalgebras, satisfies the premises of compositeAlgReconstruction — the subalgebras commute (leftHomFin_comm_rightHomFin) and generate (composite_generate_fin) — so the landed forcing theorem applies and the composite algebra IS the tensor product of the sector algebras: Matrix C₁ ⊗[ℂ] Matrix C₂ ≃ₐ[ℂ] Matrix C₁₂. Not chosen: forced, by P2's own arena-side locality and generation.

Equations

• One or more equations did not get rendered due to their size.

theorem CSD.CV.compositeArenaForced_tmul (K₁ K₂ N : ℕ) [NeZero N] (A : Matrix (FieldConfig K₁ N) (FieldConfig K₁ N) ℂ) (B : Matrix (FieldConfig K₂ N) (FieldConfig K₂ N) ℂ) : (compositeArenaForced K₁ K₂ N) (A ⊗ₜ[ℂ] B) = leftOp A * rightOp B

The forced equivalence acts as the local product: A ⊗ₜ B ↦ leftOp A · rightOp B. The abstract forcing and the concrete mode-local embeddings agree on the nose.

theorem CSD.CV.card_composite_config (K₁ K₂ N : ℕ) : Fintype.card (FieldConfig (K₁ + K₂) N) = Fintype.card (FieldConfig K₁ N) * Fintype.card (FieldConfig K₂ N)

The composite arena sits at exactly the forced dimension: the joint configuration space has the product cardinality (the arena-side face of composite_dim_eq).