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 set exhibiting state-independent contextuality, and verify them in Lean 4 with Mathlib. In the main noise model (the outcome statistics of every context are mixed with the uniform distribution on its outcomes, with weight η): - every qutrit state admits a Kochen–Specker noncontextual model if and only if η ≥ 3√33 − 17 ≈ 0.2337; the critical state is ψ ∝ (1, 1, (√33 − 5)/2);- the largest contextual fraction over all states is b(η) = max{0, 2/3 − 19η/6, (√33 − 3)/6 − (6 + √33)η/6}, and the most contextual noiseless state is not the most robust one;- under independent bit flips every state is noncontextual if and only if η ≥ 1 − √(18 − 3√33) ≈ 0.1246;- the joint-measurability threshold of the sixteen noisy contexts satisfies 0.50274 < η_c ≤ 0.50567, so on a wide interval of noise levels every state is noncontextual while the measurements remain incompatible; KS-consistent joint measurability is strictly stronger (threshold in [0.54756, 0.54765]);- for the Mermin–Peres square the KS-consistent threshold is exactly (63 + √17)/114, above its standard joint-measurability threshold (34 + 12√2)/93; for Mermin's star the standard threshold is exactly 16/25, strictly below the KS-consistent one;- for independent detector losses, a state-dependent test detects contextuality for every efficiency above (4 − √6)/2 ≈ 0.7753. All thresholds of the main model are instances of the formula V/(1 + V), V the best relative violation, which we prove in Lean for every finite scenario and every noncontextual noise model mixed in linearly. A table gives the thresholds for KCBS, the Mermin–Peres square, CEG-18 and Mermin's star. The methods are standard (linear-programming and semidefinite duality); what is new is the exact values and their formal verification: exact certificates over number fields, checked by the Lean kernel (207 cited declarations, depending only on the axioms propext, Classical.choice and Quot.sound). Code and certificate scripts: SigmaStar Lean library, version 1.2.0, doi:10.5281/zenodo.23014827.