Documentation

LeanMlir.Proofs.Certificates.SmoothingDecScorecard

The smoothing DECIMAL-radius scorecard — Φ⁻¹ leaves symbolic-land, corpus-wide #

GENERATED by scripts/smooth_dec_scorecard_gen.py from the same fixed-protocol driver runs as SmoothingCPScorecard.lean (first-100 test images, σ = 0.5, n = 10112, α = 1/1000; identical per-image q₀ = a/10000). The CP scorecard's radius column σ·Φ⁻¹(q₀) was display-only float; here each certified image gets a PROVED decimal lower bound: m/2000 ≤ σ·Φ⁻¹(a/10000) via smooth_radius_dec.

The trick that makes 279 images affordable: phiScanLit_eq kernel-evaluates the ENTIRE h = 1/1000 upper-Riemann grid (phiScanRev, 3300 panels, descending, ~2 min total); each per-image check is then a single O(index) list lookup — into the SMALLEST verified prefix covering its m, so a decide +kernel walks one 551-entry chunk, never the whole grid (milliseconds each, and the module stays ~2 GB where full-literal lookups accumulated 11.3 GB — kernel memory is not reclaimed between declarations). The grid is verified in CHUNKS of 550 panels, one MODULE each (SmoothingDecChunk1–6: phiScanRevFrom continued from literal checkpoints, glued by phiScanRevFrom_append): one whole-grid declaration retains ~15 GB of kernel-cache bignums and OOMs 16 GB CI runners, and memory is not reclaimed between declarations within a lean process — per-module processes cap the worst chunk at ~5 GB. Per image, m is the LARGEST grid index with phiGridUB (1/1000) m ≤ q₀, so the bound is grid-optimal; the intrinsic upper-sum slack costs ~0.003–0.036 vs the driver's float printout (largest at the q₀ = 0.9993 unanimous-count images).

