Documentation

LeanMlir.Proofs.Certificates.SmoothingCPScorecard

The smoothing CP scorecard — the driver's reported bounds, kernel-checked #

GENERATED by scripts/smooth_scorecard_gen.py from the fixed-protocol driver runs (run_smooth_scorecard.sh: first-100 test images, σ = 0.5, n = 10112 samples, α = 1/1000; CSVs runs/smooth_<slug>_scorecard.csv). Per certified image, the largest 4-decimal q₀ = a/10000 with binomTail n k q₀ ≤ α — verified in exact integer arithmetic at generation AND re-proved here by decide +kernel (binomTail_le_of_kernel_check). Through smoothing_cp_certified_solved, each entry certifies the radius σ·Φ⁻¹(q₀) for its observed count, w.p. ≥ 1−α.

Honest scope: this ties the driver's REPORTED (k, n, α) arithmetic to the theorem. The float Φ⁻¹ printout is closed corpus-wide by the decimal-radius scorecard (SmoothingDecScorecard.lean); the net-semantics hypotheses (C = a net's argmax + hp interiority) are discharged for a concrete trained net in SmoothingNetWitness.lean — this scorecard's own 784-dim driver checkpoints remain untied (the same witness-generator pass at full width).

theorem Proofs.smooth_cp_mlp_i0 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 0: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i1 :

binomTail 10112 10084 (9952 / 10000) ≤ 1 / 1000

img 1: label 2, pred 2, count 10084/10112 → q₀ = 9952/10000, radius ≈ 1.295

theorem Proofs.smooth_cp_mlp_i2 :

binomTail 10112 10104 (9979 / 10000) ≤ 1 / 1000

img 2: label 1, pred 1, count 10104/10112 → q₀ = 9979/10000, radius ≈ 1.431

theorem Proofs.smooth_cp_mlp_i3 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 3: label 0, pred 0, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_mlp_i4 :

binomTail 10112 9654 (9479 / 10000) ≤ 1 / 1000

img 4: label 4, pred 4, count 9654/10112 → q₀ = 9479/10000, radius ≈ 0.812

theorem Proofs.smooth_cp_mlp_i5 :

binomTail 10112 10108 (9985 / 10000) ≤ 1 / 1000

img 5: label 1, pred 1, count 10108/10112 → q₀ = 9985/10000, radius ≈ 1.484

theorem Proofs.smooth_cp_mlp_i6 :

binomTail 10112 9940 (9786 / 10000) ≤ 1 / 1000

img 6: label 4, pred 4, count 9940/10112 → q₀ = 9786/10000, radius ≈ 1.013

theorem Proofs.smooth_cp_mlp_i7 :

binomTail 10112 9637 (9461 / 10000) ≤ 1 / 1000

img 7: label 9, pred 9, count 9637/10112 → q₀ = 9461/10000, radius ≈ 0.804

theorem Proofs.smooth_cp_mlp_i8 :

binomTail 10112 8834 (8631 / 10000) ≤ 1 / 1000

img 8: label 5, pred 5, count 8834/10112 → q₀ = 8631/10000, radius ≈ 0.547

theorem Proofs.smooth_cp_mlp_i9 :

binomTail 10112 9852 (9690 / 10000) ≤ 1 / 1000

img 9: label 9, pred 9, count 9852/10112 → q₀ = 9690/10000, radius ≈ 0.933

theorem Proofs.smooth_cp_mlp_i10 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 10: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i11 :

binomTail 10112 10014 (9869 / 10000) ≤ 1 / 1000

img 11: label 6, pred 6, count 10014/10112 → q₀ = 9869/10000, radius ≈ 1.112

theorem Proofs.smooth_cp_mlp_i12 :

binomTail 10112 10032 (9889 / 10000) ≤ 1 / 1000

img 12: label 9, pred 9, count 10032/10112 → q₀ = 9889/10000, radius ≈ 1.143

theorem Proofs.smooth_cp_mlp_i13 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 13: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i14 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 14: label 1, pred 1, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i15 :

binomTail 10112 9856 (9694 / 10000) ≤ 1 / 1000

img 15: label 5, pred 5, count 9856/10112 → q₀ = 9694/10000, radius ≈ 0.936

theorem Proofs.smooth_cp_mlp_i16 :

binomTail 10112 10015 (9870 / 10000) ≤ 1 / 1000

img 16: label 9, pred 9, count 10015/10112 → q₀ = 9870/10000, radius ≈ 1.113

theorem Proofs.smooth_cp_mlp_i17 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 17: label 7, pred 7, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_mlp_i18 :

binomTail 10112 9872 (9712 / 10000) ≤ 1 / 1000

img 18: label 3, pred 3, count 9872/10112 → q₀ = 9712/10000, radius ≈ 0.949

theorem Proofs.smooth_cp_mlp_i19 :

binomTail 10112 10067 (9931 / 10000) ≤ 1 / 1000

img 19: label 4, pred 4, count 10067/10112 → q₀ = 9931/10000, radius ≈ 1.231

theorem Proofs.smooth_cp_mlp_i20 :

binomTail 10112 9541 (9360 / 10000) ≤ 1 / 1000

img 20: label 9, pred 9, count 9541/10112 → q₀ = 9360/10000, radius ≈ 0.761

theorem Proofs.smooth_cp_mlp_i21 :

binomTail 10112 9268 (9077 / 10000) ≤ 1 / 1000

img 21: label 6, pred 6, count 9268/10112 → q₀ = 9077/10000, radius ≈ 0.663

theorem Proofs.smooth_cp_mlp_i22 :

binomTail 10112 10054 (9915 / 10000) ≤ 1 / 1000

img 22: label 6, pred 6, count 10054/10112 → q₀ = 9915/10000, radius ≈ 1.193

theorem Proofs.smooth_cp_mlp_i23 :

binomTail 10112 10107 (9983 / 10000) ≤ 1 / 1000

img 23: label 5, pred 5, count 10107/10112 → q₀ = 9983/10000, radius ≈ 1.465

theorem Proofs.smooth_cp_mlp_i24 :

binomTail 10112 8868 (8665 / 10000) ≤ 1 / 1000

img 24: label 4, pred 4, count 8868/10112 → q₀ = 8665/10000, radius ≈ 0.555

theorem Proofs.smooth_cp_mlp_i25 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 25: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i26 :

binomTail 10112 10044 (9903 / 10000) ≤ 1 / 1000

img 26: label 7, pred 7, count 10044/10112 → q₀ = 9903/10000, radius ≈ 1.169

theorem Proofs.smooth_cp_mlp_i27 :

binomTail 10112 10009 (9863 / 10000) ≤ 1 / 1000

img 27: label 4, pred 4, count 10009/10112 → q₀ = 9863/10000, radius ≈ 1.103

theorem Proofs.smooth_cp_mlp_i28 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 28: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i29 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 29: label 1, pred 1, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i30 :

binomTail 10112 10102 (9976 / 10000) ≤ 1 / 1000

img 30: label 3, pred 3, count 10102/10112 → q₀ = 9976/10000, radius ≈ 1.410

theorem Proofs.smooth_cp_mlp_i31 :

binomTail 10112 10092 (9962 / 10000) ≤ 1 / 1000

img 31: label 1, pred 1, count 10092/10112 → q₀ = 9962/10000, radius ≈ 1.335

theorem Proofs.smooth_cp_mlp_i32 :

binomTail 10112 10108 (9985 / 10000) ≤ 1 / 1000

img 32: label 3, pred 3, count 10108/10112 → q₀ = 9985/10000, radius ≈ 1.484

