Empirical/CSD: a quantum circuit is a flow on Σ, and its readout is a record basin

Category: 3-Local (CSD-side companion to Empirical/QM/Algorithms/; the generic engine the algorithm twins GroverFlow.lean and ShorFlow.lean instantiate).

A quantum circuit on a register indexed by ι is a unitary U on EuclideanSpace ℂ ι. On the CSD side the register's state space is the sector Σ = ℂℙ^{card ι − 1} (cpSectorData), the circuit is the flow x ↦ U • x on it, running the circuit k times is the flow iterated k times, and the readout of the computational-basis measurement is the record basin of the outcome (RecordLayer/GlobalBasin.lean) or, on the density-operator side, the de-isolation channel (LF6/DecoherenceChannel.lean). Nothing here is specific to an algorithm: the pattern is Empirical/CSD/QEC/RegisterFlow.lean's, factored out.

• Circuit ι — a unitary on the register; Circuit.toUnitaryGroup, the enumerated unitary in U(card ι); Circuit.flow, the circuit as a Σ-flow; Circuit.flow_iterate, k runs are the projective action of U ^ k;
• ★ Circuit.isUnitaryLift_flow — the flow lifts the circuit's unitary through the register representative, with no hypothesis (through the canonical measurable unit section);
• ★★ Circuit.barycenter_flow_iterate — the density operator after k runs is U^k ρ (U^k)ᴴ, for every preparation, derived from the ontic flow (barycenter_flow);
• readout ρ i — the weight the de-isolation channel assigns to outcome i; readout_outerProduct, readout_conj_outerProduct — on a pure input it is the Born weight ‖ψ i‖², and after a unitary it is ‖(U ψ) i‖²; barycenterMatrix_dirac — the density operator of a preparation concentrated at one point is the projector of its representative;
• ★★ Circuit.epistemicMeasure_globalBasin_flow_iterate — the readout on Σ: at the point reached from the ray of a unit ψ by k runs of the circuit, the record basin of outcome i has Born weight ‖(U^k ψ) i‖² (globalBasin_born).

Helpers, index-generic: toEuclideanLin_pow_apply, toEuclideanLin_reindex_piLpCongrLeft.

⚠️ Honest scope. A circuit is its unitary; no gate decomposition, timing, or Hamiltonian generating U is modelled (the flow is the time-one map of the projective action, as in RegisterFlow.lean, and R-015 applies). The readout is the corpus's computational-basis record basin, context-fixed and kinematic (globalBasin_born's own scope note).

References: Empirical/CSD/QEC/RegisterFlow.lean (the pattern); LF2/FlowChannel.lean (IsUnitaryLift, barycenter_flow); RecordLayer/GlobalBasin.lean (globalBasin_born); LF6/DecoherenceChannel.lean; specs/BACKLOG.md #34; specs/future-work.md.

Index-generic helpers

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_pow_apply {ι : Type u_1} [Fintype ι] [DecidableEq ι] (U : Matrix ι ι ℂ) (k : ℕ) (v : EuclideanSpace ℂ ι) : (Matrix.toEuclideanLin (U ^ k)) v = (⇑(Matrix.toEuclideanLin U))^[k] v

toEuclideanLin of a power is the iterate: @[simp] Matrix.toLpLin_pow applied to a vector.

theorem CSD.Empirical.CSDBridge.Algorithms.toEuclideanLin_reindex_piLpCongrLeft {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (U : Matrix ι ι ℂ) (v : EuclideanSpace ℂ ι) : (Matrix.toEuclideanLin ((Matrix.reindex e e) U)) ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) v) = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin U) v)

Reindexing a matrix and its argument together.

