SigmaLayer/TensorTomography: the generation premise IS record-level local tomography (brick 2)

Category: 7-SigmaLayer (the projective-sector layer (Paper C)); the composites residue of the Q11 scoping session (specs/unitary-tpp-scoping.md §3.1 / §7 step 3), scoped in specs/generation-from-records-scoping.md.

What this module does

SigmaLayer/TensorReconstruction.lean forces the tensor product from two premises on a composite observable algebra 𝒜 with local embeddings ιA : M_m → 𝒜, ιB : M_n → 𝒜: locality (the images commute) and generation (Algebra.adjoin ℂ (range ιA ∪ range ιB) = ⊤). Locality is operational. Generation is stated in algebra vocabulary — nothing in compositeAlgReconstruction says what an experimenter does to check it. This module is the premise conversion (the Q11 template of RecordLayer/StatisticsRigidity.lean): it restates generation as a property of the composite's record statistics and proves the two are the same premise.

• localProducts ιA ιB — the joint operators ιA A * ιB B; span_localProducts_eq_top_iff_adjoin_eq_top — under locality the linear span of the local products is a unital subalgebra (localProductsSubalgebra), so generation ⟺ the local products SPAN.
• LocallyTomographic ιA ιB — the state-side principle in functional form: two linear functionals (states included) agreeing on every local product are equal. locallyTomographic_iff_span_eq_top: this is the same as the span condition, both ways (a proper subspace is killed by a nonzero functional).
• productRecordRate ιA ιB ρ bA bB i j — the joint record rate of the local outcomes (i, j): the Born rate Tr(ρ · ιA|bA i⟩⟨bA i| · ιB|bB j⟩⟨bB j|) of the product of the two local rank-one projectors. RecordLocallyTomographic ιA ιB: two composite densities with the same joint record rates, for every pair of local orthonormal bases, are equal. This is local tomography in the vocabulary of the record layer — joint rates of local basis measurements (the LLN limit of the joint counts).
• ★★ recordLocallyTomographic_iff_adjoin_eq_top — under locality and star-preservation of the two embeddings, record-level local tomography ⟺ generation. Hence ★ composite_dim_eq_of_recordLocallyTomographic (k = m · n) and compositeAlgReconstructionOfRecords (M_m ⊗ M_n ≃ₐ 𝒜): the tensor reconstruction consumed with the record-level premise in place of the algebraic one.
• Non-vacuity: the Kronecker composite (aliceHom / bobHom — NoCommunication.aliceOp / bobOp bundled as Matrix.kroneckerLeftAlgHom / kroneckerRightAlgHom) satisfies all the hypotheses and is record-locally-tomographic (kronecker_recordLocallyTomographic) — the record form of joint_mem_span_local.

The two directions (what the proof actually uses)

Generation ⟹ records: ρ = σ is detected by trace pairings against a spanning set (eq_of_trace_mul_eqOn_span); the local products span, and each local factor is spanned by rank-one projectors onto orthonormal-basis vectors (span_onbProjectors_eq_top, from the Hermitian spectral theorem IsHermitian.eq_eigen_outer and ℜ + i ℑ); the pairings against product projectors are the record rates, real because both factors are Hermitian (Gleason.trace_mul_isHermitian_real).

Records ⟹ generation: if the local products do NOT span, a nonzero functional kills them (Submodule.exists_le_ker_of_lt_top), realised as a trace pairing X ↦ Tr(Y X) (exists_forall_eq_trace_mul). Star-preservation makes the local products star-closed, so Yᴴ kills them too, so a nonzero Hermitian H does (exists_isHermitian_ne_zero_of_trace_mul_eq_zero); Tr H = 0 since 1 is a local product. Splitting the spectrum of H into its positive and negative parts gives two densities ρ ≠ σ with ρ.M − σ.M = c⁻¹ • H (IsHermitian.exists_densityOperatorIx_sub_eq) whose joint record rates all agree — contradicting record tomography. Star-preservation is used in both directions (the record rates are real only because the product projectors are Hermitian).

⚠️ Honest scope — read before citing

