Main.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QAC.parity_lower_bound_polynomial_size line 12
Source documentation
Measured-output parity for a polynomial qubit bound with a fixed multiplicative constant.
Distinct definitions of this name: ComparatorChallenges/RegularParity.lean:63 (same statement text; different proof or body). Qualify references as OAI.QAC.parity_lower_bound_polynomial_size@path.
```
theorem parity_lower_bound_polynomial_size (d k C : ℕ)
    (_hd : 0 < d) (_hk : 0 < k) (_hC : 0 < C) :
    ∃ n₀ : ℕ, ∀ n ≥ n₀, ∀ N : ℕ, n ≤ N → N ≤ C * (n + 1) ^ k →
      ∀ layers : List (PhysicalLayer N), layers.length ≤ d →
        ∀ out : Fin N, ∃ x : Word n,
          successProbability (physicalCircuitMatrix layers) out x < (2 : ℝ) / 3 := by
…
```
Mentions: OAI.QAC.PhysicalLayer, OAI.QAC.Word, OAI.QAC.successProbability, OAI.QAC.physicalCircuitMatrix