ST-2: the entanglement distance on the composite arena

Category: 3-Local (CV; entanglement geometry at finite dimension). BACKLOG #38, brick ST-2 of records-to-spacetime-scoping.md.

ST-1 (RecordInfluence.lean) gave the composite arena a causal shape from the coupling graph. This file gives it a correlational one: the mutual information of two sectors, and the separation functional d = −log I that reads it as a distance. The scoping note prices this as research rather than as something the record layer needs, and says so; it is here because the author asked for entanglement geometry as a direction.

Mutual information

• mutualInfo hpsd = S(ρ_A) + S(ρ_B) − S(ρ_AB) for a bipartite density, off the two partial traces, with mutualInfo_congr_matrix (it depends only on the matrix) and vonNeumannEntropy_congr_matrix underneath;
• ★★ mutualInfo_nonneg — non-negative, which is subadditivity of the von Neumann entropy (vonNeumannEntropy_subadditive), with the standard positive-definite support condition on the marginals;
• ★★★ mutualInfo_kronecker — a product state carries none: I(ρ ⊗ σ) = 0 exactly, because the marginals of a product are the factors and the entropy is additive over ⊗;
• ★★★ mutualInfo_pureDensity — on a pure state the mutual information is twice the entanglement entropy: the joint entropy vanishes (pureDensity_mul_self, new) and the two marginals have equal entropy (pure_marginal_entropy_eq), so I(A:B) = 2 S(ρ_A).

The distance, and the arena

• entDist I = −log I with I ≤ 0 sent to ⊤: ★ entDist_zero (no correlation, infinitely far), ★ entDist_antitone (more correlation is less distance), ★ entDist_eq_zero_of_one_le (a nat or more of mutual information puts the sectors at distance zero);
• compositeDM — the composite arena point in product coordinates, whose right partial trace is the corpus's reducedDM (reducedDM_eq_partialTraceRight);
• ★★★ mutualInfo_compositeDM_join and ★★ entDist_mutualInfo_join — a product point of the composite arena carries no mutual information, and its two sectors are infinitely far apart;
• ★★ mutualInfoTri_mono — enlarging a sector cannot decrease the mutual information, hence cannot increase the distance: I(A:B) ≤ I(A:BC), which is strong subadditivity rearranged.

Honest scope

⚠️ entDist is a separation functional, not a proved metric. No triangle inequality is proved or claimed, here or anywhere in the corpus. Calling −log I a "distance" is the physics convention this file adopts; the properties proved are the three the scoping note asked for — the sign, the product-point value, and monotonicity — and nothing beyond them.

⚠️ Monotonicity carries the corpus's SSA hypothesis. mutualInfoTri_mono is QuantumInfo.strong_subadditivity_of_relEntropy_monotone rearranged, so it inherits that theorem's explicit data-processing bound hDPI rather than assuming it silently: the corpus does not prove SSA unconditionally at this pin, and this file does not pretend otherwise.

⚠️ This is not geometry from records, and not a step toward emergent spacetime. It is a correlation functional on a finite-dimensional composite arena. The scoping note's finding is unchanged: what is missing for emergence proper is which coarse-graining projection defines the macroscopic coordinates, and that is the author's decision rather than a lemma. Nothing here feeds the record layer; ST-1 is the brick that does.

⚠️ Finite cutoff throughout (FieldConfig K N), and the arena statements are about the join (product) points; the entangled case is covered only through mutualInfo_pureDensity, as twice a marginal entropy, with no numerical value computed for any particular entangled ray.

References: records-to-spacetime-scoping.md ST-2; Mathlib/QuantumInfo/{Entropy, Subadditivity, StrongSubadditivity}.lean; CV/{CompositeArena, EntangledWeights}.lean; specs/BACKLOG.md #38.

Mutual information of a bipartite density

theorem CSD.CV.vonNeumannEntropy_congr_matrix {n : Type u_1} [Fintype n] [DecidableEq n] {ρ σ : Matrix n n ℂ} (h : ρ = σ) (hρ : ρ.IsHermitian) (hσ : σ.IsHermitian) : QuantumInfo.vonNeumannEntropy hρ = QuantumInfo.vonNeumannEntropy hσ

Entropy depends only on the matrix, not on the Hermitian witness or on how the matrix is written.