• This is constraint work on the composite's observable algebra, one level above Σ — the charter's "constrain Σ from above" applied to composites: it pins the composite sector (the epistemic projection of Σ_AB) given A6 locality + the record posit, and asserts nothing about Σ_AB beyond its sector. It is NOT record-layer (MD-1) progress: no {Ωᵢ(M)} is context-fixed here, no ontic record is realised, and no ontic structure is touched.
• It does NOT derive local tomography. It converts the premise: hgen is now an operational statement about joint counts. Whether the world is locally tomographic remains a posit, a permanent operational boundary (⚠️ RESIDUE(R-017)). Classical probability is locally tomographic and real quantum theory is not; local tomography alone does not select ℂ, and nothing here claims it does (the equivalence below uses ℜ/ℑ, so it is a fact about the complex composite).
• LocallyTomographic is stated on all linear functionals, RecordLocallyTomographic on all densities. The pure-state version (agreement on product projectors at every pure preparation) is not built here; under the same hypotheses it is equivalent, via the same subalgebra structure.
• DensityOperatorIx is used as the corpus's existing composite state type; no reading of composite densities as Ω₀-ignorance is a theorem of this module.

References

specs/generation-from-records-scoping.md (the scoping); specs/future-work.md (P3); specs/reconstruction-status.md (A6); SigmaLayer/TensorReconstruction.lean (compositeAlgReconstruction, composite_dim_eq — consumed); SigmaLayer/TensorGeneration.lean (joint_mem_span_local, single_eq_smul); LF2/BornWrapper.lean (outerProduct, IsHermitian.eq_eigen_outer, outerProduct_mul_outerProduct_trace); LF2/MixedEnsembleIx.lean (DensityOperatorIx.rankOne, ensemble, traceForm_rankOne_outerProduct); LF2/EffectGleason.lean (Gleason.trace_mul_isHermitian_real, and Gleason.matrix_eq_zero_of_quadForm_zero — the quadratic-form separation, a polarisation, which this module's functional-form separation exists_forall_eq_trace_mul sits beside; both are distinct from the trace-pairing separation Matrix.ext_iff_trace_mul_left/_right, whose existence form is Empirical/CSD/PointerCommutation.lean exists_trace_mul_ne); RecordLayer/StatisticsRigidity.lean (the Q11 conversion template, and productRecordRate_eq_bornRateBasis — the record rates at a pure preparation ARE the basis-measurement Born rates of the composite register). Pins: Tests/AxiomAudit/SigmaLayer.lean.

Trace pairings against a spanning set

theorem CSD.SigmaLayer.trace_conjTranspose_mul_eq_zero {κ : Type u_1} [Fintype κ] {s : Set (Matrix κ κ ℂ)} (hs : ∀ X ∈ s, star X ∈ s) {Y : Matrix κ κ ℂ} (hY : ∀ X ∈ s, (Y * X).trace = 0) (X : Matrix κ κ ℂ) (hX : X ∈ s) : (Y.conjTranspose * X).trace = 0

If Y trace-annihilates a star-closed set, so does Yᴴ.

theorem CSD.SigmaLayer.exists_isHermitian_ne_zero_of_trace_mul_eq_zero {κ : Type u_1} [Fintype κ] {s : Set (Matrix κ κ ℂ)} (hs : ∀ X ∈ s, star X ∈ s) {Y : Matrix κ κ ℂ} (hY0 : Y ≠ 0) (hY : ∀ X ∈ s, (Y * X).trace = 0) : ∃ (H : Matrix κ κ ℂ), H.IsHermitian ∧ H ≠ 0 ∧ ∀ X ∈ s, (H * X).trace = 0

A nonzero matrix trace-annihilating a star-closed set yields a nonzero Hermitian matrix trace-annihilating it: one of ℜ Y = (Y + Yᴴ)/2, ℑ Y = (Y − Yᴴ)/(2i) is nonzero, and both annihilate.

theorem CSD.SigmaLayer.eq_of_trace_mul_eqOn_span {κ : Type u_1} [Fintype κ] [DecidableEq κ] {s : Set (Matrix κ κ ℂ)} (hs : Submodule.span ℂ s = ⊤) {D E : Matrix κ κ ℂ} (h : ∀ X ∈ s, (D * X).trace = (E * X).trace) : D = E

Two matrices whose trace pairings agree on a spanning set are equal.

theorem CSD.SigmaLayer.exists_forall_eq_trace_mul {κ : Type u_1} [Fintype κ] [DecidableEq κ] (f : Matrix κ κ ℂ →ₗ[ℂ] ℂ) : ∃ (Y : Matrix κ κ ℂ), ∀ (X : Matrix κ κ ℂ), f X = (Y * X).trace

Every linear functional on a matrix algebra is a trace pairing X ↦ Tr(Y X). The functional-form separation lemma: a functional is determined by its values on the matrix units (matrix_eq_sum_single).

Rank-one projectors onto orthonormal-basis vectors span

def CSD.SigmaLayer.onbProjectors (ι : Type u_1) [Fintype ι] : Set (Matrix ι ι ℂ)

The rank-one projectors |b i⟩⟨b i| onto vectors of orthonormal bases of ℂ^ι — the effects whose Born rates are the basis-measurement record rates.

Equations

• CSD.SigmaLayer.onbProjectors ι = Set.range fun (p : OrthonormalBasis ι ℂ (EuclideanSpace ℂ ι) × ι) => CSD.LF2.outerProduct (p.1 p.2)

theorem CSD.SigmaLayer.span_onbProjectors_eq_top (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Submodule.span ℂ (onbProjectors ι) = ⊤

The orthonormal-basis projectors span the matrix algebra. A Hermitian matrix is a combination of its eigenvector projectors (IsHermitian.eq_eigen_outer), and every matrix is ℜ + i ℑ of Hermitian matrices.

Local products, and generation as a span condition

def CSD.SigmaLayer.localProducts {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜) : Set 𝒜

The local products ιA A * ιB B of a composite with local embeddings ιA, ιB.

Equations

• CSD.SigmaLayer.localProducts ιA ιB = {X : 𝒜 | ∃ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), X = ιA A * ιB B}

theorem CSD.SigmaLayer.one_mem_localProducts {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜) : 1 ∈ localProducts ιA ιB

theorem CSD.SigmaLayer.apply_mem_localProducts_left {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜) (A : Matrix (Fin m) (Fin m) ℂ) : ιA A ∈ localProducts ιA ιB

theorem CSD.SigmaLayer.apply_mem_localProducts_right {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜) (B : Matrix (Fin n) (Fin n) ℂ) : ιB B ∈ localProducts ιA ιB

theorem CSD.SigmaLayer.mul_mem_localProducts {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)) {X Y : 𝒜} (hX : X ∈ localProducts ιA ιB) (hY : Y ∈ localProducts ιA ιB) : X * Y ∈ localProducts ιA ιB

