Passive Adaptive Transcript Upper Bound

Abstract

Every deterministic adaptive transcript using a passive experiment family factors through the complete joint experiment readout.

Theorem 1.1 (Every passive adaptive transcript factors through all experiment answers).

$$\begin{array}{r}\forall U,X:\mathrm{Type},R:U\to \mathrm{Type},\\ q:\forall u:U,X\to R_u,\\ pi:\mathrm{PassiveProtocol}\left(U,R\right),\mathrm{Refines}\left(\mathrm{runPassiveProtocol}\left(q,pi\right),\mathrm{jointReadout}\left(q\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/PassiveAdaptiveTranscriptUpperBound.passive_adaptive_transcript_upper_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

A passive protocol is a finite dependent decision tree. At each query node, the answer selects the continuation, so later experiments may depend on the transcript already observed.

The operational evaluator reads each selected channel from the state. A separate replay evaluator follows the same tree from the complete dependent tuple of all experiment answers. Induction on the protocol identifies the two transcripts and supplies the factor map.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiment/PassiveAdaptiveTranscriptUpperBound.passive_adaptive_transcript_upper_bound
• Dependency: D5/S3/ConceptDynamics/ConceptJoinUniversal
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion