LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Local-Stochastic Fault-Witness Bound

Statement

Let $r \geq 0$ and let a finite rooted rectangle hierarchy have every root-to-leaf path of exactly $r$ edges. Each leaf is one elementary location; every internal node has at most $a$ children, and the elementary-location sets of distinct children are disjoint. Let $a, q$ be integers with $1 \leq q < a$ . A leaf is bad exactly when its location is faulty, and an internal node is bad exactly when at least $q + 1$ children are bad. Under an $η$ -local-stochastic fault-set law, with $A = (\binom{a}{q + 1})$ and $A η^{q} < 1$ , the probability that the root is bad is at most

A^{- 1 / q} (A^{1 / q} η)^{(q + 1)^{r}} .

No independence assumption is used.

Facts & Assumptions

Given: A finite location set, an $η$ -local-stochastic random fault set, an integer $r \geq 0$ , and the full-depth rooted hierarchy and recursive badness predicate in the statement. Prove the probability bound.

[F1]

Local-Stochastic Fault-Set Law: For every specified set $S$ of elementary locations, the probability that all of $S$ fault is at most $η^{∣ S ∣}$ .

Proof

1.1givenF1

For a leaf $v$ , its single location is a witness set $S$ whose fault forces $v$ to be bad. At depth zero there is one such witness, its size is $1 = (q + 1)^{0}$ , and [F1] bounds the bad probability by $η$ .

2.1givenstep 1.1construct

Suppose a depth- $(r + 1)$ node is bad. It has a $(q + 1)$ -subset $J$ of bad children. For each child $j \in J$ , select one witness set $S_{j}$ that forces that child to be bad. The child location sets are disjoint, so $S = ⋃_{j \in J} S_{j}$ has size $(q + 1) (q + 1)^{r} = (q + 1)^{r + 1}$ and its occurrence forces the parent to be bad. There are at most $A w_{r}^{q + 1}$ such witness sets if $w_{r}$ bounds their number at depth $r$ . Only finite selection from finite sets is used.

3.1step 2.1algebra

The witness-count recurrence $w_{0} = 1$ , $w_{r + 1} \leq A w_{r}^{q + 1}$ gives $w_{r} \leq A^{((q + 1)^{r} - 1) / q}$ . This follows by induction: it is equality at $r = 0$ , and substituting the bound at level $r$ gives exponent $1 + (q + 1) ((q + 1)^{r} - 1) / q = ((q + 1)^{r + 1} - 1) / q$ .

4.1F1step 3.1algebra∎

Each fixed witness set has probability at most $η^{(q + 1)^{r}}$ by [F1]. The union bound over all witnesses gives $P (root bad) \leq A^{((q + 1)^{r} - 1) / q} η^{(q + 1)^{r}} = A^{- 1 / q} (A^{1 / q} η)^{(q + 1)^{r}}$ . Since $A η^{q} < 1$ , the base $A^{1 / q} η$ is below one, so the bound tends to zero.

Depends on

Local-Stochastic Fault-Set Law

Used by

Concatenated Threshold Under Local-Stochastic Correlated Noise Theorem

Dependency tree · two levels

3 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

D. Aharonov and M. Ben-Or, Fault-Tolerant Quantum Computation With Constant Error (standard reference, not scraped)
P. Aliferis, D. Gottesman, J. Preskill, Accuracy Threshold for Postselected Quantum Computation (standard reference, not scraped)