Honest scope: the net-semantics hypotheses (C = a net's argmax + hp interiority) are discharged for a concrete trained net in SmoothingNetWitness.lean; the scorecard's own 784-dim driver checkpoints remain untied (the same witness-generator pass at full width).

def Proofs.phiScanNum :

The FULL scan literal's numerators: entry i is phiGridUB (1/1000) (3300 − i) (descending) over 10¹².

Equations

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

Instances For

def Proofs.phiScanLit :

The scan literal: the ℕ numerators over 10¹².

Equations

Proofs.phiScanLit = List.map (fun (n : ℚ) => n / 1000000000000) do let a ← Proofs.phiScanNum pure ↑a

Instances For

theorem Proofs.phiScanLit_eq :

phiScanRev (1 / 1000) 3300 = phiScanLit

The whole grid scan against the flat literal (chunks reassembled; the final decide is literal-vs-literal, no panel arithmetic).

theorem Proofs.smooth_dec_mlp_i0 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 0: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i1 :

2576 / 2000 ≤ 1 / 2 * stdNormalQuantile (9952 / 10000)

img 1: label 2, pred 2, q₀ = 9952/10000 → radius ≥ 2576/2000 = 1.2880 (driver float: 1.295)

theorem Proofs.smooth_dec_mlp_i2 :

2834 / 2000 ≤ 1 / 2 * stdNormalQuantile (9979 / 10000)

img 2: label 1, pred 1, q₀ = 9979/10000 → radius ≥ 2834/2000 = 1.4170 (driver float: 1.431)

theorem Proofs.smooth_dec_mlp_i3 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 3: label 0, pred 0, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_mlp_i4 :

1623 / 2000 ≤ 1 / 2 * stdNormalQuantile (9479 / 10000)

img 4: label 4, pred 4, q₀ = 9479/10000 → radius ≥ 1623/2000 = 0.8115 (driver float: 0.812)

theorem Proofs.smooth_dec_mlp_i5 :

2929 / 2000 ≤ 1 / 2 * stdNormalQuantile (9985 / 10000)

img 5: label 1, pred 1, q₀ = 9985/10000 → radius ≥ 2929/2000 = 1.4645 (driver float: 1.484)

theorem Proofs.smooth_dec_mlp_i6 :

2022 / 2000 ≤ 1 / 2 * stdNormalQuantile (9786 / 10000)

img 6: label 4, pred 4, q₀ = 9786/10000 → radius ≥ 2022/2000 = 1.0110 (driver float: 1.013)

theorem Proofs.smooth_dec_mlp_i7 :

1606 / 2000 ≤ 1 / 2 * stdNormalQuantile (9461 / 10000)

img 7: label 9, pred 9, q₀ = 9461/10000 → radius ≥ 1606/2000 = 0.8030 (driver float: 0.804)

theorem Proofs.smooth_dec_mlp_i8 :

1093 / 2000 ≤ 1 / 2 * stdNormalQuantile (8631 / 10000)

img 8: label 5, pred 5, q₀ = 8631/10000 → radius ≥ 1093/2000 = 0.5465 (driver float: 0.547)

theorem Proofs.smooth_dec_mlp_i9 :

1863 / 2000 ≤ 1 / 2 * stdNormalQuantile (9690 / 10000)

img 9: label 9, pred 9, q₀ = 9690/10000 → radius ≥ 1863/2000 = 0.9315 (driver float: 0.933)

theorem Proofs.smooth_dec_mlp_i10 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 10: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i11 :

2217 / 2000 ≤ 1 / 2 * stdNormalQuantile (9869 / 10000)

img 11: label 6, pred 6, q₀ = 9869/10000 → radius ≥ 2217/2000 = 1.1085 (driver float: 1.112)

theorem Proofs.smooth_dec_mlp_i12 :

2280 / 2000 ≤ 1 / 2 * stdNormalQuantile (9889 / 10000)

img 12: label 9, pred 9, q₀ = 9889/10000 → radius ≥ 2280/2000 = 1.1400 (driver float: 1.143)

theorem Proofs.smooth_dec_mlp_i13 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 13: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i14 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 14: label 1, pred 1, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i15 :

1869 / 2000 ≤ 1 / 2 * stdNormalQuantile (9694 / 10000)

img 15: label 5, pred 5, q₀ = 9694/10000 → radius ≥ 1869/2000 = 0.9345 (driver float: 0.936)

theorem Proofs.smooth_dec_mlp_i16 :

2220 / 2000 ≤ 1 / 2 * stdNormalQuantile (9870 / 10000)

img 16: label 9, pred 9, q₀ = 9870/10000 → radius ≥ 2220/2000 = 1.1100 (driver float: 1.113)

theorem Proofs.smooth_dec_mlp_i17 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 17: label 7, pred 7, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_mlp_i18 :

1896 / 2000 ≤ 1 / 2 * stdNormalQuantile (9712 / 10000)

img 18: label 3, pred 3, q₀ = 9712/10000 → radius ≥ 1896/2000 = 0.9480 (driver float: 0.949)

theorem Proofs.smooth_dec_mlp_i19 :

2452 / 2000 ≤ 1 / 2 * stdNormalQuantile (9931 / 10000)

img 19: label 4, pred 4, q₀ = 9931/10000 → radius ≥ 2452/2000 = 1.2260 (driver float: 1.231)

theorem Proofs.smooth_dec_mlp_i20 :

1520 / 2000 ≤ 1 / 2 * stdNormalQuantile (9360 / 10000)

img 20: label 9, pred 9, q₀ = 9360/10000 → radius ≥ 1520/2000 = 0.7600 (driver float: 0.761)

theorem Proofs.smooth_dec_mlp_i21 :

1326 / 2000 ≤ 1 / 2 * stdNormalQuantile (9077 / 10000)

img 21: label 6, pred 6, q₀ = 9077/10000 → radius ≥ 1326/2000 = 0.6630 (driver float: 0.663)

theorem Proofs.smooth_dec_mlp_i22 :

2378 / 2000 ≤ 1 / 2 * stdNormalQuantile (9915 / 10000)

img 22: label 6, pred 6, q₀ = 9915/10000 → radius ≥ 2378/2000 = 1.1890 (driver float: 1.193)

theorem Proofs.smooth_dec_mlp_i23 :

2894 / 2000 ≤ 1 / 2 * stdNormalQuantile (9983 / 10000)

img 23: label 5, pred 5, q₀ = 9983/10000 → radius ≥ 2894/2000 = 1.4470 (driver float: 1.465)

theorem Proofs.smooth_dec_mlp_i24 :

1109 / 2000 ≤ 1 / 2 * stdNormalQuantile (8665 / 10000)

img 24: label 4, pred 4, q₀ = 8665/10000 → radius ≥ 1109/2000 = 0.5545 (driver float: 0.555)

theorem Proofs.smooth_dec_mlp_i25 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 25: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i26 :

2330 / 2000 ≤ 1 / 2 * stdNormalQuantile (9903 / 10000)

img 26: label 7, pred 7, q₀ = 9903/10000 → radius ≥ 2330/2000 = 1.1650 (driver float: 1.169)

theorem Proofs.smooth_dec_mlp_i27 :

2200 / 2000 ≤ 1 / 2 * stdNormalQuantile (9863 / 10000)

img 27: label 4, pred 4, q₀ = 9863/10000 → radius ≥ 2200/2000 = 1.1000 (driver float: 1.103)

theorem Proofs.smooth_dec_mlp_i28 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 28: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i29 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 29: label 1, pred 1, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i30 :

2794 / 2000 ≤ 1 / 2 * stdNormalQuantile (9976 / 10000)

img 30: label 3, pred 3, q₀ = 9976/10000 → radius ≥ 2794/2000 = 1.3970 (driver float: 1.410)

theorem Proofs.smooth_dec_mlp_i31 :

2652 / 2000 ≤ 1 / 2 * stdNormalQuantile (9962 / 10000)

img 31: label 1, pred 1, q₀ = 9962/10000 → radius ≥ 2652/2000 = 1.3260 (driver float: 1.335)

theorem Proofs.smooth_dec_mlp_i32 :

2929 / 2000 ≤ 1 / 2 * stdNormalQuantile (9985 / 10000)

img 32: label 3, pred 3, q₀ = 9985/10000 → radius ≥ 2929/2000 = 1.4645 (driver float: 1.484)

theorem Proofs.smooth_dec_mlp_i34 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 34: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i35 :

2759 / 2000 ≤ 1 / 2 * stdNormalQuantile (9973 / 10000)

img 35: label 2, pred 2, q₀ = 9973/10000 → radius ≥ 2759/2000 = 1.3795 (driver float: 1.391)

theorem Proofs.smooth_dec_mlp_i36 :

2495 / 2000 ≤ 1 / 2 * stdNormalQuantile (9939 / 10000)

img 36: label 7, pred 7, q₀ = 9939/10000 → radius ≥ 2495/2000 = 1.2475 (driver float: 1.253)

theorem Proofs.smooth_dec_mlp_i37 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 37: label 1, pred 1, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_mlp_i38 :

761 / 2000 ≤ 1 / 2 * stdNormalQuantile (7768 / 10000)

img 38: label 2, pred 2, q₀ = 7768/10000 → radius ≥ 761/2000 = 0.3805 (driver float: 0.381)

theorem Proofs.smooth_dec_mlp_i39 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 39: label 1, pred 1, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i40 :

2374 / 2000 ≤ 1 / 2 * stdNormalQuantile (9914 / 10000)

img 40: label 1, pred 1, q₀ = 9914/10000 → radius ≥ 2374/2000 = 1.1870 (driver float: 1.191)

theorem Proofs.smooth_dec_mlp_i41 :

2501 / 2000 ≤ 1 / 2 * stdNormalQuantile (9940 / 10000)

img 41: label 7, pred 7, q₀ = 9940/10000 → radius ≥ 2501/2000 = 1.2505 (driver float: 1.256)

theorem Proofs.smooth_dec_mlp_i42 :

2468 / 2000 ≤ 1 / 2 * stdNormalQuantile (9934 / 10000)

img 42: label 4, pred 4, q₀ = 9934/10000 → radius ≥ 2468/2000 = 1.2340 (driver float: 1.239)

theorem Proofs.smooth_dec_mlp_i43 :

1136 / 2000 ≤ 1 / 2 * stdNormalQuantile (8722 / 10000)

img 43: label 2, pred 2, q₀ = 8722/10000 → radius ≥ 1136/2000 = 0.5680 (driver float: 0.568)

theorem Proofs.smooth_dec_mlp_i44 :

1010 / 2000 ≤ 1 / 2 * stdNormalQuantile (8439 / 10000)

img 44: label 3, pred 3, q₀ = 8439/10000 → radius ≥ 1010/2000 = 0.5050 (driver float: 0.505)

theorem Proofs.smooth_dec_mlp_i45 :

1757 / 2000 ≤ 1 / 2 * stdNormalQuantile (9607 / 10000)

img 45: label 5, pred 5, q₀ = 9607/10000 → radius ≥ 1757/2000 = 0.8785 (driver float: 0.879)

theorem Proofs.smooth_dec_mlp_i46 :

2409 / 2000 ≤ 1 / 2 * stdNormalQuantile (9922 / 10000)

img 46: label 1, pred 1, q₀ = 9922/10000 → radius ≥ 2409/2000 = 1.2045 (driver float: 1.209)

theorem Proofs.smooth_dec_mlp_i47 :

2062 / 2000 ≤ 1 / 2 * stdNormalQuantile (9806 / 10000)

img 47: label 2, pred 2, q₀ = 9806/10000 → radius ≥ 2062/2000 = 1.0310 (driver float: 1.033)

theorem Proofs.smooth_dec_mlp_i48 :

2727 / 2000 ≤ 1 / 2 * stdNormalQuantile (9970 / 10000)

img 48: label 4, pred 4, q₀ = 9970/10000 → radius ≥ 2727/2000 = 1.3635 (driver float: 1.374)

theorem Proofs.smooth_dec_mlp_i49 :

2370 / 2000 ≤ 1 / 2 * stdNormalQuantile (9913 / 10000)

img 49: label 4, pred 4, q₀ = 9913/10000 → radius ≥ 2370/2000 = 1.1850 (driver float: 1.189)

theorem Proofs.smooth_dec_mlp_i50 :

2254 / 2000 ≤ 1 / 2 * stdNormalQuantile (9881 / 10000)

img 50: label 6, pred 6, q₀ = 9881/10000 → radius ≥ 2254/2000 = 1.1270 (driver float: 1.130)

theorem Proofs.smooth_dec_mlp_i51 :

2170 / 2000 ≤ 1 / 2 * stdNormalQuantile (9852 / 10000)

img 51: label 3, pred 3, q₀ = 9852/10000 → radius ≥ 2170/2000 = 1.0850 (driver float: 1.088)

theorem Proofs.smooth_dec_mlp_i52 :

2716 / 2000 ≤ 1 / 2 * stdNormalQuantile (9969 / 10000)

img 52: label 5, pred 5, q₀ = 9969/10000 → radius ≥ 2716/2000 = 1.3580 (driver float: 1.369)

theorem Proofs.smooth_dec_mlp_i53 :

1962 / 2000 ≤ 1 / 2 * stdNormalQuantile (9753 / 10000)

img 53: label 5, pred 5, q₀ = 9753/10000 → radius ≥ 1962/2000 = 0.9810 (driver float: 0.983)

theorem Proofs.smooth_dec_mlp_i54 :

2989 / 2000 ≤ 1 / 2 * stdNormalQuantile (9988 / 10000)

img 54: label 6, pred 6, q₀ = 9988/10000 → radius ≥ 2989/2000 = 1.4945 (driver float: 1.518)

theorem Proofs.smooth_dec_mlp_i55 :

2518 / 2000 ≤ 1 / 2 * stdNormalQuantile (9943 / 10000)

img 55: label 0, pred 0, q₀ = 9943/10000 → radius ≥ 2518/2000 = 1.2590 (driver float: 1.265)

theorem Proofs.smooth_dec_mlp_i56 :

2968 / 2000 ≤ 1 / 2 * stdNormalQuantile (9987 / 10000)

img 56: label 4, pred 4, q₀ = 9987/10000 → radius ≥ 2968/2000 = 1.4840 (driver float: 1.506)

theorem Proofs.smooth_dec_mlp_i57 :

2794 / 2000 ≤ 1 / 2 * stdNormalQuantile (9976 / 10000)

img 57: label 1, pred 1, q₀ = 9976/10000 → radius ≥ 2794/2000 = 1.3970 (driver float: 1.410)

theorem Proofs.smooth_dec_mlp_i58 :

1983 / 2000 ≤ 1 / 2 * stdNormalQuantile (9765 / 10000)

img 58: label 9, pred 9, q₀ = 9765/10000 → radius ≥ 1983/2000 = 0.9915 (driver float: 0.993)

theorem Proofs.smooth_dec_mlp_i59 :

1868 / 2000 ≤ 1 / 2 * stdNormalQuantile (9693 / 10000)

img 59: label 5, pred 5, q₀ = 9693/10000 → radius ≥ 1868/2000 = 0.9340 (driver float: 0.935)

theorem Proofs.smooth_dec_mlp_i60 :

2929 / 2000 ≤ 1 / 2 * stdNormalQuantile (9985 / 10000)

img 60: label 7, pred 7, q₀ = 9985/10000 → radius ≥ 2929/2000 = 1.4645 (driver float: 1.484)

theorem Proofs.smooth_dec_mlp_i61 :

1906 / 2000 ≤ 1 / 2 * stdNormalQuantile (9719 / 10000)

img 61: label 8, pred 8, q₀ = 9719/10000 → radius ≥ 1906/2000 = 0.9530 (driver float: 0.955)

theorem Proofs.smooth_dec_mlp_i62 :

274 / 2000 ≤ 1 / 2 * stdNormalQuantile (6081 / 10000)

img 62: label 9, pred 9, q₀ = 6081/10000 → radius ≥ 274/2000 = 0.1370 (driver float: 0.137)

theorem Proofs.smooth_dec_mlp_i63 :

828 / 2000 ≤ 1 / 2 * stdNormalQuantile (7964 / 10000)

img 63: label 3, pred 3, q₀ = 7964/10000 → radius ≥ 828/2000 = 0.4140 (driver float: 0.414)

theorem Proofs.smooth_dec_mlp_i64 :

1794 / 2000 ≤ 1 / 2 * stdNormalQuantile (9638 / 10000)

img 64: label 7, pred 7, q₀ = 9638/10000 → radius ≥ 1794/2000 = 0.8970 (driver float: 0.898)

theorem Proofs.smooth_dec_mlp_i65 :

731 / 2000 ≤ 1 / 2 * stdNormalQuantile (7679 / 10000)

img 65: label 4, pred 4, q₀ = 7679/10000 → radius ≥ 731/2000 = 0.3655 (driver float: 0.366)

theorem Proofs.smooth_dec_mlp_i66 :

1502 / 2000 ≤ 1 / 2 * stdNormalQuantile (9336 / 10000)

img 66: label 6, pred 6, q₀ = 9336/10000 → radius ≥ 1502/2000 = 0.7510 (driver float: 0.752)

theorem Proofs.smooth_dec_mlp_i67 :

2501 / 2000 ≤ 1 / 2 * stdNormalQuantile (9940 / 10000)

img 67: label 4, pred 4, q₀ = 9940/10000 → radius ≥ 2501/2000 = 1.2505 (driver float: 1.256)

theorem Proofs.smooth_dec_mlp_i68 :

2894 / 2000 ≤ 1 / 2 * stdNormalQuantile (9983 / 10000)

img 68: label 3, pred 3, q₀ = 9983/10000 → radius ≥ 2894/2000 = 1.4470 (driver float: 1.465)

theorem Proofs.smooth_dec_mlp_i69 :

2929 / 2000 ≤ 1 / 2 * stdNormalQuantile (9985 / 10000)

img 69: label 0, pred 0, q₀ = 9985/10000 → radius ≥ 2929/2000 = 1.4645 (driver float: 1.484)

theorem Proofs.smooth_dec_mlp_i70 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 70: label 7, pred 7, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_mlp_i71 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 71: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i72 :

2284 / 2000 ≤ 1 / 2 * stdNormalQuantile (9890 / 10000)

img 72: label 2, pred 2, q₀ = 9890/10000 → radius ≥ 2284/2000 = 1.1420 (driver float: 1.145)

theorem Proofs.smooth_dec_mlp_i73 :

182 / 2000 ≤ 1 / 2 * stdNormalQuantile (5723 / 10000)

img 73: label 9, pred 9, q₀ = 5723/10000 → radius ≥ 182/2000 = 0.0910 (driver float: 0.091)

theorem Proofs.smooth_dec_mlp_i74 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 74: label 1, pred 1, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i75 :

2319 / 2000 ≤ 1 / 2 * stdNormalQuantile (9900 / 10000)

img 75: label 7, pred 7, q₀ = 9900/10000 → radius ≥ 2319/2000 = 1.1595 (driver float: 1.163)

theorem Proofs.smooth_dec_mlp_i76 :

2612 / 2000 ≤ 1 / 2 * stdNormalQuantile (9957 / 10000)

img 76: label 3, pred 3, q₀ = 9957/10000 → radius ≥ 2612/2000 = 1.3060 (driver float: 1.314)

theorem Proofs.smooth_dec_mlp_i77 :

1344 / 2000 ≤ 1 / 2 * stdNormalQuantile (9107 / 10000)

img 77: label 2, pred 2, q₀ = 9107/10000 → radius ≥ 1344/2000 = 0.6720 (driver float: 0.673)

theorem Proofs.smooth_dec_mlp_i78 :

1943 / 2000 ≤ 1 / 2 * stdNormalQuantile (9742 / 10000)

img 78: label 9, pred 9, q₀ = 9742/10000 → radius ≥ 1943/2000 = 0.9715 (driver float: 0.973)

theorem Proofs.smooth_dec_mlp_i79 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 79: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i80 :

1221 / 2000 ≤ 1 / 2 * stdNormalQuantile (8891 / 10000)

img 80: label 7, pred 7, q₀ = 8891/10000 → radius ≥ 1221/2000 = 0.6105 (driver float: 0.611)

theorem Proofs.smooth_dec_mlp_i81 :

2370 / 2000 ≤ 1 / 2 * stdNormalQuantile (9913 / 10000)

img 81: label 6, pred 6, q₀ = 9913/10000 → radius ≥ 2370/2000 = 1.1850 (driver float: 1.189)

theorem Proofs.smooth_dec_mlp_i82 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 82: label 2, pred 2, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i83 :

2111 / 2000 ≤ 1 / 2 * stdNormalQuantile (9828 / 10000)

img 83: label 7, pred 7, q₀ = 9828/10000 → radius ≥ 2111/2000 = 1.0555 (driver float: 1.058)

theorem Proofs.smooth_dec_mlp_i84 :

1953 / 2000 ≤ 1 / 2 * stdNormalQuantile (9748 / 10000)

img 84: label 8, pred 8, q₀ = 9748/10000 → radius ≥ 1953/2000 = 0.9765 (driver float: 0.978)

theorem Proofs.smooth_dec_mlp_i85 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 85: label 4, pred 4, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i86 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 86: label 7, pred 7, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_mlp_i87 :

1698 / 2000 ≤ 1 / 2 * stdNormalQuantile (9554 / 10000)

img 87: label 3, pred 3, q₀ = 9554/10000 → radius ≥ 1698/2000 = 0.8490 (driver float: 0.850)

theorem Proofs.smooth_dec_mlp_i88 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 88: label 6, pred 6, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_mlp_i89 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 89: label 1, pred 1, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_mlp_i90 :

2442 / 2000 ≤ 1 / 2 * stdNormalQuantile (9929 / 10000)

img 90: label 3, pred 3, q₀ = 9929/10000 → radius ≥ 2442/2000 = 1.2210 (driver float: 1.226)

theorem Proofs.smooth_dec_mlp_i91 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 91: label 6, pred 6, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_mlp_i92 :

416 / 2000 ≤ 1 / 2 * stdNormalQuantile (6615 / 10000)

img 92: label 9, pred 9, q₀ = 6615/10000 → radius ≥ 416/2000 = 0.2080 (driver float: 0.208)

theorem Proofs.smooth_dec_mlp_i93 :

2173 / 2000 ≤ 1 / 2 * stdNormalQuantile (9853 / 10000)

img 93: label 3, pred 3, q₀ = 9853/10000 → radius ≥ 2173/2000 = 1.0865 (driver float: 1.089)

theorem Proofs.smooth_dec_mlp_i94 :

2929 / 2000 ≤ 1 / 2 * stdNormalQuantile (9985 / 10000)

img 94: label 1, pred 1, q₀ = 9985/10000 → radius ≥ 2929/2000 = 1.4645 (driver float: 1.484)

theorem Proofs.smooth_dec_mlp_i95 :

2468 / 2000 ≤ 1 / 2 * stdNormalQuantile (9934 / 10000)

img 95: label 4, pred 4, q₀ = 9934/10000 → radius ≥ 2468/2000 = 1.2340 (driver float: 1.239)

theorem Proofs.smooth_dec_mlp_i96 :

1664 / 2000 ≤ 1 / 2 * stdNormalQuantile (9521 / 10000)

img 96: label 1, pred 1, q₀ = 9521/10000 → radius ≥ 1664/2000 = 0.8320 (driver float: 0.833)

theorem Proofs.smooth_dec_mlp_i97 :

2142 / 2000 ≤ 1 / 2 * stdNormalQuantile (9841 / 10000)

img 97: label 7, pred 7, q₀ = 9841/10000 → radius ≥ 2142/2000 = 1.0710 (driver float: 1.073)

theorem Proofs.smooth_dec_mlp_i98 :

1562 / 2000 ≤ 1 / 2 * stdNormalQuantile (9411 / 10000)

img 98: label 6, pred 6, q₀ = 9411/10000 → radius ≥ 1562/2000 = 0.7810 (driver float: 0.782)

theorem Proofs.smooth_dec_mlp_i99 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 99: label 9, pred 9, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

def Proofs.smoothDecMlpEntries :

List (ℕ × ℕ)

MNIST-MLP aggregate: (m, a) per certified image — decimal radius m/2000 for q₀ = a/10000.

Equations

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

Instances For

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

e ∈ smoothDecMlpEntries → ↑e.1 / 2000 ≤ 1 / 2 * stdNormalQuantile (↑e.2 / 10000)

Every MNIST-MLP scorecard image's decimal radius is a theorem: m/2000 ≤ σ·Φ⁻¹(a/10000).

theorem Proofs.smooth_dec_cnn_i0 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 0: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i1 :

2968 / 2000 ≤ 1 / 2 * stdNormalQuantile (9987 / 10000)

img 1: label 2, pred 2, q₀ = 9987/10000 → radius ≥ 2968/2000 = 1.4840 (driver float: 1.506)

theorem Proofs.smooth_dec_cnn_i2 :

2894 / 2000 ≤ 1 / 2 * stdNormalQuantile (9983 / 10000)

img 2: label 1, pred 1, q₀ = 9983/10000 → radius ≥ 2894/2000 = 1.4470 (driver float: 1.465)

theorem Proofs.smooth_dec_cnn_i3 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 3: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i4 :

2280 / 2000 ≤ 1 / 2 * stdNormalQuantile (9889 / 10000)

img 4: label 4, pred 4, q₀ = 9889/10000 → radius ≥ 2280/2000 = 1.1400 (driver float: 1.143)

theorem Proofs.smooth_dec_cnn_i5 :

2989 / 2000 ≤ 1 / 2 * stdNormalQuantile (9988 / 10000)

img 5: label 1, pred 1, q₀ = 9988/10000 → radius ≥ 2989/2000 = 1.4945 (driver float: 1.518)

theorem Proofs.smooth_dec_cnn_i6 :

2576 / 2000 ≤ 1 / 2 * stdNormalQuantile (9952 / 10000)

img 6: label 4, pred 4, q₀ = 9952/10000 → radius ≥ 2576/2000 = 1.2880 (driver float: 1.295)

theorem Proofs.smooth_dec_cnn_i7 :

1552 / 2000 ≤ 1 / 2 * stdNormalQuantile (9399 / 10000)

img 7: label 9, pred 9, q₀ = 9399/10000 → radius ≥ 1552/2000 = 0.7760 (driver float: 0.777)

theorem Proofs.smooth_dec_cnn_i8 :

2349 / 2000 ≤ 1 / 2 * stdNormalQuantile (9908 / 10000)

img 8: label 5, pred 5, q₀ = 9908/10000 → radius ≥ 2349/2000 = 1.1745 (driver float: 1.179)

theorem Proofs.smooth_dec_cnn_i9 :

2232 / 2000 ≤ 1 / 2 * stdNormalQuantile (9874 / 10000)

img 9: label 9, pred 9, q₀ = 9874/10000 → radius ≥ 2232/2000 = 1.1160 (driver float: 1.119)

theorem Proofs.smooth_dec_cnn_i10 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 10: label 0, pred 0, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_cnn_i11 :

2894 / 2000 ≤ 1 / 2 * stdNormalQuantile (9983 / 10000)

img 11: label 6, pred 6, q₀ = 9983/10000 → radius ≥ 2894/2000 = 1.4470 (driver float: 1.465)

theorem Proofs.smooth_dec_cnn_i12 :

2473 / 2000 ≤ 1 / 2 * stdNormalQuantile (9935 / 10000)

img 12: label 9, pred 9, q₀ = 9935/10000 → radius ≥ 2473/2000 = 1.2365 (driver float: 1.242)

theorem Proofs.smooth_dec_cnn_i13 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 13: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i14 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 14: label 1, pred 1, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i15 :

2092 / 2000 ≤ 1 / 2 * stdNormalQuantile (9820 / 10000)

img 15: label 5, pred 5, q₀ = 9820/10000 → radius ≥ 2092/2000 = 1.0460 (driver float: 1.048)

theorem Proofs.smooth_dec_cnn_i16 :

2501 / 2000 ≤ 1 / 2 * stdNormalQuantile (9940 / 10000)

img 16: label 9, pred 9, q₀ = 9940/10000 → radius ≥ 2501/2000 = 1.2505 (driver float: 1.256)

theorem Proofs.smooth_dec_cnn_i17 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 17: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i18 :

163 / 2000 ≤ 1 / 2 * stdNormalQuantile (5650 / 10000)

img 18: label 3, pred 3, q₀ = 5650/10000 → radius ≥ 163/2000 = 0.0815 (driver float: 0.082)

theorem Proofs.smooth_dec_cnn_i19 :

2968 / 2000 ≤ 1 / 2 * stdNormalQuantile (9987 / 10000)

img 19: label 4, pred 4, q₀ = 9987/10000 → radius ≥ 2968/2000 = 1.4840 (driver float: 1.506)

theorem Proofs.smooth_dec_cnn_i20 :

798 / 2000 ≤ 1 / 2 * stdNormalQuantile (7878 / 10000)

img 20: label 9, pred 9, q₀ = 7878/10000 → radius ≥ 798/2000 = 0.3990 (driver float: 0.399)

theorem Proofs.smooth_dec_cnn_i21 :

2125 / 2000 ≤ 1 / 2 * stdNormalQuantile (9834 / 10000)

img 21: label 6, pred 6, q₀ = 9834/10000 → radius ≥ 2125/2000 = 1.0625 (driver float: 1.065)

theorem Proofs.smooth_dec_cnn_i22 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 22: label 6, pred 6, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i23 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 23: label 5, pred 5, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i24 :

1399 / 2000 ≤ 1 / 2 * stdNormalQuantile (9193 / 10000)

img 24: label 4, pred 4, q₀ = 9193/10000 → radius ≥ 1399/2000 = 0.6995 (driver float: 0.700)

theorem Proofs.smooth_dec_cnn_i25 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 25: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i26 :

2878 / 2000 ≤ 1 / 2 * stdNormalQuantile (9982 / 10000)

img 26: label 7, pred 7, q₀ = 9982/10000 → radius ≥ 2878/2000 = 1.4390 (driver float: 1.456)

theorem Proofs.smooth_dec_cnn_i27 :

2737 / 2000 ≤ 1 / 2 * stdNormalQuantile (9971 / 10000)

img 27: label 4, pred 4, q₀ = 9971/10000 → radius ≥ 2737/2000 = 1.3685 (driver float: 1.379)

theorem Proofs.smooth_dec_cnn_i28 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 28: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i29 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 29: label 1, pred 1, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i30 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 30: label 3, pred 3, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i31 :

2834 / 2000 ≤ 1 / 2 * stdNormalQuantile (9979 / 10000)

img 31: label 1, pred 1, q₀ = 9979/10000 → radius ≥ 2834/2000 = 1.4170 (driver float: 1.431)

theorem Proofs.smooth_dec_cnn_i32 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 32: label 3, pred 3, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_cnn_i33 :

275 / 2000 ≤ 1 / 2 * stdNormalQuantile (6084 / 10000)

img 33: label 4, pred 4, q₀ = 6084/10000 → radius ≥ 275/2000 = 0.1375 (driver float: 0.138)

theorem Proofs.smooth_dec_cnn_i34 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 34: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i35 :

2759 / 2000 ≤ 1 / 2 * stdNormalQuantile (9973 / 10000)

img 35: label 2, pred 2, q₀ = 9973/10000 → radius ≥ 2759/2000 = 1.3795 (driver float: 1.391)

theorem Proofs.smooth_dec_cnn_i36 :

2576 / 2000 ≤ 1 / 2 * stdNormalQuantile (9952 / 10000)

img 36: label 7, pred 7, q₀ = 9952/10000 → radius ≥ 2576/2000 = 1.2880 (driver float: 1.295)

theorem Proofs.smooth_dec_cnn_i37 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 37: label 1, pred 1, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_cnn_i38 :

918 / 2000 ≤ 1 / 2 * stdNormalQuantile (8210 / 10000)

img 38: label 2, pred 2, q₀ = 8210/10000 → radius ≥ 918/2000 = 0.4590 (driver float: 0.460)

theorem Proofs.smooth_dec_cnn_i39 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 39: label 1, pred 1, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_cnn_i40 :

2678 / 2000 ≤ 1 / 2 * stdNormalQuantile (9965 / 10000)

img 40: label 1, pred 1, q₀ = 9965/10000 → radius ≥ 2678/2000 = 1.3390 (driver float: 1.348)

theorem Proofs.smooth_dec_cnn_i41 :

1957 / 2000 ≤ 1 / 2 * stdNormalQuantile (9750 / 10000)

img 41: label 7, pred 7, q₀ = 9750/10000 → radius ≥ 1957/2000 = 0.9785 (driver float: 0.980)

theorem Proofs.smooth_dec_cnn_i42 :

2894 / 2000 ≤ 1 / 2 * stdNormalQuantile (9983 / 10000)

img 42: label 4, pred 4, q₀ = 9983/10000 → radius ≥ 2894/2000 = 1.4470 (driver float: 1.465)

theorem Proofs.smooth_dec_cnn_i43 :

2495 / 2000 ≤ 1 / 2 * stdNormalQuantile (9939 / 10000)

img 43: label 2, pred 2, q₀ = 9939/10000 → radius ≥ 2495/2000 = 1.2475 (driver float: 1.253)

theorem Proofs.smooth_dec_cnn_i44 :

2284 / 2000 ≤ 1 / 2 * stdNormalQuantile (9890 / 10000)

img 44: label 3, pred 3, q₀ = 9890/10000 → radius ≥ 2284/2000 = 1.1420 (driver float: 1.145)

theorem Proofs.smooth_dec_cnn_i45 :

2395 / 2000 ≤ 1 / 2 * stdNormalQuantile (9919 / 10000)

img 45: label 5, pred 5, q₀ = 9919/10000 → radius ≥ 2395/2000 = 1.1975 (driver float: 1.202)

theorem Proofs.smooth_dec_cnn_i46 :

2989 / 2000 ≤ 1 / 2 * stdNormalQuantile (9988 / 10000)

img 46: label 1, pred 1, q₀ = 9988/10000 → radius ≥ 2989/2000 = 1.4945 (driver float: 1.518)

theorem Proofs.smooth_dec_cnn_i47 :

2989 / 2000 ≤ 1 / 2 * stdNormalQuantile (9988 / 10000)

img 47: label 2, pred 2, q₀ = 9988/10000 → radius ≥ 2989/2000 = 1.4945 (driver float: 1.518)

theorem Proofs.smooth_dec_cnn_i48 :

2071 / 2000 ≤ 1 / 2 * stdNormalQuantile (9810 / 10000)

img 48: label 4, pred 4, q₀ = 9810/10000 → radius ≥ 2071/2000 = 1.0355 (driver float: 1.037)

theorem Proofs.smooth_dec_cnn_i49 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 49: label 4, pred 4, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_cnn_i50 :

2530 / 2000 ≤ 1 / 2 * stdNormalQuantile (9945 / 10000)

img 50: label 6, pred 6, q₀ = 9945/10000 → radius ≥ 2530/2000 = 1.2650 (driver float: 1.271)

theorem Proofs.smooth_dec_cnn_i51 :

2794 / 2000 ≤ 1 / 2 * stdNormalQuantile (9976 / 10000)

img 51: label 3, pred 3, q₀ = 9976/10000 → radius ≥ 2794/2000 = 1.3970 (driver float: 1.410)

theorem Proofs.smooth_dec_cnn_i52 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 52: label 5, pred 5, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i53 :

2549 / 2000 ≤ 1 / 2 * stdNormalQuantile (9948 / 10000)

img 53: label 5, pred 5, q₀ = 9948/10000 → radius ≥ 2549/2000 = 1.2745 (driver float: 1.281)

theorem Proofs.smooth_dec_cnn_i54 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 54: label 6, pred 6, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i55 :

2894 / 2000 ≤ 1 / 2 * stdNormalQuantile (9983 / 10000)

img 55: label 0, pred 0, q₀ = 9983/10000 → radius ≥ 2894/2000 = 1.4470 (driver float: 1.465)

theorem Proofs.smooth_dec_cnn_i56 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 56: label 4, pred 4, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i57 :

2989 / 2000 ≤ 1 / 2 * stdNormalQuantile (9988 / 10000)

img 57: label 1, pred 1, q₀ = 9988/10000 → radius ≥ 2989/2000 = 1.4945 (driver float: 1.518)

theorem Proofs.smooth_dec_cnn_i58 :

2737 / 2000 ≤ 1 / 2 * stdNormalQuantile (9971 / 10000)

img 58: label 9, pred 9, q₀ = 9971/10000 → radius ≥ 2737/2000 = 1.3685 (driver float: 1.379)

theorem Proofs.smooth_dec_cnn_i59 :

2834 / 2000 ≤ 1 / 2 * stdNormalQuantile (9979 / 10000)

img 59: label 5, pred 5, q₀ = 9979/10000 → radius ≥ 2834/2000 = 1.4170 (driver float: 1.431)

theorem Proofs.smooth_dec_cnn_i60 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 60: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i61 :

813 / 2000 ≤ 1 / 2 * stdNormalQuantile (7922 / 10000)

img 61: label 8, pred 8, q₀ = 7922/10000 → radius ≥ 813/2000 = 0.4065 (driver float: 0.407)

theorem Proofs.smooth_dec_cnn_i62 :

299 / 2000 ≤ 1 / 2 * stdNormalQuantile (6176 / 10000)

img 62: label 9, pred 9, q₀ = 6176/10000 → radius ≥ 299/2000 = 0.1495 (driver float: 0.150)

theorem Proofs.smooth_dec_cnn_i63 :

1119 / 2000 ≤ 1 / 2 * stdNormalQuantile (8687 / 10000)

img 63: label 3, pred 3, q₀ = 8687/10000 → radius ≥ 1119/2000 = 0.5595 (driver float: 0.560)

theorem Proofs.smooth_dec_cnn_i64 :

2524 / 2000 ≤ 1 / 2 * stdNormalQuantile (9944 / 10000)

img 64: label 7, pred 7, q₀ = 9944/10000 → radius ≥ 2524/2000 = 1.2620 (driver float: 1.268)

theorem Proofs.smooth_dec_cnn_i65 :

1174 / 2000 ≤ 1 / 2 * stdNormalQuantile (8801 / 10000)

img 65: label 4, pred 4, q₀ = 8801/10000 → radius ≥ 1174/2000 = 0.5870 (driver float: 0.588)

theorem Proofs.smooth_dec_cnn_i66 :

2530 / 2000 ≤ 1 / 2 * stdNormalQuantile (9945 / 10000)

img 66: label 6, pred 6, q₀ = 9945/10000 → radius ≥ 2530/2000 = 1.2650 (driver float: 1.271)

theorem Proofs.smooth_dec_cnn_i67 :

2968 / 2000 ≤ 1 / 2 * stdNormalQuantile (9987 / 10000)

img 67: label 4, pred 4, q₀ = 9987/10000 → radius ≥ 2968/2000 = 1.4840 (driver float: 1.506)

theorem Proofs.smooth_dec_cnn_i68 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 68: label 3, pred 3, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i69 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 69: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i70 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 70: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i71 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 71: label 0, pred 0, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i72 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 72: label 2, pred 2, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i73 :

776 / 2000 ≤ 1 / 2 * stdNormalQuantile (7814 / 10000)

img 73: label 9, pred 9, q₀ = 7814/10000 → radius ≥ 776/2000 = 0.3880 (driver float: 0.388)

theorem Proofs.smooth_dec_cnn_i74 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 74: label 1, pred 1, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i75 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 75: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i76 :

2716 / 2000 ≤ 1 / 2 * stdNormalQuantile (9969 / 10000)

img 76: label 3, pred 3, q₀ = 9969/10000 → radius ≥ 2716/2000 = 1.3580 (driver float: 1.369)

theorem Proofs.smooth_dec_cnn_i77 :

2968 / 2000 ≤ 1 / 2 * stdNormalQuantile (9987 / 10000)

img 77: label 2, pred 2, q₀ = 9987/10000 → radius ≥ 2968/2000 = 1.4840 (driver float: 1.506)

theorem Proofs.smooth_dec_cnn_i78 :

2323 / 2000 ≤ 1 / 2 * stdNormalQuantile (9901 / 10000)

img 78: label 9, pred 9, q₀ = 9901/10000 → radius ≥ 2323/2000 = 1.1615 (driver float: 1.165)

theorem Proofs.smooth_dec_cnn_i79 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 79: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i80 :

2349 / 2000 ≤ 1 / 2 * stdNormalQuantile (9908 / 10000)

img 80: label 7, pred 7, q₀ = 9908/10000 → radius ≥ 2349/2000 = 1.1745 (driver float: 1.179)

theorem Proofs.smooth_dec_cnn_i81 :

2929 / 2000 ≤ 1 / 2 * stdNormalQuantile (9985 / 10000)

img 81: label 6, pred 6, q₀ = 9985/10000 → radius ≥ 2929/2000 = 1.4645 (driver float: 1.484)

theorem Proofs.smooth_dec_cnn_i82 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 82: label 2, pred 2, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i83 :

2834 / 2000 ≤ 1 / 2 * stdNormalQuantile (9979 / 10000)

img 83: label 7, pred 7, q₀ = 9979/10000 → radius ≥ 2834/2000 = 1.4170 (driver float: 1.431)

theorem Proofs.smooth_dec_cnn_i84 :

2759 / 2000 ≤ 1 / 2 * stdNormalQuantile (9973 / 10000)

img 84: label 8, pred 8, q₀ = 9973/10000 → radius ≥ 2759/2000 = 1.3795 (driver float: 1.391)

theorem Proofs.smooth_dec_cnn_i85 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 85: label 4, pred 4, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i86 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 86: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i87 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 87: label 3, pred 3, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i88 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 88: label 6, pred 6, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i89 :

2759 / 2000 ≤ 1 / 2 * stdNormalQuantile (9973 / 10000)

img 89: label 1, pred 1, q₀ = 9973/10000 → radius ≥ 2759/2000 = 1.3795 (driver float: 1.391)

theorem Proofs.smooth_dec_cnn_i90 :

2737 / 2000 ≤ 1 / 2 * stdNormalQuantile (9971 / 10000)

img 90: label 3, pred 3, q₀ = 9971/10000 → radius ≥ 2737/2000 = 1.3685 (driver float: 1.379)

theorem Proofs.smooth_dec_cnn_i91 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 91: label 6, pred 6, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i92 :

632 / 2000 ≤ 1 / 2 * stdNormalQuantile (7364 / 10000)

img 92: label 9, pred 9, q₀ = 7364/10000 → radius ≥ 632/2000 = 0.3160 (driver float: 0.316)

theorem Proofs.smooth_dec_cnn_i93 :

2894 / 2000 ≤ 1 / 2 * stdNormalQuantile (9983 / 10000)

img 93: label 3, pred 3, q₀ = 9983/10000 → radius ≥ 2894/2000 = 1.4470 (driver float: 1.465)

theorem Proofs.smooth_dec_cnn_i94 :

2989 / 2000 ≤ 1 / 2 * stdNormalQuantile (9988 / 10000)

img 94: label 1, pred 1, q₀ = 9988/10000 → radius ≥ 2989/2000 = 1.4945 (driver float: 1.518)

theorem Proofs.smooth_dec_cnn_i95 :

2048 / 2000 ≤ 1 / 2 * stdNormalQuantile (9799 / 10000)

img 95: label 4, pred 4, q₀ = 9799/10000 → radius ≥ 2048/2000 = 1.0240 (driver float: 1.026)

theorem Proofs.smooth_dec_cnn_i96 :

2697 / 2000 ≤ 1 / 2 * stdNormalQuantile (9967 / 10000)

img 96: label 1, pred 1, q₀ = 9967/10000 → radius ≥ 2697/2000 = 1.3485 (driver float: 1.358)

theorem Proofs.smooth_dec_cnn_i97 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 97: label 7, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cnn_i98 :

2260 / 2000 ≤ 1 / 2 * stdNormalQuantile (9883 / 10000)

img 98: label 6, pred 6, q₀ = 9883/10000 → radius ≥ 2260/2000 = 1.1300 (driver float: 1.133)

theorem Proofs.smooth_dec_cnn_i99 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 99: label 9, pred 9, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

def Proofs.smoothDecCnnEntries :

List (ℕ × ℕ)

MNIST-CNN aggregate: (m, a) per certified image — decimal radius m/2000 for q₀ = a/10000.

Equations

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

Instances For

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

e ∈ smoothDecCnnEntries → ↑e.1 / 2000 ≤ 1 / 2 * stdNormalQuantile (↑e.2 / 10000)

Every MNIST-CNN scorecard image's decimal radius is a theorem: m/2000 ≤ σ·Φ⁻¹(a/10000).

theorem Proofs.smooth_dec_cifar_i0 :

591 / 2000 ≤ 1 / 2 * stdNormalQuantile (7230 / 10000)

img 0: label 3, pred 3, q₀ = 7230/10000 → radius ≥ 591/2000 = 0.2955 (driver float: 0.296)

theorem Proofs.smooth_dec_cifar_i1 :

959 / 2000 ≤ 1 / 2 * stdNormalQuantile (8313 / 10000)

img 1: label 8, pred 8, q₀ = 8313/10000 → radius ≥ 959/2000 = 0.4795 (driver float: 0.480)

theorem Proofs.smooth_dec_cifar_i2 :

574 / 2000 ≤ 1 / 2 * stdNormalQuantile (7172 / 10000)

img 2: label 8, pred 8, q₀ = 7172/10000 → radius ≥ 574/2000 = 0.2870 (driver float: 0.287)

theorem Proofs.smooth_dec_cifar_i4 :

985 / 2000 ≤ 1 / 2 * stdNormalQuantile (8380 / 10000)

img 4: label 6, pred 6, q₀ = 8380/10000 → radius ≥ 985/2000 = 0.4925 (driver float: 0.493)

theorem Proofs.smooth_dec_cifar_i5 :

2543 / 2000 ≤ 1 / 2 * stdNormalQuantile (9947 / 10000)

img 5: label 6, pred 6, q₀ = 9947/10000 → radius ≥ 2543/2000 = 1.2715 (driver float: 1.278)

theorem Proofs.smooth_dec_cifar_i6 :

1068 / 2000 ≤ 1 / 2 * stdNormalQuantile (8574 / 10000)

img 6: label 1, pred 1, q₀ = 8574/10000 → radius ≥ 1068/2000 = 0.5340 (driver float: 0.534)

theorem Proofs.smooth_dec_cifar_i7 :

1262 / 2000 ≤ 1 / 2 * stdNormalQuantile (8967 / 10000)

img 7: label 6, pred 6, q₀ = 8967/10000 → radius ≥ 1262/2000 = 0.6310 (driver float: 0.631)

theorem Proofs.smooth_dec_cifar_i8 :

917 / 2000 ≤ 1 / 2 * stdNormalQuantile (8206 / 10000)

img 8: label 3, pred 3, q₀ = 8206/10000 → radius ≥ 917/2000 = 0.4585 (driver float: 0.459)

theorem Proofs.smooth_dec_cifar_i9 :

221 / 2000 ≤ 1 / 2 * stdNormalQuantile (5878 / 10000)

img 9: label 1, pred 1, q₀ = 5878/10000 → radius ≥ 221/2000 = 0.1105 (driver float: 0.111)

theorem Proofs.smooth_dec_cifar_i11 :

828 / 2000 ≤ 1 / 2 * stdNormalQuantile (7964 / 10000)

img 11: label 9, pred 9, q₀ = 7964/10000 → radius ≥ 828/2000 = 0.4140 (driver float: 0.414)

theorem Proofs.smooth_dec_cifar_i13 :

1382 / 2000 ≤ 1 / 2 * stdNormalQuantile (9167 / 10000)

img 13: label 7, pred 7, q₀ = 9167/10000 → radius ≥ 1382/2000 = 0.6910 (driver float: 0.692)

theorem Proofs.smooth_dec_cifar_i14 :

2462 / 2000 ≤ 1 / 2 * stdNormalQuantile (9933 / 10000)

img 14: label 9, pred 9, q₀ = 9933/10000 → radius ≥ 2462/2000 = 1.2310 (driver float: 1.236)

theorem Proofs.smooth_dec_cifar_i15 :

880 / 2000 ≤ 1 / 2 * stdNormalQuantile (8108 / 10000)

img 15: label 8, pred 8, q₀ = 8108/10000 → radius ≥ 880/2000 = 0.4400 (driver float: 0.440)

theorem Proofs.smooth_dec_cifar_i16 :

115 / 2000 ≤ 1 / 2 * stdNormalQuantile (5460 / 10000)

img 16: label 5, pred 7, q₀ = 5460/10000 → radius ≥ 115/2000 = 0.0575 (driver float: 0.058) (misclassified)

theorem Proofs.smooth_dec_cifar_i18 :

1393 / 2000 ≤ 1 / 2 * stdNormalQuantile (9184 / 10000)

img 18: label 8, pred 8, q₀ = 9184/10000 → radius ≥ 1393/2000 = 0.6965 (driver float: 0.697)

theorem Proofs.smooth_dec_cifar_i19 :

886 / 2000 ≤ 1 / 2 * stdNormalQuantile (8123 / 10000)

img 19: label 6, pred 6, q₀ = 8123/10000 → radius ≥ 886/2000 = 0.4430 (driver float: 0.443)

theorem Proofs.smooth_dec_cifar_i21 :

2530 / 2000 ≤ 1 / 2 * stdNormalQuantile (9945 / 10000)

img 21: label 0, pred 2, q₀ = 9945/10000 → radius ≥ 2530/2000 = 1.2650 (driver float: 1.271) (misclassified)

theorem Proofs.smooth_dec_cifar_i22 :

205 / 2000 ≤ 1 / 2 * stdNormalQuantile (5816 / 10000)

img 22: label 4, pred 2, q₀ = 5816/10000 → radius ≥ 205/2000 = 0.1025 (driver float: 0.103) (misclassified)

theorem Proofs.smooth_dec_cifar_i23 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 23: label 9, pred 9, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_cifar_i24 :

218 / 2000 ≤ 1 / 2 * stdNormalQuantile (5865 / 10000)

img 24: label 5, pred 2, q₀ = 5865/10000 → radius ≥ 218/2000 = 0.1090 (driver float: 0.109) (misclassified)

theorem Proofs.smooth_dec_cifar_i26 :

1150 / 2000 ≤ 1 / 2 * stdNormalQuantile (8751 / 10000)

img 26: label 4, pred 2, q₀ = 8751/10000 → radius ≥ 1150/2000 = 0.5750 (driver float: 0.575) (misclassified)

theorem Proofs.smooth_dec_cifar_i27 :

1321 / 2000 ≤ 1 / 2 * stdNormalQuantile (9069 / 10000)

img 27: label 0, pred 7, q₀ = 9069/10000 → radius ≥ 1321/2000 = 0.6605 (driver float: 0.661) (misclassified)

theorem Proofs.smooth_dec_cifar_i28 :

2071 / 2000 ≤ 1 / 2 * stdNormalQuantile (9810 / 10000)

img 28: label 9, pred 9, q₀ = 9810/10000 → radius ≥ 2071/2000 = 1.0355 (driver float: 1.037)

theorem Proofs.smooth_dec_cifar_i29 :

2628 / 2000 ≤ 1 / 2 * stdNormalQuantile (9959 / 10000)

img 29: label 6, pred 6, q₀ = 9959/10000 → radius ≥ 2628/2000 = 1.3140 (driver float: 1.322)

theorem Proofs.smooth_dec_cifar_i30 :

63 / 2000 ≤ 1 / 2 * stdNormalQuantile (5253 / 10000)

img 30: label 6, pred 3, q₀ = 5253/10000 → radius ≥ 63/2000 = 0.0315 (driver float: 0.032) (misclassified)

theorem Proofs.smooth_dec_cifar_i31 :

145 / 2000 ≤ 1 / 2 * stdNormalQuantile (5578 / 10000)

img 31: label 5, pred 7, q₀ = 5578/10000 → radius ≥ 145/2000 = 0.0725 (driver float: 0.073) (misclassified)

theorem Proofs.smooth_dec_cifar_i32 :

738 / 2000 ≤ 1 / 2 * stdNormalQuantile (7700 / 10000)

img 32: label 4, pred 4, q₀ = 7700/10000 → radius ≥ 738/2000 = 0.3690 (driver float: 0.369)

theorem Proofs.smooth_dec_cifar_i33 :

1515 / 2000 ≤ 1 / 2 * stdNormalQuantile (9353 / 10000)

img 33: label 5, pred 5, q₀ = 9353/10000 → radius ≥ 1515/2000 = 0.7575 (driver float: 0.758)

theorem Proofs.smooth_dec_cifar_i34 :

2030 / 2000 ≤ 1 / 2 * stdNormalQuantile (9790 / 10000)

img 34: label 9, pred 9, q₀ = 9790/10000 → radius ≥ 2030/2000 = 1.0150 (driver float: 1.017)

theorem Proofs.smooth_dec_cifar_i35 :

240 / 2000 ≤ 1 / 2 * stdNormalQuantile (5951 / 10000)

img 35: label 2, pred 1, q₀ = 5951/10000 → radius ≥ 240/2000 = 0.1200 (driver float: 0.120) (misclassified)

theorem Proofs.smooth_dec_cifar_i37 :

2590 / 2000 ≤ 1 / 2 * stdNormalQuantile (9954 / 10000)

img 37: label 1, pred 9, q₀ = 9954/10000 → radius ≥ 2590/2000 = 1.2950 (driver float: 1.302) (misclassified)

theorem Proofs.smooth_dec_cifar_i38 :

1359 / 2000 ≤ 1 / 2 * stdNormalQuantile (9132 / 10000)

img 38: label 9, pred 9, q₀ = 9132/10000 → radius ≥ 1359/2000 = 0.6795 (driver float: 0.680)

theorem Proofs.smooth_dec_cifar_i39 :

299 / 2000 ≤ 1 / 2 * stdNormalQuantile (6176 / 10000)

img 39: label 5, pred 5, q₀ = 6176/10000 → radius ≥ 299/2000 = 0.1495 (driver float: 0.150)

theorem Proofs.smooth_dec_cifar_i41 :

1741 / 2000 ≤ 1 / 2 * stdNormalQuantile (9594 / 10000)

img 41: label 6, pred 6, q₀ = 9594/10000 → radius ≥ 1741/2000 = 0.8705 (driver float: 0.872)

theorem Proofs.smooth_dec_cifar_i42 :

1808 / 2000 ≤ 1 / 2 * stdNormalQuantile (9649 / 10000)

img 42: label 5, pred 5, q₀ = 9649/10000 → radius ≥ 1808/2000 = 0.9040 (driver float: 0.905)

theorem Proofs.smooth_dec_cifar_i45 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 45: label 9, pred 9, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597)