Under locality the local products are closed under multiplication: (ιA A · ιB B)(ιA A' · ιB B') = ιA (A A') · ιB (B B').

theorem CSD.SigmaLayer.star_mem_localProducts {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] {ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜} {ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜} [StarRing 𝒜] (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) {X : 𝒜} (hX : X ∈ localProducts ιA ιB) : star X ∈ localProducts ιA ιB

Under locality and star-preservation the local products are star-closed.

noncomputable def CSD.SigmaLayer.localProductsSubalgebra {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)) : Subalgebra ℂ 𝒜

Under locality, the span of the local products is a unital subalgebra.

Equations

• CSD.SigmaLayer.localProductsSubalgebra ιA ιB hc = (Submodule.span ℂ (CSD.SigmaLayer.localProducts ιA ιB)).toSubalgebra ⋯ ⋯

@[simp]

theorem CSD.SigmaLayer.localProductsSubalgebra_toSubmodule {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)) : Subalgebra.toSubmodule (localProductsSubalgebra ιA ιB hc) = Submodule.span ℂ (localProducts ιA ιB)

theorem CSD.SigmaLayer.span_localProducts_eq_top_iff_adjoin_eq_top {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)) : Submodule.span ℂ (localProducts ιA ιB) = ⊤ ↔ Algebra.adjoin ℂ (Set.range ⇑ιA ∪ Set.range ⇑ιB) = ⊤

Generation ⟺ the local products span. Under locality, Algebra.adjoin ℂ (range ιA ∪ range ιB) = ⊤ (the generation premise of compositeAlgReconstruction) holds iff the linear span of the local products is everything.

State-side local tomography, functional form

def CSD.SigmaLayer.LocallyTomographic {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜) : Prop

Local tomography (state side, functional form): two linear functionals on the composite agreeing on every local product are equal — a composite state is determined by its local-product expectations.

Equations

• CSD.SigmaLayer.LocallyTomographic ιA ιB = ∀ (f g : 𝒜 →ₗ[ℂ] ℂ), (∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), f (ιA A * ιB B) = g (ιA A * ιB B)) → f = g

theorem CSD.SigmaLayer.locallyTomographic_iff_span_eq_top {m n : ℕ} {𝒜 : Type u_1} [Ring 𝒜] [Algebra ℂ 𝒜] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] 𝒜) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] 𝒜) : LocallyTomographic ιA ιB ↔ Submodule.span ℂ (localProducts ιA ιB) = ⊤

Functional-form local tomography ⟺ the local products span. (⇐) is LinearMap.ext_on; (⇒): a proper subspace is killed by a nonzero functional, which then agrees with 0 on every local product.

theorem CSD.SigmaLayer.locallyTomographic_iff_adjoin_eq_top {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)) : LocallyTomographic ιA ιB ↔ Algebra.adjoin ℂ (Set.range ⇑ιA ∪ Set.range ⇑ιB) = ⊤

Generation (the premise of compositeAlgReconstruction) is functional-form local tomography.

Record-level local tomography