theorem Proofs.smooth_cp_mlp_i34 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 34: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i35 :

binomTail 10112 10100 (9973 / 10000) ≤ 1 / 1000

img 35: label 2, pred 2, count 10100/10112 → q₀ = 9973/10000, radius ≈ 1.391

theorem Proofs.smooth_cp_mlp_i36 :

binomTail 10112 10074 (9939 / 10000) ≤ 1 / 1000

img 36: label 7, pred 7, count 10074/10112 → q₀ = 9939/10000, radius ≈ 1.253

theorem Proofs.smooth_cp_mlp_i37 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 37: label 1, pred 1, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_mlp_i38 :

binomTail 10112 7985 (7768 / 10000) ≤ 1 / 1000

img 38: label 2, pred 2, count 7985/10112 → q₀ = 7768/10000, radius ≈ 0.381

theorem Proofs.smooth_cp_mlp_i39 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 39: label 1, pred 1, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i40 :

binomTail 10112 10053 (9914 / 10000) ≤ 1 / 1000

img 40: label 1, pred 1, count 10053/10112 → q₀ = 9914/10000, radius ≈ 1.191

theorem Proofs.smooth_cp_mlp_i41 :

binomTail 10112 10075 (9940 / 10000) ≤ 1 / 1000

img 41: label 7, pred 7, count 10075/10112 → q₀ = 9940/10000, radius ≈ 1.256

theorem Proofs.smooth_cp_mlp_i42 :

binomTail 10112 10070 (9934 / 10000) ≤ 1 / 1000

img 42: label 4, pred 4, count 10070/10112 → q₀ = 9934/10000, radius ≈ 1.239

theorem Proofs.smooth_cp_mlp_i43 :

binomTail 10112 8923 (8722 / 10000) ≤ 1 / 1000

img 43: label 2, pred 2, count 8923/10112 → q₀ = 8722/10000, radius ≈ 0.568

theorem Proofs.smooth_cp_mlp_i44 :

binomTail 10112 8646 (8439 / 10000) ≤ 1 / 1000

img 44: label 3, pred 3, count 8646/10112 → q₀ = 8439/10000, radius ≈ 0.505

theorem Proofs.smooth_cp_mlp_i45 :

binomTail 10112 9775 (9607 / 10000) ≤ 1 / 1000

img 45: label 5, pred 5, count 9775/10112 → q₀ = 9607/10000, radius ≈ 0.879

theorem Proofs.smooth_cp_mlp_i46 :

binomTail 10112 10060 (9922 / 10000) ≤ 1 / 1000

img 46: label 1, pred 1, count 10060/10112 → q₀ = 9922/10000, radius ≈ 1.209

theorem Proofs.smooth_cp_mlp_i47 :

binomTail 10112 9958 (9806 / 10000) ≤ 1 / 1000

img 47: label 2, pred 2, count 9958/10112 → q₀ = 9806/10000, radius ≈ 1.033

theorem Proofs.smooth_cp_mlp_i48 :

binomTail 10112 10098 (9970 / 10000) ≤ 1 / 1000

img 48: label 4, pred 4, count 10098/10112 → q₀ = 9970/10000, radius ≈ 1.374

theorem Proofs.smooth_cp_mlp_i49 :

binomTail 10112 10052 (9913 / 10000) ≤ 1 / 1000

img 49: label 4, pred 4, count 10052/10112 → q₀ = 9913/10000, radius ≈ 1.189

theorem Proofs.smooth_cp_mlp_i50 :

binomTail 10112 10025 (9881 / 10000) ≤ 1 / 1000

img 50: label 6, pred 6, count 10025/10112 → q₀ = 9881/10000, radius ≈ 1.130

theorem Proofs.smooth_cp_mlp_i51 :

binomTail 10112 9999 (9852 / 10000) ≤ 1 / 1000

img 51: label 3, pred 3, count 9999/10112 → q₀ = 9852/10000, radius ≈ 1.088

theorem Proofs.smooth_cp_mlp_i52 :

binomTail 10112 10097 (9969 / 10000) ≤ 1 / 1000

img 52: label 5, pred 5, count 10097/10112 → q₀ = 9969/10000, radius ≈ 1.369

theorem Proofs.smooth_cp_mlp_i53 :

binomTail 10112 9910 (9753 / 10000) ≤ 1 / 1000

img 53: label 5, pred 5, count 9910/10112 → q₀ = 9753/10000, radius ≈ 0.983

theorem Proofs.smooth_cp_mlp_i54 :

binomTail 10112 10110 (9988 / 10000) ≤ 1 / 1000

img 54: label 6, pred 6, count 10110/10112 → q₀ = 9988/10000, radius ≈ 1.518

theorem Proofs.smooth_cp_mlp_i55 :

binomTail 10112 10077 (9943 / 10000) ≤ 1 / 1000

img 55: label 0, pred 0, count 10077/10112 → q₀ = 9943/10000, radius ≈ 1.265

theorem Proofs.smooth_cp_mlp_i56 :

binomTail 10112 10109 (9987 / 10000) ≤ 1 / 1000

img 56: label 4, pred 4, count 10109/10112 → q₀ = 9987/10000, radius ≈ 1.506

theorem Proofs.smooth_cp_mlp_i57 :

binomTail 10112 10102 (9976 / 10000) ≤ 1 / 1000

img 57: label 1, pred 1, count 10102/10112 → q₀ = 9976/10000, radius ≈ 1.410

theorem Proofs.smooth_cp_mlp_i58 :

binomTail 10112 9921 (9765 / 10000) ≤ 1 / 1000

img 58: label 9, pred 9, count 9921/10112 → q₀ = 9765/10000, radius ≈ 0.993

theorem Proofs.smooth_cp_mlp_i59 :

binomTail 10112 9855 (9693 / 10000) ≤ 1 / 1000

img 59: label 5, pred 5, count 9855/10112 → q₀ = 9693/10000, radius ≈ 0.935

theorem Proofs.smooth_cp_mlp_i60 :

binomTail 10112 10108 (9985 / 10000) ≤ 1 / 1000

img 60: label 7, pred 7, count 10108/10112 → q₀ = 9985/10000, radius ≈ 1.484

theorem Proofs.smooth_cp_mlp_i61 :

binomTail 10112 9879 (9719 / 10000) ≤ 1 / 1000

img 61: label 8, pred 8, count 9879/10112 → q₀ = 9719/10000, radius ≈ 0.955

theorem Proofs.smooth_cp_mlp_i62 :

binomTail 10112 6301 (6081 / 10000) ≤ 1 / 1000

img 62: label 9, pred 9, count 6301/10112 → q₀ = 6081/10000, radius ≈ 0.137

theorem Proofs.smooth_cp_mlp_i63 :

binomTail 10112 8178 (7964 / 10000) ≤ 1 / 1000

img 63: label 3, pred 3, count 8178/10112 → q₀ = 7964/10000, radius ≈ 0.414

theorem Proofs.smooth_cp_mlp_i64 :

binomTail 10112 9804 (9638 / 10000) ≤ 1 / 1000

img 64: label 7, pred 7, count 9804/10112 → q₀ = 9638/10000, radius ≈ 0.898

theorem Proofs.smooth_cp_mlp_i65 :

binomTail 10112 7896 (7679 / 10000) ≤ 1 / 1000

img 65: label 4, pred 4, count 7896/10112 → q₀ = 7679/10000, radius ≈ 0.366

theorem Proofs.smooth_cp_mlp_i66 :

