Strict PPT bounded repetition

Repeated runs are realized by splitting one polynomial-length random tape into independent blocks and mapping the saved-coin evaluator over them. The caller writes an ordinary list traversal, and the certificate charges for the entire encoded result list. Neither the output type nor its encoding needs a finite range.

Main results

• Cslib.Probability.IsPPTOn.replicate, .replicate_bool: collect independent runs.
• Cslib.Probability.IsPPTOn.countTrue: count successful trials in unary.
• Cslib.Probability.IsPPTOn.testProbabilityLT: test a rational acceptance threshold.

References

Adapted from Computability/Probabilistic/Repeat.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using the existing flat-seed law and tidy list calculus.

theorem Cslib.Probability.IsPPTOn.replicate {α β : Type} {input : α ↪ List Bool} {output : β ↪ List Bool} {program : α → ProbComp β} {count : α → ℕ} (hprogram : IsPPTOn input output program) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) : IsPPTOn input (Turing.MultiTapeTM.encList output) fun (a : α) => OracleComp.replicate (count a) (program a)

Collect an efficiently computed number of independent runs. All output framing and storage are charged, including when the number of runs depends on the complete input.

theorem Cslib.Probability.IsPPTOn.replicate_bool {α : Type} {input : α ↪ List Bool} {program : α → ProbComp Bool} {count : α → ℕ} (hprogram : IsPPTOn input Turing.MultiTapeTM.encBool program) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encBits fun (a : α) => OracleComp.replicate (count a) (program a)

Repeated Boolean results may use the raw bit-list encoding.

theorem Cslib.Probability.IsPPTOn.countTrue {α : Type} {input : α ↪ List Bool} {program : α → ProbComp Bool} {count : α → ℕ} (hprogram : IsPPTOn input Turing.MultiTapeTM.encBool program) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encUnary fun (a : α) => OracleComp.countTrue (count a) (program a)

Count successes in independent trials, charging all collected bits and the unary result.

theorem Cslib.Probability.IsPPTOn.testProbabilityLT {α : Type} {input : α ↪ List Bool} {program : α → ProbComp Bool} {count numerator denominator : α → ℕ} (hprogram : IsPPTOn input Turing.MultiTapeTM.encBool program) (hcount : Turing.MultiTapeTM.ComputableTidilyInPolyTime count input Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime numerator input Turing.MultiTapeTM.encUnary) (hdenominator : Turing.MultiTapeTM.ComputableTidilyInPolyTime denominator input Turing.MultiTapeTM.encUnary) : IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => OracleComp.testProbabilityLT (count a) (numerator a) (denominator a) (program a)

Rational threshold testing charges the trial count and every unary cross-product.