UpperGateCounting.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Finite index counts for the consecutive-block depth-five construction.

abbrev OAI.Problem335.BlockLowerIndex line 12
Source documentation
A lower product gate chooses a block, its two endpoints, and all internal indices.
```
abbrev BlockLowerIndex (n r : ℕ) (d : Fin r → ℕ) :=
…
```
abbrev OAI.Problem335.BlockMiddleIndex line 16
Source documentation
A middle sum gate computes one entry of one block product.
```
abbrev BlockMiddleIndex (n r : ℕ) := Fin r × Fin n × Fin n
```
abbrev OAI.Problem335.BlockUpperIndex line 19
Source documentation
An upper product gate chooses the indices at the boundaries between blocks.
```
abbrev BlockUpperIndex (n r : ℕ) := Fin (r - 1) → Fin n
```
theorem OAI.Problem335.card_blockMiddleIndex line 21
theorem OAI.Problem335.card_blockUpperIndex line 25

theorem OAI.Problem335.block_entry_monomial_count line 30

Source documentation

Count the monomials used for every entry of a nonempty block.

theorem block_entry_monomial_count (n d : ℕ) (hd : 1 ≤ d) :
    Fintype.card (Fin n × Fin n × (Fin (d - 1) → Fin n)) = n ^ (d + 1) := by
…

theorem OAI.Problem335.card_blockLowerIndex line 36

theorem OAI.Problem335.card_blockLowerIndex_le line 43

Source documentation

Uniform block-length bounds control the total number of lower gates.

theorem card_blockLowerIndex_le (n r t : ℕ) (d : Fin r → ℕ)
    (hn : 1 ≤ n) (hd : ∀ b, 1 ≤ d b) (hdt : ∀ b, d b ≤ t) :
    Fintype.card (BlockLowerIndex n r d) ≤ r * n ^ (t + 1) := by
…

Mentions: OAI.Problem335.BlockLowerIndex

theorem OAI.Problem335.block_gate_count_le line 53

Source documentation

The exact finite index counts give the advertised combinatorial gate bound.

theorem block_gate_count_le (n r t : ℕ) (d : Fin r → ℕ)
    (hn : 1 ≤ n) (hd : ∀ b, 1 ≤ d b) (hdt : ∀ b, d b ≤ t) :
    2 * n ^ 3 + Fintype.card (BlockLowerIndex n r d) +
        Fintype.card (BlockMiddleIndex n r) + Fintype.card (BlockUpperIndex n r) + 1 ≤
      2 * n ^ 3 + r * n ^ 2 + r * n ^ (t + 1) + n ^ (r - 1) + 1 := by
…

Mentions: OAI.Problem335.BlockLowerIndex, OAI.Problem335.BlockMiddleIndex, OAI.Problem335.BlockUpperIndex