theorem CSD.Empirical.CSDBridge.Algorithms.piLpCongrLeft_apply_apply {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (v : EuclideanSpace ℂ ι) (i : ι) : ((LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) v).ofLp (e i) = v.ofLp i

The coordinate of a reindexed vector at a reindexed index.

The register's sector and representative

structure CSD.Empirical.CSDBridge.Algorithms.Circuit (ι : Type u_1) [Fintype ι] [DecidableEq ι] : Type u_1

A circuit on the register indexed by ι: a unitary on EuclideanSpace ℂ ι.

• U : Matrix ι ι ℂ

  The unitary of the circuit.

• conjTranspose_mul : self.U.conjTranspose * self.U = 1

  Unitarity, Uᴴ U = 1.

instance CSD.Empirical.CSDBridge.Algorithms.instNeZeroCard {ι : Type u_1} [Fintype ι] [Nonempty ι] : NeZero (Fintype.card ι)

A nonempty register has a nonzero number of basis states.

@[reducible, inline]

noncomputable abbrev CSD.Empirical.CSDBridge.Algorithms.idx (ι : Type u_2) [Fintype ι] : ι ≃ Fin (Fintype.card ι)

The enumeration of the register's index that places its sector at ℂℙ^{card ι − 1}.

Equations

• CSD.Empirical.CSDBridge.Algorithms.idx ι = Fintype.equivFin ι

@[reducible, inline]

abbrev CSD.Empirical.CSDBridge.Algorithms.RegisterSector (ι : Type u_2) [Fintype ι] : Type

The register's sector, Σ = ℂℙ^{card ι − 1}.

Equations

• CSD.Empirical.CSDBridge.Algorithms.RegisterSector ι = CSD.LF4.CPN (Fintype.card ι)

noncomputable def CSD.Empirical.CSDBridge.Algorithms.registerRep (ι : Type u_2) [Fintype ι] : RegisterSector ι → EuclideanSpace ℂ ι

The register representative: the canonical measurable unit section of the sector, read in the register's own index.

Equations

• CSD.Empirical.CSDBridge.Algorithms.registerRep ι x = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ (CSD.Empirical.CSDBridge.Algorithms.idx ι)).symm (Projectivization.unitSection x)

theorem CSD.Empirical.CSDBridge.Algorithms.registerRep_norm {ι : Type u_1} [Fintype ι] (x : RegisterSector ι) : ‖registerRep ι x‖ = 1

theorem CSD.Empirical.CSDBridge.Algorithms.measurable_registerRep {ι : Type u_1} [Fintype ι] : Measurable (registerRep ι)

The circuit as a flow

noncomputable def CSD.Empirical.CSDBridge.Algorithms.Circuit.toUnitaryGroup {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) : ↥(Matrix.unitaryGroup (Fin (Fintype.card ι)) ℂ)

The circuit's unitary, enumerated, as an element of U(card ι).

Equations

• C.toUnitaryGroup = ⟨(Matrix.reindex (CSD.Empirical.CSDBridge.Algorithms.idx ι) (CSD.Empirical.CSDBridge.Algorithms.idx ι)) C.U, ⋯⟩

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.coe_toUnitaryGroup {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) : ↑C.toUnitaryGroup = (Matrix.reindex (idx ι) (idx ι)) C.U

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.coe_toUnitaryGroup_pow {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) (k : ℕ) : ↑(C.toUnitaryGroup ^ k) = (Matrix.reindex (idx ι) (idx ι)) (C.U ^ k)

The enumerated unitary of k runs is the reindexed U ^ k.

noncomputable def CSD.Empirical.CSDBridge.Algorithms.Circuit.flow {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) : RegisterSector ι → RegisterSector ι

The circuit as a flow on Σ: the projective action of its unitary on the register's sector. A flow of the corpus's cpSectorData (Σ = P = ℂℙ^{card ι − 1}, π = id).

Equations

• C.flow x = C.toUnitaryGroup • x

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.flow_def {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) (x : RegisterSector ι) : C.flow x = C.toUnitaryGroup • x

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.measurable_flow {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) : Measurable C.flow

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.flow_iterate {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) (k : ℕ) (x : RegisterSector ι) : C.flow^[k] x = C.toUnitaryGroup ^ k • x

