ActualCircuitRank.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The circuit rank bound for the actual rounded parameters.

theorem OAI.Problem335.LowerParameters.actual_circuit_rank_bound_of_weightParameters line 16
Source documentation
The full quantitative circuit estimate with actual source degrees and dimension. The weight-parameter premise is discharged uniformly eventually.
```
theorem actual_circuit_rank_bound_of_weightParameters
    {K : Type*} [Field K] {n : ℕ} (c : Depth5Circuit K n)
    (side : (Fin n × Fin n × Fin n) → Bool)
    (hvcard : Fintype.card {x // side x = true} = v n)
    (hucard : Fintype.card {x // side x = false} = u n)
    (hp : WeightParameters n (s n) (q n))
    (hc : circuitValue c = imm K n) :
    (bidegreeRank side (a n) (b n) (k n) (m n) (circuitValue c) : ℝ) ≤
      2 * (circuitSize c : ℝ) ^ 2 * sourceDimension n *
        Real.exp ((24 + 4 * Real.log 5) * Real.sqrt n) *
          (n : ℝ) ^ (-Real.sqrt n / 100) := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.u, OAI.Problem335.WeightParameters, OAI.Problem335.LowerParameters.s, OAI.Problem335.LowerParameters.q, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.bidegreeRank, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.k, OAI.Problem335.LowerParameters.m, OAI.Problem335.circuitSize, OAI.Problem335.LowerParameters.sourceDimension
theorem OAI.Problem335.LowerParameters.exists_rankData_circuit_upper_cutoff line 53
Source documentation
The actual, fixed rank measure satisfies the circuit upper bound after one absolute threshold. No numerical, product-rank, or partition hypotheses remain. This is the upper estimate used in the final rank sandwich.
```
theorem exists_rankData_circuit_upper_cutoff :
    ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n → ∀ c : Depth5Circuit ℂ n,
      circuitValue c = imm ℂ n →
      rankData n (circuitValue c) ≤
        2 * (circuitSize c : ℝ) ^ 2 * rankDimension n *
          Real.exp ((24 + 4 * Real.log 5) * Real.sqrt n) *
            (n : ℝ) ^ (-Real.sqrt n / 100) := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.LowerParameters.rankData, OAI.Problem335.circuitSize, OAI.Problem335.LowerParameters.rankDimension

theorem OAI.Problem335.LowerParameters.eventually_rankData_circuit_upper line 70

Source documentation

Filter form of the concrete circuit endpoint.

theorem eventually_rankData_circuit_upper :
    ∀ᶠ n : ℕ in Filter.atTop, ∀ c : Depth5Circuit ℂ n,
      circuitValue c = imm ℂ n →
      rankData n (circuitValue c) ≤
        2 * (circuitSize c : ℝ) ^ 2 * rankDimension n *
          Real.exp ((24 + 4 * Real.log 5) * Real.sqrt n) *
            (n : ℝ) ^ (-Real.sqrt n / 100) :=
…

Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.LowerParameters.rankData, OAI.Problem335.circuitSize, OAI.Problem335.LowerParameters.rankDimension