# Pedersen-segment-scalar-not-zero-proof

Proof that `pedersen-segment-scalar` is not 0.

This is proved by first proving that
the loop function is outside the interval
between -2^{4\cdot(j-1)} to 2^{4\cdot(j-1)},
both exclusive.
Setting j=1, we have that `pedersen-segment-scalar`
is outside the interval from -1 to 1 exclusive, i.e. it is not 0.
To prove the lemma about the loop function,
to avoid dealing with a disjunction of inequalities,
we introduce a predicate for being outside the interval
and we prove some theorems about it.
Some of these theorems are currently somewhat specific;
perhaps there is a way to improve the form of the proof.

The fact, mentioned above, that
the loop function is outside a certain interval
is also useful to prove other properties.
Thus, we export a theorem asserting that.

### Definitions and Theorems

**Theorem: **pedersen-segment-scalar-loop-outside-interval

(defthm pedersen-segment-scalar-loop-outside-interval
(implies (and (posp j)
(bit-listp segment)
(integerp (/ (len segment) 3))
(consp segment))
(or (<= (pedersen-segment-scalar-loop j segment)
(- (expt 2 (+ -4 (* 4 j)))))
(<= (expt 2 (+ -4 (* 4 j)))
(pedersen-segment-scalar-loop j segment)))))

**Theorem: **pedersen-segment-scalar-not-zero

(defthm pedersen-segment-scalar-not-zero
(implies (and (bit-listp segment)
(integerp (/ (len segment) 3))
(consp segment))
(not (equal (pedersen-segment-scalar segment)
0)))
:rule-classes :type-prescription)