Empirical selection of a clipped-vote predictor

Fresh labeled vote samples estimate each dyadic candidate's prediction probability. selectSlope returns a natural numerator for use by clippedPredict; the analytic lower-tail cutoff is never supplied to the program. The error bound combines the lower-tail argument, slope discretization, and empirical selection with explicit losses.

Main definitions

• clippedTrial, selectSlope: validate and select a finite dyadic candidate.
• Parameters.predictionInverseTolerance, .predictionGridBound: explicit polynomial budgets.

Main results

• isPPTOn_selectSlope: charge the complete grid search and its fresh validation samples.
• selectSlope_dense_margin, State.Successful.selectSlope_advantage: transfer the loop's dense-margin guarantee to the selected predictor.

References

[Hol05], Lemma 2.4 and Claim 2.15. Empirical selection over a finite slope grid replaces estimating the analytic cutoff directly. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.clippedTrial (precision numerator : ℕ) (source : ProbComp (List Bool × Bool)) : ProbComp Bool

Test a candidate on one fresh labeled vote sample.

noncomputable def Cslib.Crypto.Pseudoentropy.Boosting.selectSlope (confidence inverseTolerance precision : ℕ) (source : ProbComp (List Bool × Bool)) : ProbComp ℕ

Select a dyadic slope by comparing empirical correctness on fresh labeled samples.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_clippedTrial {α : Type} {input : α ↪ List Bool} {precision numerator : α → ℕ} {source : α → ProbComp (List Bool × Bool)} (hprecision : Turing.MultiTapeTM.ComputableTidilyInPolyTime precision input Turing.MultiTapeTM.encUnary) (hnumerator : Turing.MultiTapeTM.ComputableTidilyInPolyTime numerator input Turing.MultiTapeTM.encUnary) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) : Probability.IsPPTOn input Turing.MultiTapeTM.encBool fun (a : α) => clippedTrial (precision a) (numerator a) (source a)

A certified training sampler and efficient parameters give a strict PPT correctness trial.

theorem Cslib.Crypto.Pseudoentropy.Boosting.isPPTOn_selectSlope {α : Type} {input : α ↪ List Bool} {confidence inverseTolerance precision : α → ℕ} {source : α → ProbComp (List Bool × Bool)} (hconfidence : Turing.MultiTapeTM.ComputableTidilyInPolyTime confidence input Turing.MultiTapeTM.encUnary) (htolerance : Turing.MultiTapeTM.ComputableTidilyInPolyTime inverseTolerance input Turing.MultiTapeTM.encUnary) (hprecision : Turing.MultiTapeTM.ComputableTidilyInPolyTime precision input Turing.MultiTapeTM.encUnary) (hsource : Probability.IsPPTOn input (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBool) source) : Probability.IsPPTOn input Turing.MultiTapeTM.encUnary fun (a : α) => selectSlope (confidence a) (inverseTolerance a) (precision a) (source a)

Selecting a clipped predictor is uniformly strict PPT, including the complete grid search.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.predictionInverseTolerance (params : Parameters) : ℕ

Polynomial inverse tolerance for selecting a predictor, also bounding its final advantage.

def Cslib.Crypto.Pseudoentropy.Boosting.Parameters.predictionGridBound (params : Parameters) : ℕ

A polynomial slope grid fine enough for the maximum possible vote margin.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_predictionInverseTolerance {α : Type} {input : α ↪ List Bool} {params : α → Parameters} (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (params a).predictionInverseTolerance) input Turing.MultiTapeTM.encUnary

The selection tolerance is computed from the encoded parameter record.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.isPolyTime_predictionGridBound {α : Type} {input : α ↪ List Bool} {params : α → Parameters} (hparams : Turing.MultiTapeTM.ComputableTidilyInPolyTime params input encoding) : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (a : α) => (params a).predictionGridBound) input Turing.MultiTapeTM.encUnary

The slope grid is polynomial in the encoded parameter record.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.predictionInverseTolerance_pos (params : Parameters) : 0 < params.predictionInverseTolerance

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.prediction_error_le {params : Parameters} (hparams : params.Valid) : params.delta / 2 - params.gamma * params.delta ^ 3 / 16 + ↑params.clock / (2 * ↑(Probability.dyadicSize params.predictionGridBound)) + 2 / ↑params.predictionInverseTolerance ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance

Explicit polynomial precisions leave an inverse-polynomial advantage after both rounding and empirical selection. The bound deliberately leaves slack for the later reduction.

theorem Cslib.Crypto.Pseudoentropy.Boosting.Parameters.Valid.majority_error_le {params : Parameters} (hparams : params.Valid) : 7 * params.delta / 16 ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance

The same inverse-polynomial advantage also holds on the majority stopping branch.

theorem Cslib.Crypto.Pseudoentropy.Boosting.eval_clippedTrial_true {α : Type} [Fintype α] (precision numerator : ℕ) (source : ProbComp α) (votes : α → List Bool) (truth : α → Bool) : ((clippedTrial precision numerator ((fun (x : α) => (votes x, truth x)) <$> source)).eval true).toReal = 1 - clippedError source.eval (fun (x : α) => BitString.listVoteMargin (votes x) (truth x)) (↑numerator / ↑(Probability.dyadicSize precision))

The executable trial's success probability is one minus the clipped prediction error.

