Model.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.SingleFold.evalNat line 8
Source documentation
Evaluation over the integers of an integer polynomial at natural inputs.
Also declared: ComparatorChallenges/SingleFold.lean:8 (same declaration text).
```
noncomputable def evalNat {n m : ℕ} (P : MvPolynomial (Fin n ⊕ Fin m) ℤ)
    (a : Fin n → ℕ) (w : Fin m → ℕ) : ℤ :=
…
```
def OAI.SingleFold.Represents line 14
Source documentation
Exact existence on members, no witness on nonmembers, and uniqueness of the whole witness on every input. No coordinates are hidden outside w.
Also declared: ComparatorChallenges/SingleFold.lean:14 (same declaration text).
```
def Represents {n m : ℕ} (P : MvPolynomial (Fin n ⊕ Fin m) ℤ)
    (S : Set (Fin n → ℕ)) : Prop :=
…
```
def OAI.SingleFold.MainStatement line 20
Source documentation
Single-fold representation with positive input and witness lengths.
Also declared: ComparatorChallenges/SingleFold.lean:20 (same declaration text).
```
def MainStatement : Prop :=
…
```