Exact noise thresholds of the minimal state-independent contextuality set: critical state, full noise profile, and a machine-checked gap between contextuality and incompatibility

We determine exact noise thresholds for the Yu Oh set of 13 rays, the smallest state-independent contextuality set. In our main noise model (model A) the outcome statistics of every context are mixed with the uniform distribution with weight η. (i) Every state admits a Kochen Specker (KS) noncontextual model if and only if η ≥ 3√33 − 17 ≈ 0.2337; the critical state is ψ ∝ (1, 1, (√33−5)/2), and the maximal state-dependent relative violation is (√33−3)/9. (ii) The largest contextual fraction over all states is given in closed form for every η. (iii) Under independent bit ips the same state is critical, with threshold 1 − √︁18 − 3√33. (iv) The sixteen noisy contexts become jointly measurable at ηc ∈ (0.50274, 0.50567], so on an interval starting at 3√33 − 17 every state is noncontextual while the measurements are incompatible; KS-consistent joint measurability needs η > 0.54756, a strict separation that also holds for Mermin's star and the Mermin Peres square, whose KS-consistent threshold is exactly (63 + √17)/114. (v) For independent detector losses the e ciency thresholds are exactly (4 − √6)/2 for all states and (13 +√1033)/48 for state-independent tests. All model-A thresholds are instances of a general formula V/(1+V). For other scenarios the all-state threshold is exactly 2/5 for the Mermin Peres square, 2/7 for CEG-18, and (108 − 44√5)/31 for Kernaghan's 20 rays, attained at exactly six states. The methods are standard; what is new is the exact values and their certi cation: items (i) (iv), the contextual side of (4 −√6)/2 and the formula V/(1 + V) are proved in Lean 4 with Mathlib, by certi cates over Q, Q(√2), Z[√3], Z[i], Q(√17), Q(√33) and Q(√33, √︁18 − 3√33) checked by the kernel; the other values, by exact certi cates outside Lean. Code and certificate scripts: SigmaStar Lean library, Version 1.3.0 10.5281/zenodo.23099654