binomTail 10112 9518 (9336 / 10000) ≤ 1 / 1000

img 66: label 6, pred 6, count 9518/10112 → q₀ = 9336/10000, radius ≈ 0.752

theorem Proofs.smooth_cp_mlp_i67 :

binomTail 10112 10075 (9940 / 10000) ≤ 1 / 1000

img 67: label 4, pred 4, count 10075/10112 → q₀ = 9940/10000, radius ≈ 1.256

theorem Proofs.smooth_cp_mlp_i68 :

binomTail 10112 10107 (9983 / 10000) ≤ 1 / 1000

img 68: label 3, pred 3, count 10107/10112 → q₀ = 9983/10000, radius ≈ 1.465

theorem Proofs.smooth_cp_mlp_i69 :

binomTail 10112 10108 (9985 / 10000) ≤ 1 / 1000

img 69: label 0, pred 0, count 10108/10112 → q₀ = 9985/10000, radius ≈ 1.484

theorem Proofs.smooth_cp_mlp_i70 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 70: label 7, pred 7, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_mlp_i71 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 71: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i72 :

binomTail 10112 10033 (9890 / 10000) ≤ 1 / 1000

img 72: label 2, pred 2, count 10033/10112 → q₀ = 9890/10000, radius ≈ 1.145

theorem Proofs.smooth_cp_mlp_i73 :

binomTail 10112 5942 (5723 / 10000) ≤ 1 / 1000

img 73: label 9, pred 9, count 5942/10112 → q₀ = 5723/10000, radius ≈ 0.091

theorem Proofs.smooth_cp_mlp_i74 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 74: label 1, pred 1, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i75 :

binomTail 10112 10041 (9900 / 10000) ≤ 1 / 1000

img 75: label 7, pred 7, count 10041/10112 → q₀ = 9900/10000, radius ≈ 1.163

theorem Proofs.smooth_cp_mlp_i76 :

binomTail 10112 10088 (9957 / 10000) ≤ 1 / 1000

img 76: label 3, pred 3, count 10088/10112 → q₀ = 9957/10000, radius ≈ 1.314

theorem Proofs.smooth_cp_mlp_i77 :

binomTail 10112 9297 (9107 / 10000) ≤ 1 / 1000

img 77: label 2, pred 2, count 9297/10112 → q₀ = 9107/10000, radius ≈ 0.673

theorem Proofs.smooth_cp_mlp_i78 :

binomTail 10112 9900 (9742 / 10000) ≤ 1 / 1000

img 78: label 9, pred 9, count 9900/10112 → q₀ = 9742/10000, radius ≈ 0.973

theorem Proofs.smooth_cp_mlp_i79 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 79: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i80 :

binomTail 10112 9088 (8891 / 10000) ≤ 1 / 1000

img 80: label 7, pred 7, count 9088/10112 → q₀ = 8891/10000, radius ≈ 0.611

theorem Proofs.smooth_cp_mlp_i81 :

binomTail 10112 10052 (9913 / 10000) ≤ 1 / 1000

img 81: label 6, pred 6, count 10052/10112 → q₀ = 9913/10000, radius ≈ 1.189

theorem Proofs.smooth_cp_mlp_i82 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 82: label 2, pred 2, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i83 :

binomTail 10112 9978 (9828 / 10000) ≤ 1 / 1000

img 83: label 7, pred 7, count 9978/10112 → q₀ = 9828/10000, radius ≈ 1.058

theorem Proofs.smooth_cp_mlp_i84 :

binomTail 10112 9905 (9748 / 10000) ≤ 1 / 1000

img 84: label 8, pred 8, count 9905/10112 → q₀ = 9748/10000, radius ≈ 0.978

theorem Proofs.smooth_cp_mlp_i85 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 85: label 4, pred 4, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i86 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 86: label 7, pred 7, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_mlp_i87 :

binomTail 10112 9725 (9554 / 10000) ≤ 1 / 1000

img 87: label 3, pred 3, count 9725/10112 → q₀ = 9554/10000, radius ≈ 0.850

theorem Proofs.smooth_cp_mlp_i88 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 88: label 6, pred 6, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_mlp_i89 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 89: label 1, pred 1, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_mlp_i90 :

binomTail 10112 10066 (9929 / 10000) ≤ 1 / 1000

img 90: label 3, pred 3, count 10066/10112 → q₀ = 9929/10000, radius ≈ 1.226

theorem Proofs.smooth_cp_mlp_i91 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 91: label 6, pred 6, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_mlp_i92 :

binomTail 10112 6837 (6615 / 10000) ≤ 1 / 1000

img 92: label 9, pred 9, count 6837/10112 → q₀ = 6615/10000, radius ≈ 0.208

theorem Proofs.smooth_cp_mlp_i93 :

binomTail 10112 10000 (9853 / 10000) ≤ 1 / 1000

img 93: label 3, pred 3, count 10000/10112 → q₀ = 9853/10000, radius ≈ 1.089

theorem Proofs.smooth_cp_mlp_i94 :

binomTail 10112 10108 (9985 / 10000) ≤ 1 / 1000

img 94: label 1, pred 1, count 10108/10112 → q₀ = 9985/10000, radius ≈ 1.484

theorem Proofs.smooth_cp_mlp_i95 :

binomTail 10112 10070 (9934 / 10000) ≤ 1 / 1000

img 95: label 4, pred 4, count 10070/10112 → q₀ = 9934/10000, radius ≈ 1.239

theorem Proofs.smooth_cp_mlp_i96 :

binomTail 10112 9694 (9521 / 10000) ≤ 1 / 1000

img 96: label 1, pred 1, count 9694/10112 → q₀ = 9521/10000, radius ≈ 0.833

theorem Proofs.smooth_cp_mlp_i97 :

binomTail 10112 9990 (9841 / 10000) ≤ 1 / 1000

img 97: label 7, pred 7, count 9990/10112 → q₀ = 9841/10000, radius ≈ 1.073

theorem Proofs.smooth_cp_mlp_i98 :

binomTail 10112 9589 (9411 / 10000) ≤ 1 / 1000

img 98: label 6, pred 6, count 9589/10112 → q₀ = 9411/10000, radius ≈ 0.782

theorem Proofs.smooth_cp_mlp_i99 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 99: label 9, pred 9, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

def Proofs.smoothCpMlpEntries :

List (ℕ × ℕ × ℕ)

MNIST-MLP aggregate: (n, count, a) per certified image.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.smoothCpMlp_certified (e : ℕ × ℕ × ℕ) :

e ∈ smoothCpMlpEntries → binomTail e.1 e.2.1 (↑e.2.2 / 10000) ≤ 1 / 1000

Every MNIST-MLP scorecard entry's tail check is a theorem (99/100 first-100 images certified at σ=0.5, α=1/1000).

theorem Proofs.smooth_cp_cnn_i0 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 0: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i1 :

binomTail 10112 10109 (9987 / 10000) ≤ 1 / 1000

img 1: label 2, pred 2, count 10109/10112 → q₀ = 9987/10000, radius ≈ 1.506

theorem Proofs.smooth_cp_cnn_i2 :

binomTail 10112 10107 (9983 / 10000) ≤ 1 / 1000

img 2: label 1, pred 1, count 10107/10112 → q₀ = 9983/10000, radius ≈ 1.465

theorem Proofs.smooth_cp_cnn_i3 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 3: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i4 :

binomTail 10112 10032 (9889 / 10000) ≤ 1 / 1000

img 4: label 4, pred 4, count 10032/10112 → q₀ = 9889/10000, radius ≈ 1.143

