CharacteristicZeroTransfer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.exists_complex_circuit_of_countable line 15
Source documentation
A circuit over a countable characteristic-zero field can be realized over ℂ, with exactly the same number of gates and the same IMM identity.
```
theorem exists_complex_circuit_of_countable {K : Type u} [Field K] [CharZero K]
    [Countable K] {n : ℕ} (c : Depth5Circuit K n)
    (hc : circuitValue c = imm K n) :
    ∃ d : Depth5Circuit ℂ n, circuitValue d = imm ℂ n ∧ circuitSize d = circuitSize c := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.circuitSize

theorem OAI.Problem335.countable_circuit_bound_of_complex line 25

Source documentation

Any pointwise real gate-count lower bound over ℂ transfers to every countable field of characteristic zero.

theorem countable_circuit_bound_of_complex {K : Type u} [Field K] [CharZero K]
    [Countable K] {n : ℕ} {b : ℝ}
    (h : ∀ d : Depth5Circuit ℂ n,
      circuitValue d = imm ℂ n → b ≤ (circuitSize d : ℝ))
    (c : Depth5Circuit K n) (hc : circuitValue c = imm K n) :
    b ≤ (circuitSize c : ℝ) := by
…

Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.circuitSize

theorem OAI.Problem335.restrictCircuit_computes_imm line 35
Source documentation
Restriction to the coefficient subfield preserves and reflects the IMM identity.
```
theorem restrictCircuit_computes_imm {K : Type u} [Field K] {n : ℕ}
    (c : Depth5Circuit K n) :
    circuitValue (restrictCircuit c) = imm (circuitCoefficientField c) n ↔
      circuitValue c = imm K n := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.restrictCircuit, OAI.Problem335.imm, OAI.Problem335.circuitCoefficientField
theorem OAI.Problem335.exists_complex_circuit line 46
Source documentation
Every characteristic-zero IMM circuit has a same-size complex realization. Only the finitely many occurring coefficients are embedded, not the entire field.
```
theorem exists_complex_circuit {K : Type u} [Field K] [CharZero K]
    {n : ℕ} (c : Depth5Circuit K n) (hc : circuitValue c = imm K n) :
    ∃ d : Depth5Circuit ℂ n, circuitValue d = imm ℂ n ∧ circuitSize d = circuitSize c := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.circuitSize

theorem OAI.Problem335.circuit_bound_of_complex line 54

Source documentation

Pointwise complex gate lower bounds hold over any characteristic-zero field.

theorem circuit_bound_of_complex {K : Type u} [Field K] [CharZero K]
    {n : ℕ} {b : ℝ}
    (h : ∀ d : Depth5Circuit ℂ n,
      circuitValue d = imm ℂ n → b ≤ (circuitSize d : ℝ))
    (c : Depth5Circuit K n) (hc : circuitValue c = imm K n) :
    b ≤ (circuitSize c : ℝ) := by
…

Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.circuitSize

theorem OAI.Problem335.characteristic_zero_depth_five_lower_bound_of_complex line 66

Source documentation

The extension to characteristic zero uses the same absolute threshold as its complex counterpart. This implication has no lower-bound assumptions other than the precise complex conclusion.

theorem characteristic_zero_depth_five_lower_bound_of_complex
    (h : ∃ n0 : ℕ, ∀ n : ℕ, n0 ≤ n → ∀ c : Depth5Circuit ℂ n,
      circuitValue c = imm ℂ n →
      (n : ℝ) ^ (Real.sqrt (n : ℝ) / 400) ≤ (circuitSize c : ℝ)) :
    ∃ n0 : ℕ, ∀ (K : Type u) [Field K] [CharZero K], ∀ n : ℕ, n0 ≤ n →
      ∀ c : Depth5Circuit K n, circuitValue c = imm K n →
      (n : ℝ) ^ (Real.sqrt (n : ℝ) / 400) ≤ (circuitSize c : ℝ) := by
…

Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.circuitSize