theorem Proofs.smooth_dec_cifar_i46 :

541 / 2000 ≤ 1 / 2 * stdNormalQuantile (7059 / 10000)

img 46: label 3, pred 3, q₀ = 7059/10000 → radius ≥ 541/2000 = 0.2705 (driver float: 0.271)

theorem Proofs.smooth_dec_cifar_i47 :

1323 / 2000 ≤ 1 / 2 * stdNormalQuantile (9073 / 10000)

img 47: label 9, pred 3, q₀ = 9073/10000 → radius ≥ 1323/2000 = 0.6615 (driver float: 0.662) (misclassified)

theorem Proofs.smooth_dec_cifar_i48 :

369 / 2000 ≤ 1 / 2 * stdNormalQuantile (6441 / 10000)

img 48: label 7, pred 7, q₀ = 6441/10000 → radius ≥ 369/2000 = 0.1845 (driver float: 0.185)

theorem Proofs.smooth_dec_cifar_i49 :

1245 / 2000 ≤ 1 / 2 * stdNormalQuantile (8937 / 10000)

img 49: label 6, pred 6, q₀ = 8937/10000 → radius ≥ 1245/2000 = 0.6225 (driver float: 0.623)

theorem Proofs.smooth_dec_cifar_i50 :

3036 / 2000 ≤ 1 / 2 * stdNormalQuantile (9990 / 10000)

img 50: label 9, pred 9, q₀ = 9990/10000 → radius ≥ 3036/2000 = 1.5180 (driver float: 1.545)

theorem Proofs.smooth_dec_cifar_i51 :

1078 / 2000 ≤ 1 / 2 * stdNormalQuantile (8597 / 10000)

img 51: label 8, pred 8, q₀ = 8597/10000 → radius ≥ 1078/2000 = 0.5390 (driver float: 0.539)

theorem Proofs.smooth_dec_cifar_i52 :

393 / 2000 ≤ 1 / 2 * stdNormalQuantile (6531 / 10000)

img 52: label 0, pred 6, q₀ = 6531/10000 → radius ≥ 393/2000 = 0.1965 (driver float: 0.197) (misclassified)

theorem Proofs.smooth_dec_cifar_i53 :

381 / 2000 ≤ 1 / 2 * stdNormalQuantile (6486 / 10000)

img 53: label 3, pred 3, q₀ = 6486/10000 → radius ≥ 381/2000 = 0.1905 (driver float: 0.191)

theorem Proofs.smooth_dec_cifar_i54 :

2468 / 2000 ≤ 1 / 2 * stdNormalQuantile (9934 / 10000)

img 54: label 8, pred 8, q₀ = 9934/10000 → radius ≥ 2468/2000 = 1.2340 (driver float: 1.239)