theorem Cslib.Crypto.Pseudoentropy.Boosting.selectSlope_sound {α : Type} [Fintype α] (confidence inverseTolerance precision : ℕ) (htolerance : 0 < inverseTolerance) (source : ProbComp α) (votes : α → List Bool) (truth : α → Bool) : ((selectSlope confidence inverseTolerance precision ((fun (x : α) => (votes x, truth x)) <$> source)).eval.toOuterMeasure {chosen : ℕ | ¬(chosen ≤ Probability.dyadicSize precision ∧ ∀ numerator ≤ Probability.dyadicSize precision, clippedError source.eval (fun (x : α) => BitString.listVoteMargin (votes x) (truth x)) (↑chosen / ↑(Probability.dyadicSize precision)) ≤ clippedError source.eval (fun (x : α) => BitString.listVoteMargin (votes x) (truth x)) (↑numerator / ↑(Probability.dyadicSize precision)) + 2 / ↑inverseTolerance)}).toReal ≤ (↑(Probability.dyadicSize precision) + 1) * (1 / 2) ^ confidence

Except with one estimation failure per grid point, the selected predictor is within twice the tolerance of every dyadic candidate.

theorem Cslib.Crypto.Pseudoentropy.Boosting.selectSlope_dense_margin {α : Type} [Fintype α] (confidence inverseTolerance precision : ℕ) (htolerance : 0 < inverseTolerance) (source : ProbComp α) (votes : α → List Bool) (truth : α → Bool) {δ gap bound : ℝ} (hδ : 0 < δ) (hδone : δ ≤ 1) (hgap : 1 ≤ gap) (hmargin : ∀ (x : α), |BitString.listVoteMargin (votes x) (truth x)| ≤ bound) (hdense : ∀ (softSet : α → ℝ), (∀ (x : α), softSet x ∈ Set.Icc 0 1) → δ ≤ ∑ x : α, (source.eval x).toReal * softSet x → (∑ x : α, (source.eval x).toReal * softSet x) * gap ≤ ∑ x : α, (source.eval x).toReal * (softSet x * BitString.listVoteMargin (votes x) (truth x))) : ((selectSlope confidence inverseTolerance precision ((fun (x : α) => (votes x, truth x)) <$> source)).eval.toOuterMeasure {chosen : ℕ | ¬clippedError source.eval (fun (x : α) => BitString.listVoteMargin (votes x) (truth x)) (↑chosen / ↑(Probability.dyadicSize precision)) ≤ δ / 2 - δ * gap / (2 * bound) + bound / (2 * ↑(Probability.dyadicSize precision)) + 2 / ↑inverseTolerance}).toReal ≤ (↑(Probability.dyadicSize precision) + 1) * (1 / 2) ^ confidence

The empirically selected executable predictor inherits the dense-margin advantage, with explicit dyadic rounding and sampling losses.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.Successful.selectSlope_error {α : Type} [Fintype α] {source : ProbComp α} {observe : α → List Bool} {truth : α → Bool} {evaluate : List Bool → List Bool → Bool} {params : Parameters} {state : State} (hstate : Successful source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state) (hparams : params.Valid) (hbounded : Bounded params.clock params.codeBound state) (hactive : state.stopped = false) (confidence inverseTolerance precision : ℕ) (htolerance : 0 < inverseTolerance) : ((selectSlope confidence inverseTolerance precision (withVotes evaluate ((fun (x : α) => (observe x, truth x)) <$> source) state)).eval.toOuterMeasure {chosen : ℕ | ¬clippedError source.eval (state.margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth) (↑chosen / ↑(Probability.dyadicSize precision)) ≤ params.delta / 2 - params.gamma * params.delta ^ 3 / 16 + ↑params.clock / (2 * ↑(Probability.dyadicSize precision)) + 2 / ↑inverseTolerance}).toReal ≤ (↑(Probability.dyadicSize precision) + 1) * (1 / 2) ^ confidence

On the dense-margin branch of a successful clocked run, empirical selection produces the final clipped predictor with the boosting advantage and explicit approximation losses.

theorem Cslib.Crypto.Pseudoentropy.Boosting.State.Successful.selectSlope_advantage {α : Type} [Fintype α] {source : ProbComp α} {observe : α → List Bool} {truth : α → Bool} {evaluate : List Bool → List Bool → Bool} {params : Parameters} {state : State} (hstate : Successful source.eval (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth params state) (hparams : params.Valid) (hbounded : Bounded params.clock params.codeBound state) (hactive : state.stopped = false) (confidence : ℕ) : ((selectSlope confidence params.predictionInverseTolerance params.predictionGridBound (withVotes evaluate ((fun (x : α) => (observe x, truth x)) <$> source) state)).eval.toOuterMeasure {chosen : ℕ | ¬clippedError source.eval (state.margin (fun (code : List Bool) (x : α) => evaluate code (observe x)) truth) (↑chosen / ↑(Probability.dyadicSize params.predictionGridBound)) ≤ params.delta / 2 - 1 / ↑params.predictionInverseTolerance}).toReal ≤ (↑(Probability.dyadicSize params.predictionGridBound) + 1) * (1 / 2) ^ confidence

With the explicit polynomial grid and tolerance, the final predictor beats δ / 2 by an inverse-polynomial amount. Only the supplied confidence controls selection failure.