theorem Proofs.smooth_cp_cnn_i5 :

binomTail 10112 10110 (9988 / 10000) ≤ 1 / 1000

img 5: label 1, pred 1, count 10110/10112 → q₀ = 9988/10000, radius ≈ 1.518

theorem Proofs.smooth_cp_cnn_i6 :

binomTail 10112 10084 (9952 / 10000) ≤ 1 / 1000

img 6: label 4, pred 4, count 10084/10112 → q₀ = 9952/10000, radius ≈ 1.295

theorem Proofs.smooth_cp_cnn_i7 :

binomTail 10112 9578 (9399 / 10000) ≤ 1 / 1000

img 7: label 9, pred 9, count 9578/10112 → q₀ = 9399/10000, radius ≈ 0.777

theorem Proofs.smooth_cp_cnn_i8 :

binomTail 10112 10048 (9908 / 10000) ≤ 1 / 1000

img 8: label 5, pred 5, count 10048/10112 → q₀ = 9908/10000, radius ≈ 1.179

theorem Proofs.smooth_cp_cnn_i9 :

binomTail 10112 10019 (9874 / 10000) ≤ 1 / 1000

img 9: label 9, pred 9, count 10019/10112 → q₀ = 9874/10000, radius ≈ 1.119

theorem Proofs.smooth_cp_cnn_i10 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 10: label 0, pred 0, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_cnn_i11 :

binomTail 10112 10107 (9983 / 10000) ≤ 1 / 1000

img 11: label 6, pred 6, count 10107/10112 → q₀ = 9983/10000, radius ≈ 1.465

theorem Proofs.smooth_cp_cnn_i12 :

binomTail 10112 10071 (9935 / 10000) ≤ 1 / 1000

img 12: label 9, pred 9, count 10071/10112 → q₀ = 9935/10000, radius ≈ 1.242

theorem Proofs.smooth_cp_cnn_i13 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 13: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i14 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 14: label 1, pred 1, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i15 :

binomTail 10112 9971 (9820 / 10000) ≤ 1 / 1000

img 15: label 5, pred 5, count 9971/10112 → q₀ = 9820/10000, radius ≈ 1.048

theorem Proofs.smooth_cp_cnn_i16 :

binomTail 10112 10075 (9940 / 10000) ≤ 1 / 1000

img 16: label 9, pred 9, count 10075/10112 → q₀ = 9940/10000, radius ≈ 1.256

theorem Proofs.smooth_cp_cnn_i17 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 17: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i18 :

binomTail 10112 5868 (5650 / 10000) ≤ 1 / 1000

img 18: label 3, pred 3, count 5868/10112 → q₀ = 5650/10000, radius ≈ 0.082

theorem Proofs.smooth_cp_cnn_i19 :

binomTail 10112 10109 (9987 / 10000) ≤ 1 / 1000

img 19: label 4, pred 4, count 10109/10112 → q₀ = 9987/10000, radius ≈ 1.506

theorem Proofs.smooth_cp_cnn_i20 :

binomTail 10112 8093 (7878 / 10000) ≤ 1 / 1000

img 20: label 9, pred 9, count 8093/10112 → q₀ = 7878/10000, radius ≈ 0.399

theorem Proofs.smooth_cp_cnn_i21 :

binomTail 10112 9983 (9834 / 10000) ≤ 1 / 1000

img 21: label 6, pred 6, count 9983/10112 → q₀ = 9834/10000, radius ≈ 1.065

theorem Proofs.smooth_cp_cnn_i22 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 22: label 6, pred 6, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i23 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 23: label 5, pred 5, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i24 :

binomTail 10112 9380 (9193 / 10000) ≤ 1 / 1000

img 24: label 4, pred 4, count 9380/10112 → q₀ = 9193/10000, radius ≈ 0.700

theorem Proofs.smooth_cp_cnn_i25 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 25: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i26 :

binomTail 10112 10106 (9982 / 10000) ≤ 1 / 1000

img 26: label 7, pred 7, count 10106/10112 → q₀ = 9982/10000, radius ≈ 1.456

theorem Proofs.smooth_cp_cnn_i27 :

binomTail 10112 10099 (9971 / 10000) ≤ 1 / 1000

img 27: label 4, pred 4, count 10099/10112 → q₀ = 9971/10000, radius ≈ 1.379

theorem Proofs.smooth_cp_cnn_i28 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 28: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i29 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 29: label 1, pred 1, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i30 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 30: label 3, pred 3, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i31 :

binomTail 10112 10104 (9979 / 10000) ≤ 1 / 1000

img 31: label 1, pred 1, count 10104/10112 → q₀ = 9979/10000, radius ≈ 1.431

theorem Proofs.smooth_cp_cnn_i32 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 32: label 3, pred 3, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_cnn_i33 :

binomTail 10112 6304 (6084 / 10000) ≤ 1 / 1000

img 33: label 4, pred 4, count 6304/10112 → q₀ = 6084/10000, radius ≈ 0.138

theorem Proofs.smooth_cp_cnn_i34 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 34: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i35 :

binomTail 10112 10100 (9973 / 10000) ≤ 1 / 1000

img 35: label 2, pred 2, count 10100/10112 → q₀ = 9973/10000, radius ≈ 1.391

theorem Proofs.smooth_cp_cnn_i36 :

binomTail 10112 10084 (9952 / 10000) ≤ 1 / 1000

img 36: label 7, pred 7, count 10084/10112 → q₀ = 9952/10000, radius ≈ 1.295

theorem Proofs.smooth_cp_cnn_i37 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 37: label 1, pred 1, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_cnn_i38 :

binomTail 10112 8421 (8210 / 10000) ≤ 1 / 1000

img 38: label 2, pred 2, count 8421/10112 → q₀ = 8210/10000, radius ≈ 0.460

theorem Proofs.smooth_cp_cnn_i39 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 39: label 1, pred 1, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_cnn_i40 :

binomTail 10112 10094 (9965 / 10000) ≤ 1 / 1000

img 40: label 1, pred 1, count 10094/10112 → q₀ = 9965/10000, radius ≈ 1.348

theorem Proofs.smooth_cp_cnn_i41 :

binomTail 10112 9907 (9750 / 10000) ≤ 1 / 1000

img 41: label 7, pred 7, count 9907/10112 → q₀ = 9750/10000, radius ≈ 0.980

theorem Proofs.smooth_cp_cnn_i42 :

binomTail 10112 10107 (9983 / 10000) ≤ 1 / 1000

img 42: label 4, pred 4, count 10107/10112 → q₀ = 9983/10000, radius ≈ 1.465

theorem Proofs.smooth_cp_cnn_i43 :

binomTail 10112 10074 (9939 / 10000) ≤ 1 / 1000

img 43: label 2, pred 2, count 10074/10112 → q₀ = 9939/10000, radius ≈ 1.253

theorem Proofs.smooth_cp_cnn_i44 :

binomTail 10112 10033 (9890 / 10000) ≤ 1 / 1000

img 44: label 3, pred 3, count 10033/10112 → q₀ = 9890/10000, radius ≈ 1.145

theorem Proofs.smooth_cp_cnn_i45 :

binomTail 10112 10057 (9919 / 10000) ≤ 1 / 1000

img 45: label 5, pred 5, count 10057/10112 → q₀ = 9919/10000, radius ≈ 1.202

theorem Proofs.smooth_cp_cnn_i46 :

binomTail 10112 10110 (9988 / 10000) ≤ 1 / 1000