theorem Proofs.smooth_dec_cifar_i55 :

1362 / 2000 ≤ 1 / 2 * stdNormalQuantile (9136 / 10000)

img 55: label 8, pred 8, q₀ = 9136/10000 → radius ≥ 1362/2000 = 0.6810 (driver float: 0.682)

theorem Proofs.smooth_dec_cifar_i57 :

557 / 2000 ≤ 1 / 2 * stdNormalQuantile (7116 / 10000)

img 57: label 7, pred 6, q₀ = 7116/10000 → radius ≥ 557/2000 = 0.2785 (driver float: 0.279) (misclassified)

theorem Proofs.smooth_dec_cifar_i60 :

1469 / 2000 ≤ 1 / 2 * stdNormalQuantile (9293 / 10000)

img 60: label 7, pred 7, q₀ = 9293/10000 → radius ≥ 1469/2000 = 0.7345 (driver float: 0.735)

theorem Proofs.smooth_dec_cifar_i61 :

1566 / 2000 ≤ 1 / 2 * stdNormalQuantile (9415 / 10000)

img 61: label 3, pred 3, q₀ = 9415/10000 → radius ≥ 1566/2000 = 0.7830 (driver float: 0.784)

theorem Proofs.smooth_dec_cifar_i62 :

561 / 2000 ≤ 1 / 2 * stdNormalQuantile (7129 / 10000)

img 62: label 6, pred 6, q₀ = 7129/10000 → radius ≥ 561/2000 = 0.2805 (driver float: 0.281)

theorem Proofs.smooth_dec_cifar_i63 :

340 / 2000 ≤ 1 / 2 * stdNormalQuantile (6331 / 10000)

img 63: label 3, pred 9, q₀ = 6331/10000 → radius ≥ 340/2000 = 0.1700 (driver float: 0.170) (misclassified)

theorem Proofs.smooth_dec_cifar_i64 :

178 / 2000 ≤ 1 / 2 * stdNormalQuantile (5710 / 10000)

img 64: label 6, pred 5, q₀ = 5710/10000 → radius ≥ 178/2000 = 0.0890 (driver float: 0.089) (misclassified)

theorem Proofs.smooth_dec_cifar_i65 :

163 / 2000 ≤ 1 / 2 * stdNormalQuantile (5649 / 10000)

img 65: label 2, pred 2, q₀ = 5649/10000 → radius ≥ 163/2000 = 0.0815 (driver float: 0.082)

theorem Proofs.smooth_dec_cifar_i67 :

607 / 2000 ≤ 1 / 2 * stdNormalQuantile (7282 / 10000)

img 67: label 2, pred 2, q₀ = 7282/10000 → radius ≥ 607/2000 = 0.3035 (driver float: 0.304)

