CircuitOutputDegree.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.outputDegree_eq_of_circuitValue_eq_imm line 11
Source documentation
A nonzero IMM output forces the assigned syntactic output degree to be the layer count.
```
theorem outputDegree_eq_of_circuitValue_eq_imm {K : Type*} [CommSemiring K]
    [Nontrivial K] {n : ℕ} (hn : 0 < n) (c : Depth5Circuit K n)
    (hc : circuitValue c = imm K n) : c.outputDegree = n := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm

theorem OAI.Problem335.upper_degree_eq_of_circuitValue_eq_imm line 19

Source documentation

Every upper product contributing to an IMM circuit has formal degree n.

theorem upper_degree_eq_of_circuitValue_eq_imm {K : Type*} [CommSemiring K]
    [Nontrivial K] {n : ℕ} (hn : 0 < n) (c : Depth5Circuit K n)
    (hc : circuitValue c = imm K n) (entry : K × Fin c.upperCount)
    (he : entry ∈ c.outputInputs) :
    ((c.upperInputs entry.2).map c.middleDegree).sum = n := by
…

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

theorem OAI.Problem335.outputInputs_ne_nil_of_circuitValue_eq_imm line 27
Source documentation
Nonzero IMM cannot be computed by an empty output sum.
```
theorem outputInputs_ne_nil_of_circuitValue_eq_imm {K : Type*} [CommSemiring K]
    [Nontrivial K] {n : ℕ} (hn : 0 < n) (c : Depth5Circuit K n)
    (hc : circuitValue c = imm K n) : c.outputInputs ≠ [] := by
…
```
Mentions: OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm