Documentation

CsdLean4.SigmaLayer.TensorReconstruction

SigmaLayer/TensorReconstruction: locality + generation FORCE the tensor product (P3, the uniqueness half) #

Category: 7-SigmaLayer (the projective-sector layer (Paper C)).

SigmaLayer/TensorSolved.lean proves SUFFICIENCY — the standard Kronecker composite satisfies locality and local tomography. This module proves the converse, NECESSITY / uniqueness: any composite algebra 𝒜 carrying commuting local matrix algebras that GENERATE it must BE the tensor product — there is no other composite. That is the real "why ⊗" reconstruction, and its dimension corollary discharges bridge B6 (CompositeSector.tensor_dimension, NA · NB = Njoint) as a THEOREM rather than a posit.

The theorem #

Given unital ℂ-algebra embeddings ιA : M_m → 𝒜, ιB : M_n → 𝒜 with COMMUTING images that GENERATE 𝒜 (Algebra.adjoin ℂ (range ιA ∪ range ιB) = ⊤), the lifted map

Φ = Algebra.TensorProduct.lift ιA ιB : M_m ⊗[ℂ] M_n → 𝒜, A ⊗ B ↦ ιA A · ιB B

is an ALGEBRA EQUIVALENCE (compositeAlgReconstruction). The mechanism is exactly the operational argument: M_m ⊗ M_n is a SIMPLE ring (Artin–Wedderburn: it is ≃ M_{mn}), so the unital Φ is INJECTIVE (a ring hom out of a simple ring is injective); GENERATION makes it SURJECTIVE; hence bijective.

The dimension corollary (discharging B6) #

For a composite represented by M_k(ℂ), finrank across the equivalence forces k² = (mn)², i.e. k = mn (composite_dim_eq). So the tensor-product dimension NA · NB is not a postulate but a consequence of locality + generation — the reconstruction the sector interface (CompositeInterface, TensorSector) previously took as the bridge-B6 field.

References: specs/future-work.md (P3 / SL-P3r, bridge B6); SigmaLayer/TensorSolved.lean (composite_is_tensor_product, the sufficiency half — the tensor model realizes the principles); SigmaLayer/TensorGeneration.lean (joint_mem_span_local, the quantum generation fact); SigmaLayer/CompositeInterface.lean (CompositeSector.tensor_dimension, the field this discharges).

M_m ⊗ M_n is a simple ring #

source
instance CSD.SigmaLayer.matrixTensor_isSimpleRing (m n : ℕ) [NeZero m] [NeZero n] :
IsSimpleRing (TensorProduct ℂ (Matrix (Fin m) (Fin m) ℂ) (Matrix (Fin n) (Fin n) ℂ))

M_m(ℂ) ⊗ M_n(ℂ) is simple. Transport IsSimpleRing along the Kronecker algebra equivalence M_m ⊗ M_n ≃ₐ M_{m×n}(ℂ ⊗ ℂ) from the matrix ring over the simple ℂ ⊗ ℂ. This is the Artin–Wedderburn fact that makes any unital map out of M_m ⊗ M_n injective.

The reconstruction #

source
noncomputable def CSD.SigmaLayer.reconMap {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ι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)) :
TensorProduct ℂ (Matrix (Fin m) (Fin m) ℂ) (Matrix (Fin n) (Fin n) ℂ) →ₐ[ℂ] 𝒜

The reconstruction map Φ : M_m ⊗ M_n → 𝒜, A ⊗ B ↦ ιA A · ιB B, from commuting local embeddings. Algebra.TensorProduct.lift of the two algebra homs with commuting images.

Equations
Instances For
    source
    @[simp]
    theorem CSD.SigmaLayer.reconMap_tmul {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ι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)) (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ) :
    (reconMap ιA ιB hc) (A ⊗ₜ[ℂ] B) = ιA A * ιB B
    source
    noncomputable def CSD.SigmaLayer.compositeAlgReconstruction {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] [NeZero m] [NeZero n] [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) = ⊤) :
    TensorProduct ℂ (Matrix (Fin m) (Fin m) ℂ) (Matrix (Fin n) (Fin n) ℂ) ≃ₐ[ℂ] 𝒜

    THE RECONSTRUCTION — locality + generation force ⊗. With commuting local embeddings whose images GENERATE 𝒜, the reconstruction map Φ is an ALGEBRA EQUIVALENCE M_m ⊗ M_n ≃ₐ 𝒜: injective because M_m ⊗ M_n is simple (so the unital Φ has trivial kernel), surjective because the images generate. So the composite 𝒜 IS the tensor product — not chosen, forced.

    Equations
    Instances For

      The dimension corollary — discharging bridge B6 #

      source
      theorem CSD.SigmaLayer.composite_dim_eq {m n k : ℕ} [NeZero m] [NeZero n] [NeZero k] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix (Fin k) (Fin k) ℂ) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix (Fin k) (Fin k) ℂ) (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) = ⊤) :
      k = m * n

      The composite dimension is forced: k = m · n. If a composite represented by M_k(ℂ) carries commuting, generating local algebras M_m, M_n, then k = m · n. The reconstruction gives an algebra (hence linear) equivalence M_m ⊗ M_n ≃ M_k, so finrank gives (m·n)² = k², whence k = m·n. This discharges bridge B6 (CompositeSector.tensor_dimension) as a theorem.

      Discharging bridge B6 in the sector interface #

      CompositeSector.tensor_dimension (SigmaLayer/CompositeInterface.lean) is the NA · NB = Njoint FIELD that posited B6. The smart constructor below builds a CompositeSector in which that field is DERIVED from the reconstruction — the caller supplies the joint sector plus commuting, generating local observable embeddings, and composite_dim_eq PROVES the dimension. So B6 need no longer be assumed: any composite whose local algebras are commuting and generating gets its tensor dimension for free.

      source
      noncomputable def CSD.SigmaLayer.CompositeSector.ofReconstruction {NA NB k : ℕ} [NeZero NA] [NeZero NB] [NeZero k] {Sigma : Type u_2} [MeasurableSpace Sigma] {D : ConstraintDynamics Sigma} (jointSector : ProjectiveSector k D) (ιA : Matrix (Fin NA) (Fin NA) ℂ →ₐ[ℂ] Matrix (Fin k) (Fin k) ℂ) (ιB : Matrix (Fin NB) (Fin NB) ℂ →ₐ[ℂ] Matrix (Fin k) (Fin k) ℂ) (hc : ∀ (A : Matrix (Fin NA) (Fin NA) ℂ) (B : Matrix (Fin NB) (Fin NB) ℂ), Commute (ιA A) (ιB B)) (hgen : Algebra.adjoin ℂ (Set.range ⇑ιA ∪ Set.range ⇑ιB) = ⊤) :
      CompositeSector NA NB k D

      A composite sector with the tensor dimension DERIVED, not posited (B6 discharged). Given the joint ProjectiveSector on M_k and commuting, generating local observable embeddings M_NA, M_NB ↪ M_k, this constructs the CompositeSector whose tensor_dimension : NA * NB = k field is filled by composite_dim_eq rather than taken on faith.

      Equations
      Instances For