Research proof index

Singleton bound for arbitrary codes

Hidden-bit decomposition at the SPMF level: the bias of a coin-flip guessing game equals the distinguishing advantage between the two branches, assuming the coin is fair and both branches have full mass (no failure). This is the SPMF analogue of ProbComp.boolBiasAdvantage_eq_boolDistAdvantage_uniformBool_branch. The ProbComp version holds unconditionall...

withStateOracle commutes with <$>: mapping a function over the surface computation is the same as mapping it over the observed SPMF. This holds because interpret is the bundled monad morphism simulateQ', and the StateT observer fun mx => toSPMF (StateT.run' mx s) preserves <$> even though it is not a full monad morphism: <$> does not thr...

Two conditionally independent executions dominate the square of the corresponding single-execution output probability.

Lemma 5.4: Round-by-round soundness of the STIR IOPP Consider parameters: ι = {ιᵢ}_{i = 0, ..., M} be smooth evaluation domains P : Params ι F containing required protocol parameters - initial degree, folding parameters foldingParamᵢ, embedding φᵢ, repetition parameters repeatParamᵢ hParams : ParamConditions ι P, stating conditions that parame...

Selector fibers inside an optional output are disjoint, so their finite sum is bounded by the probability of returning any some value.