Sampling a certificate beside a framed word

Turing.MultiTapePTM.pairSampler is one fixed fair-coin machine with three control states and no work tapes. On an input frame y ++ r it copies frame y to the output, then emits one fresh fair bit for each symbol of r, and halts at the right boundary. So it outputs frame y ++ w, the pair encoding of (y, w), for a uniform word w of length r.length. It takes exactly (frame y ++ r).length + 1 transitions. Each copying transition also draws a coin, and ignores it. Read nondeterministically, the machine guesses a certificate for the framed instance.

Main definitions

• Turing.MultiTapePTM.pairSampler: the framed copier and certificate sampler.

Main results

• Turing.MultiTapePTM.eval_pairSampler: the output is a uniform certificate after the framed word.
• Turing.MultiTapePTM.pairSampler_halted: every run has halted at the linear clock.

inductive Turing.MultiTapePTM.PairSampler.Phase : Type

The control phases: before a frame tag, before a framed data bit, and in the sampled tail.

• tag : Phase
• data : Phase
• tail : Phase

@[instance_reducible]

instance Turing.MultiTapePTM.PairSampler.instDecidableEqPhase : DecidableEq Phase

@[instance_reducible]

instance Turing.MultiTapePTM.PairSampler.instFintypePhase : Fintype Phase

def Turing.MultiTapePTM.PairSampler.next : Phase → Option Bool → Option Phase

The control state after reading a symbol. The right boundary halts.

def Turing.MultiTapePTM.PairSampler.emit : Phase → Option Bool → Bool → Option Bool

The emitted symbol. Framed symbols are copied, and tail symbols are replaced by the coin.

def Turing.MultiTapePTM.pairSampler : MultiTapePTM 0 Bool PairSampler.Phase

Copy a framed word, then emit one fair bit per remaining input symbol, and halt at the right boundary, without work tapes.

theorem Turing.MultiTapePTM.eval_pairSampler (y r : List Bool) : (pairSampler.runClosed ((MultiTapeTM.frame y ++ r).length + 1) (MultiTapeTM.frame y ++ r)).eval = PMF.map (fun (x : List Bool) => MultiTapeTM.frame y ++ x) (Cslib.BitString.uniformList r.length)

The sampler outputs a uniform certificate after the framed word, in a linear number of transitions.

theorem Turing.MultiTapePTM.pairSampler_halted (y r : List Bool) (final : MultiTapeMachine.Config 0 Bool PairSampler.Phase Empty (MultiTapeTM.frame y ++ r)) : final ∈ (pairSampler.runClosedConfigFrom ((MultiTapeTM.frame y ++ r).length + 1) (MultiTapeMachine.initialConfig pairSampler (MultiTapeTM.frame y ++ r))).eval.support → final.tapes.state = none

Every supported configuration has actually halted by the linear clock.