Bound on the value of `pedersen-segment-scalar`.

Theorem 5.4.1 in [ZPS:5.4.1.7] defines @$(\Delta$) as
a bound on the value of the encoding function `pedersen-segment-scalar` is more generally defined
over segments of any length that is a multiple of 3.
Accordingly, we define a function that expresses `pedersen-segment-scalar` is defined in terms of
an auxiliary recursive function that is defined even more generally
over not only a segment of length multiple of 3
but also the index

Based on the summation that defines `pedersen-segment-scalar` is obtained from that
by setting

To prove that these are actual bounds,
we start with a proof by induction for the recursive function and bound.
We need a lemma about the length of `pedersen-enc`.
(These two lemmas are at the beginning of this file.)
We also need a few arithmetic lemmas
to nudge the proof in the right direction.
(These arithmetic lemmas are below.)
With linear bound rules for the recursive function in hand,
the bound proofs for `pedersen-segment-scalar` are automatic.

**Function: **

(defun pedersen-segment-scalar-loop-bound (j segment) (declare (xargs :guard (and (posp j) (bit-listp segment)))) (declare (xargs :guard (integerp (/ (len segment) 3)))) (let ((__function__ 'pedersen-segment-scalar-loop-bound)) (declare (ignorable __function__)) (if (consp segment) (+ (* 4 (expt 2 (* 4 (1- j)))) (pedersen-segment-scalar-loop-bound (1+ j) (nthcdr 3 segment))) 0)))

**Theorem: **

(defthm natp-of-pedersen-segment-scalar-loop-bound (implies (posp j) (b* ((bound (pedersen-segment-scalar-loop-bound j segment))) (natp bound))) :rule-classes :rewrite)

**Function: **

(defun pedersen-segment-scalar-bound (segment) (declare (xargs :guard (bit-listp segment))) (declare (xargs :guard (integerp (/ (len segment) 3)))) (let ((__function__ 'pedersen-segment-scalar-bound)) (declare (ignorable __function__)) (pedersen-segment-scalar-loop-bound 1 segment)))

**Theorem: **

(defthm natp-of-pedersen-segment-scalar-bound (b* ((bound (pedersen-segment-scalar-bound segment))) (natp bound)) :rule-classes :rewrite)

**Theorem: **

(defthm pedersen-segment-scalar-loop-upper-bound (implies (and (posp j) (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (pedersen-segment-scalar-loop j segment) (pedersen-segment-scalar-loop-bound j segment))) :rule-classes :linear)

**Theorem: **

(defthm pedersen-segment-scalar-loop-lower-bound (implies (and (posp j) (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (- (pedersen-segment-scalar-loop-bound j segment)) (pedersen-segment-scalar-loop j segment))) :rule-classes :linear)

**Theorem: **

(defthm pedersen-segment-scalar-upper-bound (implies (and (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (pedersen-segment-scalar segment) (pedersen-segment-scalar-bound segment))) :rule-classes :linear)

**Theorem: **

(defthm pedersen-segment-scalar-lower-bound (implies (and (bit-listp segment) (integerp (/ (len segment) 3)) (consp segment)) (<= (- (pedersen-segment-scalar-bound segment)) (pedersen-segment-scalar segment))) :rule-classes :linear)