noncomputable def CSD.SigmaLayer.productRecordRate {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (ρ : LF2.DensityOperatorIx κ) (bA : OrthonormalBasis (Fin m) ℂ (EuclideanSpace ℂ (Fin m))) (bB : OrthonormalBasis (Fin n) ℂ (EuclideanSpace ℂ (Fin n))) (i : Fin m) (j : Fin n) : ℝ

The joint record rate of the local outcomes (i, j): the Born rate, at the composite preparation ρ, of the product of the local rank-one projectors onto bA i and bB j — the joint rate of the two local basis measurements (the LLN limit of their joint count).

Equations

• CSD.SigmaLayer.productRecordRate ιA ιB ρ bA bB i j = ρ.traceForm (ιA (CSD.LF2.outerProduct (bA i)) * ιB (CSD.LF2.outerProduct (bB j)))

def CSD.SigmaLayer.RecordLocallyTomographic {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ) : Prop

Record-level local tomography: two composite preparations with the same joint record rates for every pair of local orthonormal bases are equal.

Equations

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

theorem CSD.SigmaLayer.isHermitian_apply_mul_apply {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] {ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ} {ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ} (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) {A : Matrix (Fin m) (Fin m) ℂ} {B : Matrix (Fin n) (Fin n) ℂ} (hA : A.IsHermitian) (hB : B.IsHermitian) : (ιA A * ιB B).IsHermitian

Under locality and star-preservation, the image of a pair of Hermitian local operators is Hermitian.

theorem CSD.SigmaLayer.traceForm_eq_iff_of_isHermitian {κ : Type u_1} [Fintype κ] [DecidableEq κ] (ρ σ : LF2.DensityOperatorIx κ) {P : Matrix κ κ ℂ} (hP : P.IsHermitian) : ρ.traceForm P = σ.traceForm P ↔ (ρ.M * P).trace = (σ.M * P).trace

Born rates of a Hermitian effect agree iff the (real) trace pairings agree.

theorem CSD.SigmaLayer.span_localProducts_le_span_mul {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] {ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ} {ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ} : Submodule.span ℂ (localProducts ιA ιB) ≤ Submodule.span ℂ (⇑ιA '' onbProjectors (Fin m) * ⇑ιB '' onbProjectors (Fin n))

Under locality, the span of the local products lies in the span of the product projectors ιA |a⟩⟨a| · ιB |b⟩⟨b| (a, b orthonormal-basis vectors) — the effects whose Born rates are the joint record rates.

theorem CSD.SigmaLayer.recordLocallyTomographic_of_span_eq_top {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] {ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ} {ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ} (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) (hspan : Submodule.span ℂ (localProducts ιA ιB) = ⊤) : RecordLocallyTomographic ιA ιB

Generation ⟹ record-level local tomography. If the local products span, two densities with equal joint record rates have equal trace pairings on the product projectors, which span.

theorem CSD.SigmaLayer.IsHermitian.exists_densityOperatorIx_sub_eq {κ : Type u_1} [Fintype κ] [DecidableEq κ] {H : Matrix κ κ ℂ} (hH : H.IsHermitian) (hH0 : H ≠ 0) (htr : H.trace = 0) : ∃ (ρ : LF2.DensityOperatorIx κ) (σ : LF2.DensityOperatorIx κ) (c : ℝ), 0 < c ∧ ρ.M - σ.M = (↑c)⁻¹ • H

A traceless nonzero Hermitian matrix is a positive multiple of a difference of two densities: split the spectrum into positive and negative parts, H = c (ρ − σ) with ρ = ∑ max(λᵢ,0)/c · |eᵢ⟩⟨eᵢ|, σ = ∑ max(−λᵢ,0)/c · |eᵢ⟩⟨eᵢ|, c = ∑ max(λᵢ,0) > 0.

theorem CSD.SigmaLayer.span_eq_top_of_recordLocallyTomographic {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] {ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ} {ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ} (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) (h : RecordLocallyTomographic ιA ιB) : Submodule.span ℂ (localProducts ιA ιB) = ⊤

Record-level local tomography ⟹ generation. If the local products do not span, a nonzero Hermitian H trace-annihilates them; it is traceless (1 is a local product), so it is a multiple of a difference of two densities whose joint record rates all agree — contradicting record tomography.

theorem CSD.SigmaLayer.recordLocallyTomographic_iff_adjoin_eq_top {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) : RecordLocallyTomographic ιA ιB ↔ Algebra.adjoin ℂ (Set.range ⇑ιA ∪ Set.range ⇑ιB) = ⊤

★★ Record-level local tomography ⟺ generation. Under locality and star-preservation of the local embeddings, the generation premise of the tensor reconstruction is exactly: the composite's joint record rates of local basis measurements determine its state.

theorem CSD.SigmaLayer.recordLocallyTomographic_iff_locallyTomographic {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) : RecordLocallyTomographic ιA ιB ↔ LocallyTomographic ιA ιB

Record-level and functional-form local tomography coincide under the same hypotheses.

noncomputable def CSD.SigmaLayer.compositeAlgReconstructionOfRecords {m n : ℕ} {κ : Type u_1} [Fintype κ] [DecidableEq κ] (ιA : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix κ κ ℂ) (ιB : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix κ κ ℂ) [NeZero m] [NeZero n] [Nonempty κ] (hc : ∀ (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ), Commute (ιA A) (ιB B)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) (h : RecordLocallyTomographic ιA ιB) : TensorProduct ℂ (Matrix (Fin m) (Fin m) ℂ) (Matrix (Fin n) (Fin n) ℂ) ≃ₐ[ℂ] Matrix κ κ ℂ

The tensor reconstruction with the record-level premise: M_m ⊗ M_n ≃ₐ M_κ from locality, star-preservation and record-level local tomography (compositeAlgReconstruction consumed with recordLocallyTomographic_iff_adjoin_eq_top).

Equations

• CSD.SigmaLayer.compositeAlgReconstructionOfRecords ιA ιB hc hsA hsB h = CSD.SigmaLayer.compositeAlgReconstruction ιA ιB hc ⋯

theorem CSD.SigmaLayer.composite_dim_eq_of_recordLocallyTomographic {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)) (hsA : ∀ (A : Matrix (Fin m) (Fin m) ℂ), ιA (star A) = star (ιA A)) (hsB : ∀ (B : Matrix (Fin n) (Fin n) ℂ), ιB (star B) = star (ιB B)) (h : RecordLocallyTomographic ιA ιB) : k = m * n

★ The dimension corollary with the record-level premise: a composite M_k with commuting, star-preserving local embeddings whose joint record rates determine its state has k = m · n (composite_dim_eq consumed through recordLocallyTomographic_iff_adjoin_eq_top).

Non-vacuity: the Kronecker composite

noncomputable def CSD.SigmaLayer.aliceHom (m n : ℕ) : Matrix (Fin m) (Fin m) ℂ →ₐ[ℂ] Matrix (Fin m × Fin n) (Fin m × Fin n) ℂ