img 46: label 1, pred 1, count 10110/10112 → q₀ = 9988/10000, radius ≈ 1.518

theorem Proofs.smooth_cp_cnn_i47 :

binomTail 10112 10110 (9988 / 10000) ≤ 1 / 1000

img 47: label 2, pred 2, count 10110/10112 → q₀ = 9988/10000, radius ≈ 1.518

theorem Proofs.smooth_cp_cnn_i48 :

binomTail 10112 9962 (9810 / 10000) ≤ 1 / 1000

img 48: label 4, pred 4, count 9962/10112 → q₀ = 9810/10000, radius ≈ 1.037

theorem Proofs.smooth_cp_cnn_i49 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 49: label 4, pred 4, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_cnn_i50 :

binomTail 10112 10079 (9945 / 10000) ≤ 1 / 1000

img 50: label 6, pred 6, count 10079/10112 → q₀ = 9945/10000, radius ≈ 1.271

theorem Proofs.smooth_cp_cnn_i51 :

binomTail 10112 10102 (9976 / 10000) ≤ 1 / 1000

img 51: label 3, pred 3, count 10102/10112 → q₀ = 9976/10000, radius ≈ 1.410

theorem Proofs.smooth_cp_cnn_i52 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 52: label 5, pred 5, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i53 :

binomTail 10112 10081 (9948 / 10000) ≤ 1 / 1000

img 53: label 5, pred 5, count 10081/10112 → q₀ = 9948/10000, radius ≈ 1.281

theorem Proofs.smooth_cp_cnn_i54 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 54: label 6, pred 6, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i55 :

binomTail 10112 10107 (9983 / 10000) ≤ 1 / 1000

img 55: label 0, pred 0, count 10107/10112 → q₀ = 9983/10000, radius ≈ 1.465

theorem Proofs.smooth_cp_cnn_i56 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 56: label 4, pred 4, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i57 :

binomTail 10112 10110 (9988 / 10000) ≤ 1 / 1000

img 57: label 1, pred 1, count 10110/10112 → q₀ = 9988/10000, radius ≈ 1.518

theorem Proofs.smooth_cp_cnn_i58 :

binomTail 10112 10099 (9971 / 10000) ≤ 1 / 1000

img 58: label 9, pred 9, count 10099/10112 → q₀ = 9971/10000, radius ≈ 1.379

theorem Proofs.smooth_cp_cnn_i59 :

binomTail 10112 10104 (9979 / 10000) ≤ 1 / 1000

img 59: label 5, pred 5, count 10104/10112 → q₀ = 9979/10000, radius ≈ 1.431

theorem Proofs.smooth_cp_cnn_i60 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 60: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i61 :

binomTail 10112 8137 (7922 / 10000) ≤ 1 / 1000

img 61: label 8, pred 8, count 8137/10112 → q₀ = 7922/10000, radius ≈ 0.407

theorem Proofs.smooth_cp_cnn_i62 :

binomTail 10112 6397 (6176 / 10000) ≤ 1 / 1000

img 62: label 9, pred 9, count 6397/10112 → q₀ = 6176/10000, radius ≈ 0.150

theorem Proofs.smooth_cp_cnn_i63 :

binomTail 10112 8889 (8687 / 10000) ≤ 1 / 1000

img 63: label 3, pred 3, count 8889/10112 → q₀ = 8687/10000, radius ≈ 0.560

theorem Proofs.smooth_cp_cnn_i64 :

binomTail 10112 10078 (9944 / 10000) ≤ 1 / 1000

img 64: label 7, pred 7, count 10078/10112 → q₀ = 9944/10000, radius ≈ 1.268

theorem Proofs.smooth_cp_cnn_i65 :

binomTail 10112 9000 (8801 / 10000) ≤ 1 / 1000

img 65: label 4, pred 4, count 9000/10112 → q₀ = 8801/10000, radius ≈ 0.588

theorem Proofs.smooth_cp_cnn_i66 :

binomTail 10112 10079 (9945 / 10000) ≤ 1 / 1000

img 66: label 6, pred 6, count 10079/10112 → q₀ = 9945/10000, radius ≈ 1.271

theorem Proofs.smooth_cp_cnn_i67 :

binomTail 10112 10109 (9987 / 10000) ≤ 1 / 1000

img 67: label 4, pred 4, count 10109/10112 → q₀ = 9987/10000, radius ≈ 1.506

theorem Proofs.smooth_cp_cnn_i68 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 68: label 3, pred 3, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i69 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 69: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i70 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 70: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i71 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 71: label 0, pred 0, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i72 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 72: label 2, pred 2, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i73 :

binomTail 10112 8030 (7814 / 10000) ≤ 1 / 1000

img 73: label 9, pred 9, count 8030/10112 → q₀ = 7814/10000, radius ≈ 0.388

theorem Proofs.smooth_cp_cnn_i74 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 74: label 1, pred 1, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i75 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 75: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i76 :

binomTail 10112 10097 (9969 / 10000) ≤ 1 / 1000

img 76: label 3, pred 3, count 10097/10112 → q₀ = 9969/10000, radius ≈ 1.369

theorem Proofs.smooth_cp_cnn_i77 :

binomTail 10112 10109 (9987 / 10000) ≤ 1 / 1000

img 77: label 2, pred 2, count 10109/10112 → q₀ = 9987/10000, radius ≈ 1.506

theorem Proofs.smooth_cp_cnn_i78 :

binomTail 10112 10042 (9901 / 10000) ≤ 1 / 1000

img 78: label 9, pred 9, count 10042/10112 → q₀ = 9901/10000, radius ≈ 1.165

theorem Proofs.smooth_cp_cnn_i79 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 79: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i80 :

binomTail 10112 10048 (9908 / 10000) ≤ 1 / 1000

img 80: label 7, pred 7, count 10048/10112 → q₀ = 9908/10000, radius ≈ 1.179

theorem Proofs.smooth_cp_cnn_i81 :

binomTail 10112 10108 (9985 / 10000) ≤ 1 / 1000

img 81: label 6, pred 6, count 10108/10112 → q₀ = 9985/10000, radius ≈ 1.484

theorem Proofs.smooth_cp_cnn_i82 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 82: label 2, pred 2, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i83 :

binomTail 10112 10104 (9979 / 10000) ≤ 1 / 1000

img 83: label 7, pred 7, count 10104/10112 → q₀ = 9979/10000, radius ≈ 1.431

theorem Proofs.smooth_cp_cnn_i84 :

binomTail 10112 10100 (9973 / 10000) ≤ 1 / 1000

img 84: label 8, pred 8, count 10100/10112 → q₀ = 9973/10000, radius ≈ 1.391

theorem Proofs.smooth_cp_cnn_i85 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 85: label 4, pred 4, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i86 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 86: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i87 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 87: label 3, pred 3, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i88 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 88: label 6, pred 6, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i89 :

binomTail 10112 10100 (9973 / 10000) ≤ 1 / 1000

img 89: label 1, pred 1, count 10100/10112 → q₀ = 9973/10000, radius ≈ 1.391

theorem Proofs.smooth_cp_cnn_i90 :

binomTail 10112 10099 (9971 / 10000) ≤ 1 / 1000

img 90: label 3, pred 3, count 10099/10112 → q₀ = 9971/10000, radius ≈ 1.379

theorem Proofs.smooth_cp_cnn_i91 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 91: label 6, pred 6, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i92 :

binomTail 10112 7584 (7364 / 10000) ≤ 1 / 1000

img 92: label 9, pred 9, count 7584/10112 → q₀ = 7364/10000, radius ≈ 0.316