k runs of the circuit are the flow iterated k times: the projective action of U ^ k.

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.isUnitaryLift_flow_unitSection {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (C : Circuit ι) (p₀ : RegisterSector ι) : LF2.IsUnitaryLift (LF4.cpSectorData p₀) C.flow Projectivization.unitSection ↑C.toUnitaryGroup

★ The flow lifts the enumerated unitary through the canonical unit section, with no hypothesis.

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.isUnitaryLift_flow {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (C : Circuit ι) (p₀ : RegisterSector ι) : LF2.IsUnitaryLift (LF4.cpSectorData p₀) C.flow (registerRep ι) C.U

★ The flow lifts the circuit's own unitary through the register representative.

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.barycenter_flow_iterate {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (C : Circuit ι) (p₀ : RegisterSector ι) (μprep : MeasureTheory.Measure (RegisterSector ι)) [MeasureTheory.IsProbabilityMeasure μprep] (k : ℕ) : LF2.barycenterMatrix (registerRep ι) (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π (MeasureTheory.Measure.map C.flow^[k] μprep)) = C.U ^ k * LF2.barycenterMatrix (registerRep ι) (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π μprep) * (C.U ^ k).conjTranspose

★★ The density operator after k runs is U^k ρ (U^k)ᴴ, for every preparation on the sector, derived from the ontic flow: the Schrödinger picture of the circuit.

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.barycenter_unitSection_flow_iterate {ι : Type u_1} [Fintype ι] [DecidableEq ι] [Nonempty ι] (C : Circuit ι) (p₀ : RegisterSector ι) (μprep : MeasureTheory.Measure (RegisterSector ι)) [MeasureTheory.IsProbabilityMeasure μprep] (k : ℕ) : LF2.barycenterMatrix Projectivization.unitSection (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π (MeasureTheory.Measure.map C.flow^[k] μprep)) = ↑(C.toUnitaryGroup ^ k) * LF2.barycenterMatrix Projectivization.unitSection (MeasureTheory.Measure.map (LF4.cpSectorData p₀).π μprep) * (↑(C.toUnitaryGroup ^ k)).conjTranspose

The same in the enumerated index, the form the readout channel takes.

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.flow_iterate_mk {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) (k : ℕ) (ψ : EuclideanSpace ℂ (Fin (Fintype.card ι))) (hψ0 : ψ ≠ 0) : C.flow^[k] (Projectivization.mk ℂ ψ hψ0) = Projectivization.mk ℂ ((Matrix.toEuclideanLin ↑(C.toUnitaryGroup ^ k)) ψ) ⋯

The point reached from the ray of ψ by k runs is the ray of U^k ψ.

theorem CSD.Empirical.CSDBridge.Algorithms.Circuit.epistemicMeasure_globalBasin_flow_iterate {ι : Type u_1} [Fintype ι] [DecidableEq ι] (C : Circuit ι) (k : ℕ) (ψ : EuclideanSpace ℂ (Fin (Fintype.card ι))) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin (Fintype.card ι)) : (RecordLayer.epistemicMeasure (C.flow^[k] (Projectivization.mk ℂ ψ hψ0))) (RecordLayer.globalBasin (RecordLayer.momentContext (Fintype.card ι)) i) = ENNReal.ofReal (‖((Matrix.toEuclideanLin ↑(C.toUnitaryGroup ^ k)) ψ).ofLp i‖ ^ 2)

★★ The readout on Σ. At the point reached from the ray of a unit vector ψ by k runs of the circuit, the record basin of the computational-basis outcome i (the apparatus's context-fixed basin, globalBasin) has Born weight ‖(U^k ψ) i‖².

The readout channel

noncomputable def CSD.Empirical.CSDBridge.Algorithms.readout {M : ℕ} [NeZero M] (ρ : Matrix (Fin M) (Fin M) ℂ) (i : Fin M) : ℂ

The readout: the weight the de-isolation channel assigns to the computational-basis outcome i of a density operator ρ, the diagonal entry of the channel's output.

Equations

• CSD.Empirical.CSDBridge.Algorithms.readout ρ i = (CSD.LF6.deisolationChannel M).apply ρ i i

theorem CSD.Empirical.CSDBridge.Algorithms.readout_outerProduct {M : ℕ} [NeZero M] (φ : EuclideanSpace ℂ (Fin M)) (i : Fin M) : readout (LF2.outerProduct φ) i = ↑(‖φ.ofLp i‖ ^ 2)

On a pure input the readout is the Born weight.

theorem CSD.Empirical.CSDBridge.Algorithms.readout_conj_outerProduct {M : ℕ} [NeZero M] (V : Matrix (Fin M) (Fin M) ℂ) (φ : EuclideanSpace ℂ (Fin M)) (i : Fin M) : readout (V * LF2.outerProduct φ * V.conjTranspose) i = ↑(‖((Matrix.toEuclideanLin V) φ).ofLp i‖ ^ 2)

After a unitary, the readout of a pure input is the Born weight of the image.

theorem CSD.Empirical.CSDBridge.Algorithms.barycenterMatrix_dirac {Q : Type u_2} [MeasurableSpace Q] [MeasurableSingletonClass Q] {κ : Type u_3} (rep : Q → EuclideanSpace ℂ κ) (q : Q) : LF2.barycenterMatrix rep (MeasureTheory.Measure.dirac q) = LF2.outerProduct (rep q)

The density operator of a preparation concentrated at one point is the projector of that point's representative.