theorem Proofs.smooth_dec_cifar_i68 :

2270 / 2000 ≤ 1 / 2 * stdNormalQuantile (9886 / 10000)

img 68: label 3, pred 3, q₀ = 9886/10000 → radius ≥ 2270/2000 = 1.1350 (driver float: 1.138)

theorem Proofs.smooth_dec_cifar_i69 :

1925 / 2000 ≤ 1 / 2 * stdNormalQuantile (9731 / 10000)

img 69: label 7, pred 9, q₀ = 9731/10000 → radius ≥ 1925/2000 = 0.9625 (driver float: 0.964) (misclassified)

theorem Proofs.smooth_dec_cifar_i71 :

1075 / 2000 ≤ 1 / 2 * stdNormalQuantile (8591 / 10000)

img 71: label 6, pred 6, q₀ = 8591/10000 → radius ≥ 1075/2000 = 0.5375 (driver float: 0.538)

theorem Proofs.smooth_dec_cifar_i72 :

1684 / 2000 ≤ 1 / 2 * stdNormalQuantile (9541 / 10000)

img 72: label 8, pred 8, q₀ = 9541/10000 → radius ≥ 1684/2000 = 0.8420 (driver float: 0.843)

theorem Proofs.smooth_dec_cifar_i73 :

2362 / 2000 ≤ 1 / 2 * stdNormalQuantile (9911 / 10000)