theorem Proofs.smooth_cp_cnn_i93 :

binomTail 10112 10107 (9983 / 10000) ≤ 1 / 1000

img 93: label 3, pred 3, count 10107/10112 → q₀ = 9983/10000, radius ≈ 1.465

theorem Proofs.smooth_cp_cnn_i94 :

binomTail 10112 10110 (9988 / 10000) ≤ 1 / 1000

img 94: label 1, pred 1, count 10110/10112 → q₀ = 9988/10000, radius ≈ 1.518

theorem Proofs.smooth_cp_cnn_i95 :

binomTail 10112 9952 (9799 / 10000) ≤ 1 / 1000

img 95: label 4, pred 4, count 9952/10112 → q₀ = 9799/10000, radius ≈ 1.026

theorem Proofs.smooth_cp_cnn_i96 :

binomTail 10112 10096 (9967 / 10000) ≤ 1 / 1000

img 96: label 1, pred 1, count 10096/10112 → q₀ = 9967/10000, radius ≈ 1.358

theorem Proofs.smooth_cp_cnn_i97 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 97: label 7, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cnn_i98 :

binomTail 10112 10027 (9883 / 10000) ≤ 1 / 1000

img 98: label 6, pred 6, count 10027/10112 → q₀ = 9883/10000, radius ≈ 1.133

theorem Proofs.smooth_cp_cnn_i99 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 99: label 9, pred 9, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

def Proofs.smoothCpCnnEntries :

List (ℕ × ℕ × ℕ)

MNIST-CNN aggregate: (n, count, a) per certified image.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.smoothCpCnn_certified (e : ℕ × ℕ × ℕ) :

e ∈ smoothCpCnnEntries → binomTail e.1 e.2.1 (↑e.2.2 / 10000) ≤ 1 / 1000

Every MNIST-CNN scorecard entry's tail check is a theorem (100/100 first-100 images certified at σ=0.5, α=1/1000).

theorem Proofs.smooth_cp_cifar_i0 :

binomTail 10112 7450 (7230 / 10000) ≤ 1 / 1000

img 0: label 3, pred 3, count 7450/10112 → q₀ = 7230/10000, radius ≈ 0.296

theorem Proofs.smooth_cp_cifar_i1 :

binomTail 10112 8523 (8313 / 10000) ≤ 1 / 1000

img 1: label 8, pred 8, count 8523/10112 → q₀ = 8313/10000, radius ≈ 0.480

theorem Proofs.smooth_cp_cifar_i2 :

binomTail 10112 7393 (7172 / 10000) ≤ 1 / 1000

img 2: label 8, pred 8, count 7393/10112 → q₀ = 7172/10000, radius ≈ 0.287

theorem Proofs.smooth_cp_cifar_i4 :

binomTail 10112 8588 (8380 / 10000) ≤ 1 / 1000

img 4: label 6, pred 6, count 8588/10112 → q₀ = 8380/10000, radius ≈ 0.493

theorem Proofs.smooth_cp_cifar_i5 :

binomTail 10112 10080 (9947 / 10000) ≤ 1 / 1000

img 5: label 6, pred 6, count 10080/10112 → q₀ = 9947/10000, radius ≈ 1.278

theorem Proofs.smooth_cp_cifar_i6 :

binomTail 10112 8779 (8574 / 10000) ≤ 1 / 1000

img 6: label 1, pred 1, count 8779/10112 → q₀ = 8574/10000, radius ≈ 0.534

theorem Proofs.smooth_cp_cifar_i7 :

binomTail 10112 9162 (8967 / 10000) ≤ 1 / 1000

img 7: label 6, pred 6, count 9162/10112 → q₀ = 8967/10000, radius ≈ 0.631

theorem Proofs.smooth_cp_cifar_i8 :

binomTail 10112 8417 (8206 / 10000) ≤ 1 / 1000

img 8: label 3, pred 3, count 8417/10112 → q₀ = 8206/10000, radius ≈ 0.459

theorem Proofs.smooth_cp_cifar_i9 :

binomTail 10112 6098 (5878 / 10000) ≤ 1 / 1000

img 9: label 1, pred 1, count 6098/10112 → q₀ = 5878/10000, radius ≈ 0.111

theorem Proofs.smooth_cp_cifar_i11 :

binomTail 10112 8178 (7964 / 10000) ≤ 1 / 1000

img 11: label 9, pred 9, count 8178/10112 → q₀ = 7964/10000, radius ≈ 0.414

theorem Proofs.smooth_cp_cifar_i13 :

binomTail 10112 9355 (9167 / 10000) ≤ 1 / 1000

img 13: label 7, pred 7, count 9355/10112 → q₀ = 9167/10000, radius ≈ 0.692

theorem Proofs.smooth_cp_cifar_i14 :

binomTail 10112 10069 (9933 / 10000) ≤ 1 / 1000

img 14: label 9, pred 9, count 10069/10112 → q₀ = 9933/10000, radius ≈ 1.236

theorem Proofs.smooth_cp_cifar_i15 :

binomTail 10112 8321 (8108 / 10000) ≤ 1 / 1000

img 15: label 8, pred 8, count 8321/10112 → q₀ = 8108/10000, radius ≈ 0.440

theorem Proofs.smooth_cp_cifar_i16 :

binomTail 10112 5677 (5460 / 10000) ≤ 1 / 1000

img 16: label 5, pred 7, count 5677/10112 → q₀ = 5460/10000, radius ≈ 0.058 (misclassified)

theorem Proofs.smooth_cp_cifar_i18 :

binomTail 10112 9372 (9184 / 10000) ≤ 1 / 1000

img 18: label 8, pred 8, count 9372/10112 → q₀ = 9184/10000, radius ≈ 0.697

theorem Proofs.smooth_cp_cifar_i19 :

binomTail 10112 8335 (8123 / 10000) ≤ 1 / 1000

img 19: label 6, pred 6, count 8335/10112 → q₀ = 8123/10000, radius ≈ 0.443

theorem Proofs.smooth_cp_cifar_i21 :

binomTail 10112 10079 (9945 / 10000) ≤ 1 / 1000

img 21: label 0, pred 2, count 10079/10112 → q₀ = 9945/10000, radius ≈ 1.271 (misclassified)

theorem Proofs.smooth_cp_cifar_i22 :

binomTail 10112 6035 (5816 / 10000) ≤ 1 / 1000

img 22: label 4, pred 2, count 6035/10112 → q₀ = 5816/10000, radius ≈ 0.103 (misclassified)

theorem Proofs.smooth_cp_cifar_i23 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 23: label 9, pred 9, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_cifar_i24 :

binomTail 10112 6084 (5865 / 10000) ≤ 1 / 1000

img 24: label 5, pred 2, count 6084/10112 → q₀ = 5865/10000, radius ≈ 0.109 (misclassified)

theorem Proofs.smooth_cp_cifar_i26 :

binomTail 10112 8952 (8751 / 10000) ≤ 1 / 1000

img 26: label 4, pred 2, count 8952/10112 → q₀ = 8751/10000, radius ≈ 0.575 (misclassified)

theorem Proofs.smooth_cp_cifar_i27 :

binomTail 10112 9261 (9069 / 10000) ≤ 1 / 1000

img 27: label 0, pred 7, count 9261/10112 → q₀ = 9069/10000, radius ≈ 0.661 (misclassified)

theorem Proofs.smooth_cp_cifar_i28 :

binomTail 10112 9962 (9810 / 10000) ≤ 1 / 1000

