## Weights

Formalization in Lean4 of some results in *Minimization of hypersurfaces* by A.-S. Elsenhans and myself.

### Contents

The paper introduces the notion of a *weight* on forms of degree `Weight`

.

We can then compare weights in the following way. We first define `Weight.testvecs n d`

).
Then to a weight `Weight.f`

.

Then we say that a weight *dominates* another weight `w ≤d w'`

for this relation. `≤d`

is a pre-order
on the set of weights, but not a (partial) order. For example, a weight

We say that a weight *normalized* (`Weight.normalized`

). We show that if a normalized weight `Weight.dom_of_dom_perm`

). So up to permutations, it suffices to consider
only normalized weights.

We say that a set *complete* if every normalized
weight is dominated by an element of `Weight.complete_set`

). We say that a complete
set of weights is *minimal* if it is minimal with respect to inclusion among complete sets
(`Weight.minimal_complete_set`

). This is equivalent to saying that when

The first main result formalized here is that there is a *unique* minimal complete set
of weights, which is given by the set `Weight.M n d`

of all normalized weights that are minimal
elements with respect to domination within the set of all normalized weights.
This is **Proposition 3.13** in the paper. See `Weight.M_is_minimal`

and `Weight.M_is_unique`

.

We show in addition that the entries of nonzero elements of `M n d`

are coprime
(`Weight.gcd_eq_one_of_in_M`

) and that `M n 1`

consists of the single
element `Weight.w1_unique`

).

The second main result is a proof of **Theorem 1.6** in the paper, which says that
in the case `Weight.dom_by_max_le_d`

and `Weight.theorem_1_6`

.