img 73: label 8, pred 8, q₀ = 9911/10000 → radius ≥ 2362/2000 = 1.1810 (driver float: 1.185)

theorem Proofs.smooth_dec_cifar_i75 :

365 / 2000 ≤ 1 / 2 * stdNormalQuantile (6428 / 10000)

img 75: label 2, pred 2, q₀ = 6428/10000 → radius ≥ 365/2000 = 0.1825 (driver float: 0.183)

theorem Proofs.smooth_dec_cifar_i76 :

433 / 2000 ≤ 1 / 2 * stdNormalQuantile (6678 / 10000)

img 76: label 9, pred 9, q₀ = 6678/10000 → radius ≥ 433/2000 = 0.2165 (driver float: 0.217)

theorem Proofs.smooth_dec_cifar_i77 :

1507 / 2000 ≤ 1 / 2 * stdNormalQuantile (9343 / 10000)

img 77: label 3, pred 3, q₀ = 9343/10000 → radius ≥ 1507/2000 = 0.7535 (driver float: 0.754)

theorem Proofs.smooth_dec_cifar_i79 :

936 / 2000 ≤ 1 / 2 * stdNormalQuantile (8256 / 10000)

img 79: label 8, pred 8, q₀ = 8256/10000 → radius ≥ 936/2000 = 0.4680 (driver float: 0.468)

theorem Proofs.smooth_dec_cifar_i80 :

962 / 2000 ≤ 1 / 2 * stdNormalQuantile (8322 / 10000)

img 80: label 8, pred 8, q₀ = 8322/10000 → radius ≥ 962/2000 = 0.4810 (driver float: 0.481)

theorem Proofs.smooth_dec_cifar_i81 :

744 / 2000 ≤ 1 / 2 * stdNormalQuantile (7717 / 10000)

img 81: label 1, pred 1, q₀ = 7717/10000 → radius ≥ 744/2000 = 0.3720 (driver float: 0.372)

theorem Proofs.smooth_dec_cifar_i82 :

2543 / 2000 ≤ 1 / 2 * stdNormalQuantile (9947 / 10000)

img 82: label 1, pred 1, q₀ = 9947/10000 → radius ≥ 2543/2000 = 1.2715 (driver float: 1.278)

theorem Proofs.smooth_dec_cifar_i83 :

938 / 2000 ≤ 1 / 2 * stdNormalQuantile (8262 / 10000)

img 83: label 7, pred 7, q₀ = 8262/10000 → radius ≥ 938/2000 = 0.4690 (driver float: 0.470)

theorem Proofs.smooth_dec_cifar_i84 :

246 / 2000 ≤ 1 / 2 * stdNormalQuantile (5975 / 10000)

img 84: label 2, pred 2, q₀ = 5975/10000 → radius ≥ 246/2000 = 0.1230 (driver float: 0.123)

theorem Proofs.smooth_dec_cifar_i85 :

3122 / 2000 ≤ 1 / 2 * stdNormalQuantile (9993 / 10000)

img 85: label 5, pred 7, q₀ = 9993/10000 → radius ≥ 3122/2000 = 1.5610 (driver float: 1.597) (misclassified)

theorem Proofs.smooth_dec_cifar_i86 :

251 / 2000 ≤ 1 / 2 * stdNormalQuantile (5991 / 10000)

img 86: label 2, pred 2, q₀ = 5991/10000 → radius ≥ 251/2000 = 0.1255 (driver float: 0.126)

theorem Proofs.smooth_dec_cifar_i87 :

16 / 2000 ≤ 1 / 2 * stdNormalQuantile (5065 / 10000)

img 87: label 7, pred 8, q₀ = 5065/10000 → radius ≥ 16/2000 = 0.0080 (driver float: 0.008) (misclassified)

theorem Proofs.smooth_dec_cifar_i88 :

567 / 2000 ≤ 1 / 2 * stdNormalQuantile (7149 / 10000)

img 88: label 8, pred 8, q₀ = 7149/10000 → radius ≥ 567/2000 = 0.2835 (driver float: 0.284)

theorem Proofs.smooth_dec_cifar_i89 :

1933 / 2000 ≤ 1 / 2 * stdNormalQuantile (9736 / 10000)

img 89: label 9, pred 9, q₀ = 9736/10000 → radius ≥ 1933/2000 = 0.9665 (driver float: 0.968)

theorem Proofs.smooth_dec_cifar_i90 :

705 / 2000 ≤ 1 / 2 * stdNormalQuantile (7599 / 10000)

img 90: label 0, pred 0, q₀ = 7599/10000 → radius ≥ 705/2000 = 0.3525 (driver float: 0.353)

theorem Proofs.smooth_dec_cifar_i92 :

2362 / 2000 ≤ 1 / 2 * stdNormalQuantile (9911 / 10000)

img 92: label 8, pred 8, q₀ = 9911/10000 → radius ≥ 2362/2000 = 1.1810 (driver float: 1.185)

theorem Proofs.smooth_dec_cifar_i93 :

334 / 2000 ≤ 1 / 2 * stdNormalQuantile (6310 / 10000)

img 93: label 6, pred 5, q₀ = 6310/10000 → radius ≥ 334/2000 = 0.1670 (driver float: 0.167) (misclassified)

theorem Proofs.smooth_dec_cifar_i95 :

268 / 2000 ≤ 1 / 2 * stdNormalQuantile (6057 / 10000)

img 95: label 6, pred 3, q₀ = 6057/10000 → radius ≥ 268/2000 = 0.1340 (driver float: 0.134) (misclassified)

theorem Proofs.smooth_dec_cifar_i96 :

699 / 2000 ≤ 1 / 2 * stdNormalQuantile (7580 / 10000)

img 96: label 6, pred 6, q₀ = 7580/10000 → radius ≥ 699/2000 = 0.3495 (driver float: 0.350)

theorem Proofs.smooth_dec_cifar_i98 :

2186 / 2000 ≤ 1 / 2 * stdNormalQuantile (9858 / 10000)

img 98: label 0, pred 0, q₀ = 9858/10000 → radius ≥ 2186/2000 = 1.0930 (driver float: 1.096)

theorem Proofs.smooth_dec_cifar_i99 :

590 / 2000 ≤ 1 / 2 * stdNormalQuantile (7225 / 10000)

img 99: label 7, pred 7, q₀ = 7225/10000 → radius ≥ 590/2000 = 0.2950 (driver float: 0.295)

def Proofs.smoothDecCifarEntries :

List (ℕ × ℕ)

CIFAR-CNN aggregate: (m, a) per certified image — decimal radius m/2000 for q₀ = a/10000.

Equations

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

Instances For

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

e ∈ smoothDecCifarEntries → ↑e.1 / 2000 ≤ 1 / 2 * stdNormalQuantile (↑e.2 / 10000)

Every CIFAR-CNN scorecard image's decimal radius is a theorem: m/2000 ≤ σ·Φ⁻¹(a/10000).