noncomputable def CSD.CV.mutualInfo {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {ρ : Matrix (n × m) (n × m) ℂ} (hpsd : ρ.PosSemidef) : ℝ

The mutual information I(A:B) = S(ρ_A) + S(ρ_B) − S(ρ_AB) of a bipartite density, read off the two partial traces.

Equations

• CSD.CV.mutualInfo hpsd = QuantumInfo.vonNeumannEntropy ⋯ + QuantumInfo.vonNeumannEntropy ⋯ - QuantumInfo.vonNeumannEntropy ⋯

theorem CSD.CV.mutualInfo_congr_matrix {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {ρ σ : Matrix (n × m) (n × m) ℂ} (h : ρ = σ) (hρ : ρ.PosSemidef) (hσ : σ.PosSemidef) : mutualInfo hρ = mutualInfo hσ

Mutual information depends only on the matrix.

theorem CSD.CV.mutualInfo_nonneg {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {ρ : Matrix (n × m) (n × m) ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) (hpdA : (QuantumInfo.partialTraceRight ρ).PosDef) (hpdB : (QuantumInfo.partialTraceLeft ρ).PosDef) : 0 ≤ mutualInfo hpsd

★★ Mutual information is non-negative — subadditivity of the von Neumann entropy, with the standard positive-definite support condition on the two marginals.

theorem CSD.CV.mutualInfo_kronecker {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {ρ : Matrix n n ℂ} {σ : Matrix m m ℂ} (hpsdρ : ρ.PosSemidef) (hpsdσ : σ.PosSemidef) (htrρ : ρ.trace = 1) (htrσ : σ.trace = 1) : mutualInfo ⋯ = 0

★★★ A product state carries no mutual information. The marginals of ρ ⊗ σ are ρ and σ and the entropy is additive over the tensor product, so I = 0 exactly.

theorem CSD.CV.pureDensity_mul_self {n : Type u_1} {m : Type u_2} [Fintype n] [Fintype m] {ψ : n × m → ℂ} (hψ : ∑ p : n × m, ‖ψ p‖ ^ 2 = 1) : QuantumInfo.pureDensity ψ * QuantumInfo.pureDensity ψ = QuantumInfo.pureDensity ψ

A unit vector's pure density is a projection.

theorem CSD.CV.mutualInfo_pureDensity {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] {ψ : n × m → ℂ} (hψ : ∑ p : n × m, ‖ψ p‖ ^ 2 = 1) (hpsd : (QuantumInfo.pureDensity ψ).PosSemidef) : mutualInfo hpsd = 2 * QuantumInfo.vonNeumannEntropy ⋯

★★★ For a pure bipartite state the mutual information is twice the marginal entropy. The joint entropy vanishes and the two marginals have equal entropy, so I(A:B) = 2 S(ρ_A): on a pure state the mutual information is the entanglement entropy, doubled.

The entanglement distance

noncomputable def CSD.CV.entDist (I : ℝ) : ENNReal

The entanglement distance of a mutual information: d = −log I, with the vanishing case sent to ⊤. Unentangled sectors are infinitely far apart; a mutual information of at least 1 nat puts them at distance zero. ⚠️ This is a separation functional, not a proved metric: no triangle inequality is claimed anywhere in this file.

Equations

• CSD.CV.entDist I = if I ≤ 0 then ⊤ else ENNReal.ofReal (-Real.log I)

@[simp]

theorem CSD.CV.entDist_of_nonpos {I : ℝ} (h : I ≤ 0) : entDist I = ⊤

theorem CSD.CV.entDist_zero : entDist 0 = ⊤

theorem CSD.CV.entDist_of_pos {I : ℝ} (h : 0 < I) : entDist I = ENNReal.ofReal (-Real.log I)

theorem CSD.CV.entDist_antitone {I J : ℝ} (hI : 0 < I) (hIJ : I ≤ J) : entDist J ≤ entDist I

★ More correlation is less distance: the distance is antitone in the mutual information.

theorem CSD.CV.entDist_eq_zero_of_one_le {I : ℝ} (h : 1 ≤ I) : entDist I = 0

★ A mutual information of a nat or more sits at distance zero.

On the composite arena

noncomputable def CSD.CV.compositeDM {K₁ K₂ N : ℕ} (x : FieldArena (K₁ + K₂) N) : Matrix (FieldConfig K₁ N × FieldConfig K₂ N) (FieldConfig K₁ N × FieldConfig K₂ N) ℂ

The composite arena density in product coordinates: the matrix whose partial traces are the two sectors' reduced states.

Equations

• CSD.CV.compositeDM x = CSD.CV.compositeReindex.symm (CSD.CV.arenaDM x)

theorem CSD.CV.reducedDM_eq_partialTraceRight {K₁ K₂ N : ℕ} (x : FieldArena (K₁ + K₂) N) : reducedDM x = QuantumInfo.partialTraceRight (compositeDM x)

theorem CSD.CV.mutualInfo_compositeDM_join {K₁ K₂ N : ℕ} (p : FieldArena K₁ N) (q : FieldArena K₂ N) (hpsd : (compositeDM (arenaJoin p q)).PosSemidef) : mutualInfo hpsd = 0

★★★ A product point of the composite arena carries no mutual information. The join of two single-sector points has I = 0: on the arena, zero mutual information is exactly the product-point case this theorem names, and the entanglement distance there is infinite.

theorem CSD.CV.entDist_mutualInfo_join {K₁ K₂ N : ℕ} (p : FieldArena K₁ N) (q : FieldArena K₂ N) (hpsd : (compositeDM (arenaJoin p q)).PosSemidef) : entDist (mutualInfo hpsd) = ⊤

★★ The two sectors of a product point are infinitely far apart.

Monotonicity under sector enlargement

theorem CSD.CV.mutualInfoTri_mono {a : Type u_1} {b : Type u_2} {c : Type u_3} [Fintype a] [DecidableEq a] [Fintype b] [DecidableEq b] [Fintype c] [DecidableEq c] {ρ : Matrix (a × b × c) (a × b × c) ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) (hpdA : (QuantumInfo.rhoA ρ).PosDef) (hpdB : (QuantumInfo.rhoB ρ).PosDef) (hpdBC : (QuantumInfo.rhoBC ρ).PosDef) (hDPI : ∀ (hpdA' : (QuantumInfo.partialTraceRight (QuantumInfo.rhoAB ρ)).PosDef), QuantumInfo.relEntropy ⋯ ⋯ ≤ QuantumInfo.relEntropy ⋯ ⋯) : QuantumInfo.vonNeumannEntropy ⋯ + QuantumInfo.vonNeumannEntropy ⋯ - QuantumInfo.vonNeumannEntropy ⋯ ≤ QuantumInfo.vonNeumannEntropy ⋯ + QuantumInfo.vonNeumannEntropy ⋯ - QuantumInfo.vonNeumannEntropy ⋯

★★ Enlarging a sector cannot decrease the mutual information, hence cannot increase the entanglement distance: I(A:B) ≤ I(A:BC). This is strong subadditivity rearranged, and it carries the same hypothesis the corpus's SSA carries — the data-processing bound hDPI, left explicit rather than assumed (QuantumInfo.strong_subadditivity_of_relEntropy_monotone).