Bounded Adaptive Low-Instrument Effects

Abstract

The complex spans of finite adaptive event effects with bounded forward calls satisfy an exact recurrence under free low instruments.

Definition 1.1 (Worst recorded-branch call count).

$$\forall A\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)]\forall e\in \mathrm{Event}(A),\mathrm{worstBranchCalls}(e)=\mathrm{cases}(e,\mathrm{stop}(b:\mathrm{Bool}())\mapsto 0,\mathrm{tick}(next:\mathrm{Event}(A))\mapsto 1+\mathrm{worstBranchCalls}(next),\mathrm{observe}(I:\mathrm{LowInstrument}(A),next:\mathrm{Fin}(\mathrm{outcomes}(I))\to \mathrm{Event}(A))\mapsto \mathrm{FinsetSup}(\mathrm{univ}(\mathrm{Fin}(\mathrm{outcomes}(I))),y:\mathrm{Fin}(\mathrm{outcomes}(I))\mapsto \mathrm{worstBranchCalls}(\mathrm{apply}(next,y))))$$

Formalization. D5/S3/Quantum/Measurement/BoundedAdaptiveLowInstrumentSpan.worstBranchCalls (✓ std3).

Source. Repository-derived.

Commentary.

A stopped event uses no calls. A tick adds one call. An instrument takes the maximum over its recorded outcomes, with empty maximum zero. Instruments are free. The hidden Kraus index is summed in the effect and never selects a continuation or enters the call maximum.

Definition 1.2 (Actual effects within a budget).

$$\forall A\in \mathrm{Type}(),\forall H\in \mathrm{Type}(),[\mathrm{Fintype}(A)][\mathrm{DecidableEq}(A)][\mathrm{Fintype}(H)][\mathrm{DecidableEq}(H)]\forall W\in \mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C}),\forall N\in \mathrm{Nat}(),\mathrm{boundedEffectSpan}(W,N)=\mathrm{complexSpan}(\{X:\mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C})\mid \exists e\in \mathrm{Event}(A),\mathrm{worstBranchCalls}(e)\le N\wedge X=\mathrm{effect}(\mathrm{tensorLow}(H),W,e)\})$$

Formalization. D5/S3/Quantum/Measurement/BoundedAdaptiveLowInstrumentSpan.boundedEffectSpan (✓ std3).

Source. Repository-derived.

Commentary.

The generators are effects of actual finite event trees with at most N ticks on every recorded branch. The low action tensors a low matrix with the high identity. Complex linear combinations need not themselves be executable events. The budget counts ticks and places no bound on the number of free instruments, records or linear-combination coefficients.

Theorem 1.3 (The exact next-call span).

$$\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}),\forall N\in \mathrm{Nat}(),\mathrm{boundedEffectSpan}(W,N+1)=\mathrm{complexSpan}(\mathrm{carrier}(\mathrm{boundedEffectSpan}(W,N))\cup \{Y:\mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C})\mid \exists K\in \mathrm{CStarMatrix}(A,A,\mathbb{C}),\exists X\in \mathrm{CStarMatrix}(A\times H,A\times H,\mathbb{C}),X\in \mathrm{boundedEffectSpan}(W,N)\wedge Y=\mathrm{star}(\mathrm{tensorLow}(H,K))\cdot \mathrm{star}(W)\cdot X\cdot W\cdot \mathrm{tensorLow}(H,K)\})$$

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

Source. Repository-derived.

Commentary.

For every natural budget and finite nonempty low and high index types, the next span is generated by the current span and its low sandwiches after one forward pullback. A low matrix can be scaled to a contraction and completed by the positive square root of its defect to a two-outcome instrument. Continuing on the first outcome and rejecting on the second preserves the call count. Cancelling the nonzero scale in the complex span gives low sandwich stability. Tree induction handles all finite free prefixes and sums each hidden Kraus index with the same recorded-outcome continuation. Conversely, for a tail that is an actual event, prefixing one tick and such a filter realizes its sandwich up to a nonzero scalar. Complex linearity then places the sandwich of every element of the current span in the next span. The joint matrix W is arbitrary in this algebraic identity. A physical clock application requires a unitary W; positivity and normalization are supplied by the unitary event theory. The recurrence asserts neither general multiplicative closure, a saturation budget nor a uniform probability gap.

References

• Truth anchor: D5/S3/Quantum/Measurement/BoundedAdaptiveLowInstrumentSpan.actual_bounded_effect_span_recurrence
• Truth anchor: D5/S3/Quantum/Measurement/BoundedAdaptiveLowInstrumentSpan.boundedEffectSpan
• Truth anchor: D5/S3/Quantum/Measurement/BoundedAdaptiveLowInstrumentSpan.worstBranchCalls
• Dependency: D5/S3/Quantum/Measurement/AdaptiveLowInstrumentSpan