img 28: label 9, pred 9, count 9962/10112 → q₀ = 9810/10000, radius ≈ 1.037

theorem Proofs.smooth_cp_cifar_i29 :

binomTail 10112 10090 (9959 / 10000) ≤ 1 / 1000

img 29: label 6, pred 6, count 10090/10112 → q₀ = 9959/10000, radius ≈ 1.322

theorem Proofs.smooth_cp_cifar_i30 :

binomTail 10112 5468 (5253 / 10000) ≤ 1 / 1000

img 30: label 6, pred 3, count 5468/10112 → q₀ = 5253/10000, radius ≈ 0.032 (misclassified)

theorem Proofs.smooth_cp_cifar_i31 :

binomTail 10112 5796 (5578 / 10000) ≤ 1 / 1000

img 31: label 5, pred 7, count 5796/10112 → q₀ = 5578/10000, radius ≈ 0.073 (misclassified)

theorem Proofs.smooth_cp_cifar_i32 :

binomTail 10112 7917 (7700 / 10000) ≤ 1 / 1000

img 32: label 4, pred 4, count 7917/10112 → q₀ = 7700/10000, radius ≈ 0.369

theorem Proofs.smooth_cp_cifar_i33 :

binomTail 10112 9534 (9353 / 10000) ≤ 1 / 1000

img 33: label 5, pred 5, count 9534/10112 → q₀ = 9353/10000, radius ≈ 0.758

theorem Proofs.smooth_cp_cifar_i34 :

binomTail 10112 9944 (9790 / 10000) ≤ 1 / 1000

img 34: label 9, pred 9, count 9944/10112 → q₀ = 9790/10000, radius ≈ 1.017

theorem Proofs.smooth_cp_cifar_i35 :

binomTail 10112 6171 (5951 / 10000) ≤ 1 / 1000

img 35: label 2, pred 1, count 6171/10112 → q₀ = 5951/10000, radius ≈ 0.120 (misclassified)

theorem Proofs.smooth_cp_cifar_i37 :

binomTail 10112 10086 (9954 / 10000) ≤ 1 / 1000

img 37: label 1, pred 9, count 10086/10112 → q₀ = 9954/10000, radius ≈ 1.302 (misclassified)

theorem Proofs.smooth_cp_cifar_i38 :

binomTail 10112 9322 (9132 / 10000) ≤ 1 / 1000

img 38: label 9, pred 9, count 9322/10112 → q₀ = 9132/10000, radius ≈ 0.680

theorem Proofs.smooth_cp_cifar_i39 :

binomTail 10112 6397 (6176 / 10000) ≤ 1 / 1000

img 39: label 5, pred 5, count 6397/10112 → q₀ = 6176/10000, radius ≈ 0.150

theorem Proofs.smooth_cp_cifar_i41 :

binomTail 10112 9762 (9594 / 10000) ≤ 1 / 1000

img 41: label 6, pred 6, count 9762/10112 → q₀ = 9594/10000, radius ≈ 0.872

theorem Proofs.smooth_cp_cifar_i42 :

binomTail 10112 9814 (9649 / 10000) ≤ 1 / 1000

img 42: label 5, pred 5, count 9814/10112 → q₀ = 9649/10000, radius ≈ 0.905

theorem Proofs.smooth_cp_cifar_i45 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 45: label 9, pred 9, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597

theorem Proofs.smooth_cp_cifar_i46 :

binomTail 10112 7280 (7059 / 10000) ≤ 1 / 1000

img 46: label 3, pred 3, count 7280/10112 → q₀ = 7059/10000, radius ≈ 0.271

theorem Proofs.smooth_cp_cifar_i47 :

binomTail 10112 9265 (9073 / 10000) ≤ 1 / 1000

img 47: label 9, pred 3, count 9265/10112 → q₀ = 9073/10000, radius ≈ 0.662 (misclassified)

theorem Proofs.smooth_cp_cifar_i48 :

binomTail 10112 6663 (6441 / 10000) ≤ 1 / 1000

img 48: label 7, pred 7, count 6663/10112 → q₀ = 6441/10000, radius ≈ 0.185

theorem Proofs.smooth_cp_cifar_i49 :

binomTail 10112 9133 (8937 / 10000) ≤ 1 / 1000

img 49: label 6, pred 6, count 9133/10112 → q₀ = 8937/10000, radius ≈ 0.623

theorem Proofs.smooth_cp_cifar_i50 :

binomTail 10112 10111 (9990 / 10000) ≤ 1 / 1000

img 50: label 9, pred 9, count 10111/10112 → q₀ = 9990/10000, radius ≈ 1.545

theorem Proofs.smooth_cp_cifar_i51 :

binomTail 10112 8801 (8597 / 10000) ≤ 1 / 1000

img 51: label 8, pred 8, count 8801/10112 → q₀ = 8597/10000, radius ≈ 0.539

theorem Proofs.smooth_cp_cifar_i52 :

binomTail 10112 6753 (6531 / 10000) ≤ 1 / 1000

img 52: label 0, pred 6, count 6753/10112 → q₀ = 6531/10000, radius ≈ 0.197 (misclassified)

theorem Proofs.smooth_cp_cifar_i53 :

binomTail 10112 6708 (6486 / 10000) ≤ 1 / 1000

img 53: label 3, pred 3, count 6708/10112 → q₀ = 6486/10000, radius ≈ 0.191

theorem Proofs.smooth_cp_cifar_i54 :

binomTail 10112 10070 (9934 / 10000) ≤ 1 / 1000

img 54: label 8, pred 8, count 10070/10112 → q₀ = 9934/10000, radius ≈ 1.239

theorem Proofs.smooth_cp_cifar_i55 :

binomTail 10112 9325 (9136 / 10000) ≤ 1 / 1000

img 55: label 8, pred 8, count 9325/10112 → q₀ = 9136/10000, radius ≈ 0.682

theorem Proofs.smooth_cp_cifar_i57 :

binomTail 10112 7337 (7116 / 10000) ≤ 1 / 1000

img 57: label 7, pred 6, count 7337/10112 → q₀ = 7116/10000, radius ≈ 0.279 (misclassified)

theorem Proofs.smooth_cp_cifar_i60 :

binomTail 10112 9476 (9293 / 10000) ≤ 1 / 1000

img 60: label 7, pred 7, count 9476/10112 → q₀ = 9293/10000, radius ≈ 0.735

theorem Proofs.smooth_cp_cifar_i61 :

binomTail 10112 9593 (9415 / 10000) ≤ 1 / 1000

img 61: label 3, pred 3, count 9593/10112 → q₀ = 9415/10000, radius ≈ 0.784

theorem Proofs.smooth_cp_cifar_i62 :

binomTail 10112 7350 (7129 / 10000) ≤ 1 / 1000

img 62: label 6, pred 6, count 7350/10112 → q₀ = 7129/10000, radius ≈ 0.281

theorem Proofs.smooth_cp_cifar_i63 :

binomTail 10112 6552 (6331 / 10000) ≤ 1 / 1000

img 63: label 3, pred 9, count 6552/10112 → q₀ = 6331/10000, radius ≈ 0.170 (misclassified)

theorem Proofs.smooth_cp_cifar_i64 :

binomTail 10112 5929 (5710 / 10000) ≤ 1 / 1000

img 64: label 6, pred 5, count 5929/10112 → q₀ = 5710/10000, radius ≈ 0.089 (misclassified)

theorem Proofs.smooth_cp_cifar_i65 :

binomTail 10112 5867 (5649 / 10000) ≤ 1 / 1000

