Exact noise thresholds of parity proofs: sub-proof roots under independent bit flips

A parity proof of the Kochen–Specker theorem is a set of observables arranged in contexts of commuting observables whose products are ±I with an odd number of minus signs along a dependency. We study the exact noise threshold of such a proof at the maximally mixed state when every observable outcome is flipped independently with probability η/2 (model F). Contexts may have different sizes s_c. We prove that for every parity proof η*F ≥ max_T (1 − x_T), where T runs over sub-proofs, k_T ≥ 1 is the least number of contexts of T that a noncontextual assignment must violate, and x_T ∈ (0,1) is the root of Σ{c∈T} xs_c = |T| − 2k_T (1 − x_T := 1 if |T| ≤ 2k_T). Under a symmetrisation condition (condition L, automatic for Pauli proofs with minimal contexts), and with s_c the row weights of the incidence matrix, equality holds when the space K of dependencies is one-dimensional and, by a block reduction to a coset of a short code, whenever the contexts fall into at most dim K + 1 nonzero incidence classes — in particular for every proof with dim K = 2 — and for direct sums of such proofs. Beyond this range the equality can fail for abstract proofs with condition L: for the simplex proof [7,3] (dim K = 4) η*_F = 1 − 5^(−1/4) > max_T (1 − x_T) = 1 − 3^(−1/4). For Pauli proofs with more than dim K + 1 incidence classes it is open; an exact search over 360 abstract proofs with dim K = 2, 3, 4 found no discrepancy (random sampling did not meet the simplex example). The variant with a single root taken over the whole proof is false. Examples with mixed sizes give exact thresholds such as η*_F = 0.1011287750… (4x^5 + x^4 = 3) for a four-qubit Mermin star. For uniform mixing we relate the equal-size value 2k_min/m to the robustness measure of Trandafir, Lisoněk and Cabello and treat a qudit Mermin–Peres square. The methods are standard (parity polytopes, linear programming with exact certificates); what is new is the exact form of the thresholds, the reduction for overlapping dependencies and the certified values.