Alice's local algebra A ↦ A ⊗ₖ 1 as an algebra hom: NoCommunication.aliceOp bundled (Matrix.kroneckerLeftAlgHom).

Equations

• CSD.SigmaLayer.aliceHom m n = Matrix.kroneckerLeftAlgHom ℂ (Fin m) (Fin n)

noncomputable def CSD.SigmaLayer.bobHom (m n : ℕ) : Matrix (Fin n) (Fin n) ℂ →ₐ[ℂ] Matrix (Fin m × Fin n) (Fin m × Fin n) ℂ

Bob's local algebra B ↦ 1 ⊗ₖ B as an algebra hom: NoCommunication.bobOp bundled (Matrix.kroneckerRightAlgHom).

Equations

• CSD.SigmaLayer.bobHom m n = Matrix.kroneckerRightAlgHom ℂ (Fin m) (Fin n)

@[simp]

theorem CSD.SigmaLayer.aliceHom_apply {m n : ℕ} (A : Matrix (Fin m) (Fin m) ℂ) : (aliceHom m n) A = Empirical.QM.NoCommunication.aliceOp A

@[simp]

theorem CSD.SigmaLayer.bobHom_apply {m n : ℕ} (B : Matrix (Fin n) (Fin n) ℂ) : (bobHom m n) B = Empirical.QM.NoCommunication.bobOp B

theorem CSD.SigmaLayer.aliceHom_star {m n : ℕ} (A : Matrix (Fin m) (Fin m) ℂ) : (aliceHom m n) (star A) = star ((aliceHom m n) A)

theorem CSD.SigmaLayer.bobHom_star {m n : ℕ} (B : Matrix (Fin n) (Fin n) ℂ) : (bobHom m n) (star B) = star ((bobHom m n) B)

theorem CSD.SigmaLayer.commute_aliceHom_bobHom {m n : ℕ} (A : Matrix (Fin m) (Fin m) ℂ) (B : Matrix (Fin n) (Fin n) ℂ) : Commute ((aliceHom m n) A) ((bobHom m n) B)

Locality of the Kronecker composite (aliceOp_bobOp_commute in bundled form).

theorem CSD.SigmaLayer.localProducts_aliceHom_bobHom {m n : ℕ} : localProducts (aliceHom m n) (bobHom m n) = {X : Matrix (Fin m × Fin n) (Fin m × Fin n) ℂ | ∃ (U : Matrix (Fin m) (Fin m) ℂ) (Q : Matrix (Fin n) (Fin n) ℂ), X = Empirical.QM.NoCommunication.aliceOp U * Empirical.QM.NoCommunication.bobOp Q}

The local products of the Kronecker composite are the joint local products of joint_mem_span_local.

theorem CSD.SigmaLayer.kronecker_adjoin_eq_top {m n : ℕ} : Algebra.adjoin ℂ (Set.range ⇑(aliceHom m n) ∪ Set.range ⇑(bobHom m n)) = ⊤

The Kronecker local algebras generate (Matrix.adjoin_range_kroneckerLeftAlgHom_union_eq_top; the subalgebra form of joint_mem_span_local).

theorem CSD.SigmaLayer.kronecker_recordLocallyTomographic {m n : ℕ} : RecordLocallyTomographic (aliceHom m n) (bobHom m n)

The Kronecker composite is record-locally-tomographic: joint rates of local basis measurements determine the composite state. Non-vacuity of RecordLocallyTomographic.

theorem CSD.SigmaLayer.kronecker_locallyTomographic {m n : ℕ} : LocallyTomographic (aliceHom m n) (bobHom m n)

The Kronecker composite is locally tomographic in functional form.

Product projectors are projectors onto product vectors

theorem CSD.SigmaLayer.outerProduct_tensorState {ι₁ : Type u_1} {ι₂ : Type u_2} (φ : EuclideanSpace ℂ ι₁) (ψ : EuclideanSpace ℂ ι₂) : LF2.outerProduct (QuantumInfo.tensorState φ ψ) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (LF2.outerProduct φ) (LF2.outerProduct ψ)

The outer product of a product vector is the Kronecker product of the outer products: |φ ⊗ ψ⟩⟨φ ⊗ ψ| = |φ⟩⟨φ| ⊗ₖ |ψ⟩⟨ψ|.