Actual Adaptive Low-Instrument Effects

Abstract

Finite adaptive events generated by one forward unitary and arbitrary low instruments span the least invariant unital star algebra.

Definition 1.1 (Normalized finite instruments).

$$\forall A\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)]\mathrm{LowInstrument}(A)=\{n:\mathrm{Nat}(),m:\mathrm{Nat}(),K:\mathrm{Fin}(n)\to \mathrm{Fin}(m)\to \mathrm{CStarMatrix}(A,A,\mathbb{C})\mid \sum _{y:\mathrm{Fin}(n)}\sum _{r:\mathrm{Fin}(m)}\mathrm{star}(K(y,r))\cdot K(y,r)=\mathrm{identity}(A)\}$$

Formalization. D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.LowInstrument (✓ std3).

Source. Repository-derived.

Commentary.

The outcome index is retained. The Kraus index within an outcome is hidden and summed. Different outcomes can select different subsequent protocols. Zero Kraus operators allow different finite Kraus multiplicities to be padded to a common size.

Definition 1.2 (Finite adaptive events).

$$\forall A\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)]\mathrm{Event}(A)=\mathrm{inductive}(\forall b\in \mathrm{Bool}(),\mathrm{stop}(b):\mathrm{Event}(A),\forall next\in \mathrm{Event}(A),\mathrm{tick}(next):\mathrm{Event}(A),\forall I\in \mathrm{LowInstrument}(A),\forall next\in \mathrm{Fin}(\mathrm{outcomes}(I))\to \mathrm{Event}(A),\mathrm{observe}(I,next):\mathrm{Event}(A))$$

Formalization. D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.Event (✓ std3).

Source. Repository-derived.

Commentary.

An event is a finite tree with accepting or rejecting Boolean leaves, a forward tick, and a normalized low instrument with an outcome-dependent continuation. Selecting the accepting leaves specifies a union of mutually exclusive complete histories. Selecting every descendant of a node specifies an intermediate event.

Definition 1.3 (The actual low tensor action).

$$\forall A\in \mathrm{Type}(),\forall H\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)][\mathrm{Fintype}(H)][\mathrm{DecidableEq}(H)]\forall K\in \mathrm{CStarMatrix}(A,A,\mathbb{C}),\mathrm{tensorLow}(H,K)=\mathrm{kronecker}(K,\mathrm{identity}(H))$$

Formalization. D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.tensorLow (✓ std3).

Source. Repository-derived.

Commentary.

The low embedding tensors a low matrix with the high identity. It preserves the unit, addition, multiplication, complex scalars and adjoints.

Definition 1.4 (Heisenberg event effects).

$$\forall A\in \mathrm{Type}(),\forall J\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)][\mathrm{Fintype}(J)][\mathrm{DecidableEq}(J)]\forall l\in \mathrm{StarAlgHom}(\mathbb{C},\mathrm{CStarMatrix}(A,A,\mathbb{C}),\mathrm{CStarMatrix}(J,J,\mathbb{C})),\forall W\in \mathrm{CStarMatrix}(J,J,\mathbb{C}),\forall e\in \mathrm{Event}(A),\mathrm{effect}(l,W,e)=\mathrm{cases}(e,\mathrm{stop}(b:\mathrm{Bool}())\mapsto \mathrm{if}(b,\mathrm{identity}(J),0),\mathrm{tick}(X:\mathrm{Event}(A))\mapsto \mathrm{star}(W)\cdot \mathrm{effect}(l,W,X)\cdot W,\mathrm{observe}(I:\mathrm{LowInstrument}(A),next:\mathrm{Fin}(\mathrm{outcomes}(I))\to \mathrm{Event}(A))\mapsto \sum _{y:\mathrm{Fin}(\mathrm{outcomes}(I))}\sum _{r:\mathrm{Fin}(\mathrm{multiplicity}(I))}\mathrm{star}(\mathrm{apply}(l,\mathrm{kraus}(I,y,r)))\cdot \mathrm{effect}(l,W,\mathrm{apply}(next,y))\cdot \mathrm{apply}(l,\mathrm{kraus}(I,y,r)))$$

Formalization. D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.effect (✓ std3).

Source. Repository-derived.

Commentary.

An accepted leaf has effect identity and a rejected leaf has effect zero. A tick pulls back the next effect by W. An instrument sums its Kraus pullbacks, using the continuation selected by each recorded outcome.

Definition 1.5 (Accepted Schrödinger substates).