img 65: label 2, pred 2, count 5867/10112 → q₀ = 5649/10000, radius ≈ 0.082

theorem Proofs.smooth_cp_cifar_i67 :

binomTail 10112 7502 (7282 / 10000) ≤ 1 / 1000

img 67: label 2, pred 2, count 7502/10112 → q₀ = 7282/10000, radius ≈ 0.304

theorem Proofs.smooth_cp_cifar_i68 :

binomTail 10112 10029 (9886 / 10000) ≤ 1 / 1000

img 68: label 3, pred 3, count 10029/10112 → q₀ = 9886/10000, radius ≈ 1.138

theorem Proofs.smooth_cp_cifar_i69 :

binomTail 10112 9890 (9731 / 10000) ≤ 1 / 1000

img 69: label 7, pred 9, count 9890/10112 → q₀ = 9731/10000, radius ≈ 0.964 (misclassified)

theorem Proofs.smooth_cp_cifar_i71 :

binomTail 10112 8795 (8591 / 10000) ≤ 1 / 1000

img 71: label 6, pred 6, count 8795/10112 → q₀ = 8591/10000, radius ≈ 0.538

theorem Proofs.smooth_cp_cifar_i72 :

binomTail 10112 9713 (9541 / 10000) ≤ 1 / 1000

img 72: label 8, pred 8, count 9713/10112 → q₀ = 9541/10000, radius ≈ 0.843

theorem Proofs.smooth_cp_cifar_i73 :

binomTail 10112 10051 (9911 / 10000) ≤ 1 / 1000

img 73: label 8, pred 8, count 10051/10112 → q₀ = 9911/10000, radius ≈ 1.185

theorem Proofs.smooth_cp_cifar_i75 :

binomTail 10112 6649 (6428 / 10000) ≤ 1 / 1000

img 75: label 2, pred 2, count 6649/10112 → q₀ = 6428/10000, radius ≈ 0.183

theorem Proofs.smooth_cp_cifar_i76 :

binomTail 10112 6900 (6678 / 10000) ≤ 1 / 1000

img 76: label 9, pred 9, count 6900/10112 → q₀ = 6678/10000, radius ≈ 0.217

theorem Proofs.smooth_cp_cifar_i77 :

binomTail 10112 9524 (9343 / 10000) ≤ 1 / 1000

img 77: label 3, pred 3, count 9524/10112 → q₀ = 9343/10000, radius ≈ 0.754

theorem Proofs.smooth_cp_cifar_i79 :

binomTail 10112 8466 (8256 / 10000) ≤ 1 / 1000

img 79: label 8, pred 8, count 8466/10112 → q₀ = 8256/10000, radius ≈ 0.468

theorem Proofs.smooth_cp_cifar_i80 :

binomTail 10112 8531 (8322 / 10000) ≤ 1 / 1000

img 80: label 8, pred 8, count 8531/10112 → q₀ = 8322/10000, radius ≈ 0.481

theorem Proofs.smooth_cp_cifar_i81 :

binomTail 10112 7934 (7717 / 10000) ≤ 1 / 1000

img 81: label 1, pred 1, count 7934/10112 → q₀ = 7717/10000, radius ≈ 0.372

theorem Proofs.smooth_cp_cifar_i82 :

binomTail 10112 10080 (9947 / 10000) ≤ 1 / 1000

img 82: label 1, pred 1, count 10080/10112 → q₀ = 9947/10000, radius ≈ 1.278

theorem Proofs.smooth_cp_cifar_i83 :

binomTail 10112 8472 (8262 / 10000) ≤ 1 / 1000

img 83: label 7, pred 7, count 8472/10112 → q₀ = 8262/10000, radius ≈ 0.470

theorem Proofs.smooth_cp_cifar_i84 :

binomTail 10112 6195 (5975 / 10000) ≤ 1 / 1000

img 84: label 2, pred 2, count 6195/10112 → q₀ = 5975/10000, radius ≈ 0.123

theorem Proofs.smooth_cp_cifar_i85 :

binomTail 10112 10112 (9993 / 10000) ≤ 1 / 1000

img 85: label 5, pred 7, count 10112/10112 → q₀ = 9993/10000, radius ≈ 1.597 (misclassified)

theorem Proofs.smooth_cp_cifar_i86 :

binomTail 10112 6211 (5991 / 10000) ≤ 1 / 1000

img 86: label 2, pred 2, count 6211/10112 → q₀ = 5991/10000, radius ≈ 0.126

theorem Proofs.smooth_cp_cifar_i87 :

binomTail 10112 5278 (5065 / 10000) ≤ 1 / 1000

img 87: label 7, pred 8, count 5278/10112 → q₀ = 5065/10000, radius ≈ 0.008 (misclassified)

theorem Proofs.smooth_cp_cifar_i88 :

binomTail 10112 7370 (7149 / 10000) ≤ 1 / 1000

img 88: label 8, pred 8, count 7370/10112 → q₀ = 7149/10000, radius ≈ 0.284

theorem Proofs.smooth_cp_cifar_i89 :

binomTail 10112 9894 (9736 / 10000) ≤ 1 / 1000

img 89: label 9, pred 9, count 9894/10112 → q₀ = 9736/10000, radius ≈ 0.968

theorem Proofs.smooth_cp_cifar_i90 :

binomTail 10112 7817 (7599 / 10000) ≤ 1 / 1000

img 90: label 0, pred 0, count 7817/10112 → q₀ = 7599/10000, radius ≈ 0.353

theorem Proofs.smooth_cp_cifar_i92 :

binomTail 10112 10051 (9911 / 10000) ≤ 1 / 1000

img 92: label 8, pred 8, count 10051/10112 → q₀ = 9911/10000, radius ≈ 1.185

theorem Proofs.smooth_cp_cifar_i93 :

binomTail 10112 6531 (6310 / 10000) ≤ 1 / 1000

img 93: label 6, pred 5, count 6531/10112 → q₀ = 6310/10000, radius ≈ 0.167 (misclassified)

theorem Proofs.smooth_cp_cifar_i95 :

binomTail 10112 6277 (6057 / 10000) ≤ 1 / 1000

img 95: label 6, pred 3, count 6277/10112 → q₀ = 6057/10000, radius ≈ 0.134 (misclassified)

theorem Proofs.smooth_cp_cifar_i96 :

binomTail 10112 7798 (7580 / 10000) ≤ 1 / 1000

img 96: label 6, pred 6, count 7798/10112 → q₀ = 7580/10000, radius ≈ 0.350

theorem Proofs.smooth_cp_cifar_i98 :

binomTail 10112 10005 (9858 / 10000) ≤ 1 / 1000

img 98: label 0, pred 0, count 10005/10112 → q₀ = 9858/10000, radius ≈ 1.096

theorem Proofs.smooth_cp_cifar_i99 :

binomTail 10112 7445 (7225 / 10000) ≤ 1 / 1000

img 99: label 7, pred 7, count 7445/10112 → q₀ = 7225/10000, radius ≈ 0.295

def Proofs.smoothCpCifarEntries :

List (ℕ × ℕ × ℕ)

CIFAR-CNN aggregate: (n, count, a) per certified image.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Proofs.smoothCpCifar_certified (e : ℕ × ℕ × ℕ) :

e ∈ smoothCpCifarEntries → binomTail e.1 e.2.1 (↑e.2.2 / 10000) ≤ 1 / 1000

Every CIFAR-CNN scorecard entry's tail check is a theorem (80/100 first-100 images certified at σ=0.5, α=1/1000).