LF3 Projectors / TensorModel: derive ProjectorAlgebra from a tensor structure

Category: 3-Local (LF3 v2 derivation: ProjectorAlgebra / MeasurementUnitary from TensorEmbedding / UnitaryTensorEmbedding).

Paper §9.7 v2 derivation target.

The abstract ProjectorAlgebra in LF3/Projectors/Core.lean carries the four projection identities (self-adjointness, idempotence, mutual orthogonality, completeness) as fields, per spec §9.7's "v1.00 takes the algebra as data" carve-out. This module supplies the corresponding v2 derivation: given an abstract bipartite tensor-factor structure on H_SA (encoded as a TensorEmbedding K_A K_B H_SA), the four projection-algebra fields become theorems derived from the BinaryPointerProjectors per-wing data plus the tensor-embedding algebraic laws.

This discharges the ProjectorAlgebra half of D4 / G6 (the composite tensor structure debt) at the Lean level. The MeasurementUnitary half of D4 / G6 splits in two: the factorisation field is feasible by the same TensorEmbedding-based derivation (immediate follow-up); the eigenstate- action field requires operator-exponential / Stone machinery and is explicitly LF4-or-later per spec §9.5.

Design

A TensorEmbedding encodes the bipartite tensor structure of H_SA through two lift functions liftA, liftB that embed per-wing operators into H_SA-operators (the implicit "tensor with identity on the other factor and on the system factor" map), together with the algebraic properties that make them unital *-algebra homomorphisms with commuting images.

This formulation avoids Mathlib's tensor-product-of-inner-product-spaces API (uneven coverage). The system Hilbert space H_AB itself is not exposed as a field; only the projections through liftA and liftB matter for the ProjectorAlgebra derivation. Concrete instantiations (matrix realisations via Matrix.kroneckerMap, or full Hilbert-space constructions via TensorProduct ℂ) are left to LF4 or to callers; this module gives the abstract derivation.

ProjectorAlgebra.ofTensorEmbedding builds the abstract projector algebra from a TensorEmbedding plus the SystemApparatusSetup's per-wing BinaryPointerProjectors. The four fields are theorems.

Callers without a TensorEmbedding (LF3 v1.00 callers) continue to construct ProjectorAlgebra directly; this module is additive, not invasive.

Helper: reverse pointer-projector orthogonality

BinaryPointerProjectors.orthogonal gives proj .plus ∘L proj .minus = 0 in that order. The orthogonal proof for ProjectorAlgebra.ofTensorEmbedding also needs proj .minus ∘L proj .plus = 0 (case s = .minus, s' = .plus). It follows from completeness and idempotence: proj .minus ∘L proj .plus = proj .minus ∘L (1 - proj .minus) = proj .minus - proj .minus ∘L proj .minus = proj .minus - proj .minus = 0.

theorem CSD.LF3.BinaryPointerProjectors.orthogonal_rev {K : Type u_4} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [FiniteDimensional ℂ K] (P : BinaryPointerProjectors K) : P.proj Sign.minus ∘SL P.proj Sign.plus = 0

TensorEmbedding

structure CSD.LF3.TensorEmbedding (K_A : Type u_4) (K_B : Type u_5) (H_SA : Type u_6) [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] : Type (max (max u_4 u_5) u_6)

Abstract bipartite tensor-factor structure on H_SA with K_A and K_B as the two pointer-side factors. Encoded through lift functions liftA : (K_A →L[ℂ] K_A) → (H_SA →L[ℂ] H_SA) and similarly liftB, satisfying unital algebra-homomorphism laws (composition, identity, addition, zero) and commuting images.

Mathematically: liftA(f) realises f ⊗ I_AB ⊗ I_{K_B} and liftB(g) realises I_{K_A} ⊗ I_AB ⊗ g under an implicit identification H_SA ≅ H_AB ⊗ K_A ⊗ K_B. The system Hilbert space H_AB itself is not a field of the structure; only the projections through liftA and liftB matter for the ProjectorAlgebra derivation.

• liftA : (K_A →L[ℂ] K_A) → H_SA →L[ℂ] H_SA

  Lift of A-side operators to H_SA-operators.

• liftB : (K_B →L[ℂ] K_B) → H_SA →L[ℂ] H_SA

  Lift of B-side operators.

• liftA_comp (f g : K_A →L[ℂ] K_A) : self.liftA (f ∘SL g) = self.liftA f ∘SL self.liftA g

  liftA preserves composition.

• liftB_comp (f g : K_B →L[ℂ] K_B) : self.liftB (f ∘SL g) = self.liftB f ∘SL self.liftB g

  liftB preserves composition.

• liftA_one : self.liftA 1 = 1

  liftA preserves identity.

• liftB_one : self.liftB 1 = 1

  liftB preserves identity.

• liftA_add (f g : K_A →L[ℂ] K_A) : self.liftA (f + g) = self.liftA f + self.liftA g

  liftA preserves addition.

• liftB_add (f g : K_B →L[ℂ] K_B) : self.liftB (f + g) = self.liftB f + self.liftB g

  liftB preserves addition.

• liftA_zero : self.liftA 0 = 0

  liftA preserves zero.

• liftB_zero : self.liftB 0 = 0

  liftB preserves zero.

• liftA_selfAdjoint (f : K_A →L[ℂ] K_A) : (∀ (x y : K_A), inner ℂ (f x) y = inner ℂ x (f y)) → ∀ (x y : H_SA), inner ℂ ((self.liftA f) x) y = inner ℂ x ((self.liftA f) y)

  liftA preserves the inner-product self-adjointness predicate.

• liftB_selfAdjoint (f : K_B →L[ℂ] K_B) : (∀ (x y : K_B), inner ℂ (f x) y = inner ℂ x (f y)) → ∀ (x y : H_SA), inner ℂ ((self.liftB f) x) y = inner ℂ x ((self.liftB f) y)

  liftB preserves the inner-product self-adjointness predicate.

• liftA_liftB_commute (f : K_A →L[ℂ] K_A) (g : K_B →L[ℂ] K_B) : self.liftA f ∘SL self.liftB g = self.liftB g ∘SL self.liftA f

  A-side and B-side lifts commute (tensor-factor independence).

Pointwise commutation lemma

theorem CSD.LF3.TensorEmbedding.liftA_liftB_commute_apply {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (T : TensorEmbedding K_A K_B H_SA) (f : K_A →L[ℂ] K_A) (g : K_B →L[ℂ] K_B) (y : H_SA) : (T.liftB g) ((T.liftA f) y) = (T.liftA f) ((T.liftB g) y)

Pointwise consequence of liftA_liftB_commute.

ProjectorAlgebra constructor

def CSD.LF3.ProjectorAlgebra.ofTensorEmbedding {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (T : TensorEmbedding K_A K_B H_SA) : ProjectorAlgebra S

ProjectorAlgebra from a TensorEmbedding. The pointer-sector projector M_{st} is T.liftA (S.ptrA.proj s) ∘L T.liftB (S.ptrB.proj t), encoding I_AB ⊗ Q^A_s ⊗ Q^B_t under the implicit tensor identification of H_SA. The four projection-algebra fields are derived as theorems from the corresponding BinaryPointerProjectors fields plus the tensor-embedding algebraic laws.

Equations

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

UnitaryTensorEmbedding and the MeasurementUnitary factorisation

The same bipartite tensor-factor structure of H_SA, in its unitary form: per-wing unitaries vA : K_A ≃ₗᵢ[ℂ] K_A and vB : K_B ≃ₗᵢ[ℂ] K_B lift to H_SA ≃ₗᵢ[ℂ] H_SA through unitary-preserving extensions of the TensorEmbedding's algebra-homomorphism lifts.

Used to derive MeasurementUnitary.factorises (u x = uA (uB x)) from the definition u := uB.trans uA. The eigenstate-action field (action) remains data per spec §9.5 carve-out (operator-exponential machinery).

The commutation condition liftA_unitary vA and liftB_unitary vB commute is the unitary analogue of TensorEmbedding.liftA_liftB_commute: tensor-factor independence at the unitary level. It is physically required (per-wing unitaries act on independent Hilbert factors and therefore commute) and is included for fidelity, even though MeasurementUnitary.factorises itself does not consume it.

A UnitaryTensorEmbedding is intentionally a standalone structure rather than an extension of TensorEmbedding: callers needing only the operator algebra-hom (e.g. the ProjectorAlgebra derivation above) should not be required to supply unitary lifts as well. Future work that needs a single coherent abstraction (with (liftA_unitary v).toContinuousLinearMap = liftA v.toContinuousLinearMap as a coherence field) can combine the two; the current split keeps preconditions minimal.

structure CSD.LF3.UnitaryTensorEmbedding (K_A : Type u_4) (K_B : Type u_5) (H_SA : Type u_6) [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] : Type (max (max u_4 u_5) u_6)

Unitary bipartite tensor-factor structure on H_SA. Per-wing unitaries lift to H_SA-unitaries; A-wing and B-wing lifts commute.

• liftA_unitary : (K_A ≃ₗᵢ[ℂ] K_A) → H_SA ≃ₗᵢ[ℂ] H_SA

  Lift of A-wing unitary.

• liftB_unitary : (K_B ≃ₗᵢ[ℂ] K_B) → H_SA ≃ₗᵢ[ℂ] H_SA

  Lift of B-wing unitary.

• liftA_liftB_unitary_commute (vA : K_A ≃ₗᵢ[ℂ] K_A) (vB : K_B ≃ₗᵢ[ℂ] K_B) : (self.liftA_unitary vA).trans (self.liftB_unitary vB) = (self.liftB_unitary vB).trans (self.liftA_unitary vA)

  A-wing and B-wing unitary lifts commute (tensor-factor independence at the unitary level; physically required because per-wing unitaries act on independent Hilbert factors).

theorem CSD.LF3.liftA_liftB_apply_comm {K_A : Type u_4} {K_B : Type u_5} {H_SA : Type u_6} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (E : UnitaryTensorEmbedding K_A K_B H_SA) (vA : K_A ≃ₗᵢ[ℂ] K_A) (vB : K_B ≃ₗᵢ[ℂ] K_B) (x : H_SA) : (E.liftB_unitary vB) ((E.liftA_unitary vA) x) = (E.liftA_unitary vA) ((E.liftB_unitary vB) x)

Local operations on independent wings commute, pointwise. Applying the A-wing unitary and then the B-wing one gives the same state as the other order — the kinematic core of tensor-factor independence, and the level at which no-signalling starts.

This is the consumer of liftA_liftB_unitary_commute. Until 2026-07-28 that field was carried by every instance and used by nothing (scripts/check-vacuity.sh); the docstring above says so honestly, but a hypothesis every instantiator must discharge should buy something. Now it does.

def CSD.LF3.MeasurementUnitary.ofUnitaryTensorEmbedding {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (T : UnitaryTensorEmbedding K_A K_B H_SA) (vA : K_A ≃ₗᵢ[ℂ] K_A) (vB : K_B ≃ₗᵢ[ℂ] K_B) (jointEig : Sign × Sign → K_A → K_B → H_SA) (ptrTransA : Sign → K_A → K_A) (ptrTransB : Sign → K_B → K_B) (action : ∀ (s t : Sign) (φA : K_A) (φB : K_B), (T.liftA_unitary vA) ((T.liftB_unitary vB) (jointEig (s, t) φA φB)) = jointEig (s, t) (ptrTransA s φA) (ptrTransB t φB)) : MeasurementUnitary S

MeasurementUnitary from a UnitaryTensorEmbedding plus per-wing unitaries plus the joint-eigenstate / pointer-translation data.

The full unitary is defined as u := (liftB_unitary vB).trans (liftA_unitary vA). The factorises field then follows by definition of LinearIsometryEquiv.trans, discharged here as rfl (no separate proof needed). The action field remains caller-supplied per spec §9.5: it encodes the impulsive-readout idealisation and requires operator-exponential / Stone machinery, which is LF4-or-later.

Equations

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