$$\forall A\in \mathrm{Type}(),\forall J\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)][\mathrm{Fintype}(J)][\mathrm{DecidableEq}(J)]\forall l\in \mathrm{StarAlgHom}(\mathbb{C},\mathrm{CStarMatrix}(A,A,\mathbb{C}),\mathrm{CStarMatrix}(J,J,\mathbb{C})),\forall W\in \mathrm{CStarMatrix}(J,J,\mathbb{C}),\forall e\in \mathrm{Event}(A),\forall rho\in \mathrm{CStarMatrix}(J,J,\mathbb{C}),\mathrm{eventState}(l,W,e,rho)=\mathrm{cases}(e,\mathrm{stop}(b:\mathrm{Bool}())\mapsto \mathrm{if}(b,rho,0),\mathrm{tick}(X:\mathrm{Event}(A))\mapsto \mathrm{eventState}(l,W,X,W\cdot rho\cdot \mathrm{star}(W)),\mathrm{observe}(I:\mathrm{LowInstrument}(A),next:\mathrm{Fin}(\mathrm{outcomes}(I))\to \mathrm{Event}(A))\mapsto \sum _{y:\mathrm{Fin}(\mathrm{outcomes}(I))}\sum _{r:\mathrm{Fin}(\mathrm{multiplicity}(I))}\mathrm{eventState}(l,W,\mathrm{apply}(next,y),\mathrm{apply}(l,\mathrm{kraus}(I,y,r))\cdot rho\cdot \mathrm{star}(\mathrm{apply}(l,\mathrm{kraus}(I,y,r)))))$$

Formalization. D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.eventState (✓ std3).

Source. Repository-derived.

Commentary.

The event map returns the input at an accepted leaf and zero at a rejected leaf. A tick evolves the input by W before continuing. An instrument continues on each Kraus substate and sums the accepted outputs. Inputs may have arbitrary low-high correlations.

Definition 1.6 (The actual complex effect span).

$$\forall A\in \mathrm{Type}(),\forall J\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)][\mathrm{Fintype}(J)][\mathrm{DecidableEq}(J)]\forall l\in \mathrm{StarAlgHom}(\mathbb{C},\mathrm{CStarMatrix}(A,A,\mathbb{C}),\mathrm{CStarMatrix}(J,J,\mathbb{C})),\forall W\in \mathrm{CStarMatrix}(J,J,\mathbb{C}),\mathrm{effectSpan}(l,W)=\mathrm{complexSpan}(\mathrm{range}(\mathrm{effect}(l,W)))$$

Formalization. D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.effectSpan (✓ std3).

Source. Repository-derived.

Commentary.

The span is taken over the effects of actual finite events. Linear combinations of effects are algebraic observables and need not themselves be executable events.

Theorem 1.7 (Trace duality, effect bounds and the least invariant algebra).

$$\forall A\in \mathrm{Type}(),\forall H\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)][\mathrm{Nonempty}(A)][\mathrm{Fintype}(H)][\mathrm{DecidableEq}(H)][\mathrm{Nonempty}(H)]\forall W\in \mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C}),\left(\mathrm{star}(W)\cdot W=\mathrm{identity}(A\times H)\wedge W\cdot \mathrm{star}(W)=\mathrm{identity}(A\times H)\right)\Rightarrow \left(\left(\forall e\in \mathrm{Event}(A),\forall rho\in \mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C}),\mathrm{trace}(\mathrm{eventState}(\mathrm{tensorLow}(H),W,e,rho))=\mathrm{trace}(\mathrm{effect}(\mathrm{tensorLow}(H),W,e)\cdot rho)\right)\wedge \left(\left(\forall e\in \mathrm{Event}(A),0\le \mathrm{effect}(\mathrm{tensorLow}(H),W,e)\wedge \mathrm{effect}(\mathrm{tensorLow}(H),W,e)\le \mathrm{identity}(A\times H)\right)\wedge \left(\exists D\in \mathrm{StarSubalgebra}(\mathbb{C},\mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C})),\mathrm{complexSpace}(D)=\mathrm{effectSpan}(\mathrm{tensorLow}(H),W)\wedge \left(\left(\forall K\in \mathrm{CStarMatrix}(A,A,\mathbb{C}),\mathrm{tensorLow}(H,K)\in D\right)\wedge \left(\left(\forall X\in \mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C}),X\in D\iff \mathrm{star}(W)\cdot X\cdot W\in D\right)\wedge \left(\forall R\in \mathrm{StarSubalgebra}(\mathbb{C},\mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C})),\left(\left(\forall K\in \mathrm{CStarMatrix}(A,A,\mathbb{C}),\mathrm{tensorLow}(H,K)\in R\right)\wedge \left(\forall X\in \mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C}),X\in R\Rightarrow \mathrm{star}(W)\cdot X\cdot W\in R\right)\right)\Rightarrow D\subseteq R\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.actual_adaptive_span (✓ std3). ∎

Source. Repository-derived.

Commentary.

A scaled low filter can be completed by the positive square root of its defect to a normalized two-outcome instrument. Selecting the filter outcome and polarizing gives every low cross-sandwich of the actual effect span. Its two-sided idealizer therefore contains the low algebra. Forward prefixing preserves the span; finite-dimensional injectivity makes this preservation surjective. The idealizer is invariant, and event recursion puts every effect back in it. This proves equality and minimality. Inverse conjugation occurs only in the finite-dimensional proof; the event tree permits only forward ticks.

References

• Truth anchor: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.Event
• Truth anchor: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.LowInstrument
• Truth anchor: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.actual_adaptive_span
• Truth anchor: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.effect
• Truth anchor: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.effectSpan
• Truth anchor: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.eventState
• Truth anchor: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan.tensorLow
• Dependency: D5/S3/Quantum/Foundation/FiniteStateChannel