Part of #27043 Hahn's embedding theorem

Part of #27043  (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from #27451 (`Valuation.ball`) and `Metric.ball` / `Metric.closedBall` (`ArchimedeanClass M` actually becomes a `Valuation` when `M` is a ring so these names make sense).

Part of #27043  (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from #27451 (`Valuation.ball`) and `Metric.ball` / `Metric.closedBall` (`ArchimedeanClass M` actually becomes a `Valuation` when `M` is a ring so these names make sense).

Part of leanprover-community#27043 Hahn's embedding theorem

Part of leanprover-community#27043  (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from leanprover-community#27451 (`Valuation.ball`) and `Metric.ball` / `Metric.closedBall` (`ArchimedeanClass M` actually becomes a `Valuation` when `M` is a ring so these names make sense).

Part of leanprover-community#27043  (Hahn embedding theorem). For concepts in this part, I don't find good names from literature, so I took inspiration from leanprover-community#27451 (`Valuation.ball`) and `Metric.ball` / `Metric.closedBall` (`ArchimedeanClass M` actually becomes a `Valuation` when `M` is a ring so these names make sense).

Part 1 of Hahn embedding theorem, or the core part of it. This proves that one can embed an ordered module in HahnSeries.

To obtain the full Hahn embedding theorem, one needs to specialize the coefficient of HahnSeries to Real as a module over Rat, and compose with another embedding from ordered group to ordered module. These will be in part 2

There is a debatable design here: throughout the file, all lemmas uses an input `HahnEmbedding.Seed`. Because the the final theorem is an existence theorem without specifying what `HahnEmbedding.Seed` is used, it is possible to `Classical.choose` a seed from the very beginning (provided `R = Real` ), and the entire file will just use the same chosen seed. Overall, choosing everything from the beginning will likely make the code a little bit more concise. 

I decided against choosing anything till the final step, for the reason that such choice is not canonical for an arbitrary module, and there may be future use of this construction with more canonical choice for specific modules. Examples are:
 - if the input is a `HahnSeries Γ R`, the canonical choice for the `stratum` would be `HahnSeries.single`
 - for the field version of Hahn embedding theorem ("every linearly ordered field can be embedded in `HahnSeries` as a field", not implemented), the canonical choice should ensure that all `stratum` form a graded ring, and the `coeff` should map `(1 : M)` to `(1 : R)`.

But if the argument is not strong enough, I am OK with converting everything to a classical choose.

…nity#27043)

Part 1 of Hahn embedding theorem, or the core part of it. This proves that one can embed an ordered module in HahnSeries.

To obtain the full Hahn embedding theorem, one needs to specialize the coefficient of HahnSeries to Real as a module over Rat, and compose with another embedding from ordered group to ordered module. These will be in part 2

There is a debatable design here: throughout the file, all lemmas uses an input `HahnEmbedding.Seed`. Because the the final theorem is an existence theorem without specifying what `HahnEmbedding.Seed` is used, it is possible to `Classical.choose` a seed from the very beginning (provided `R = Real` ), and the entire file will just use the same chosen seed. Overall, choosing everything from the beginning will likely make the code a little bit more concise. 

I decided against choosing anything till the final step, for the reason that such choice is not canonical for an arbitrary module, and there may be future use of this construction with more canonical choice for specific modules. Examples are:
 - if the input is a `HahnSeries Γ R`, the canonical choice for the `stratum` would be `HahnSeries.single`
 - for the field version of Hahn embedding theorem ("every linearly ordered field can be embedded in `HahnSeries` as a field", not implemented), the canonical choice should ensure that all `stratum` form a graded ring, and the `coeff` should map `(1 : M)` to `(1 : R)`.

But if the argument is not strong enough, I am OK with converting everything to a classical choose.

…nity#27043)

Part 1 of Hahn embedding theorem, or the core part of it. This proves that one can embed an ordered module in HahnSeries.

To obtain the full Hahn embedding theorem, one needs to specialize the coefficient of HahnSeries to Real as a module over Rat, and compose with another embedding from ordered group to ordered module. These will be in part 2

There is a debatable design here: throughout the file, all lemmas uses an input `HahnEmbedding.Seed`. Because the the final theorem is an existence theorem without specifying what `HahnEmbedding.Seed` is used, it is possible to `Classical.choose` a seed from the very beginning (provided `R = Real` ), and the entire file will just use the same chosen seed. Overall, choosing everything from the beginning will likely make the code a little bit more concise. 

I decided against choosing anything till the final step, for the reason that such choice is not canonical for an arbitrary module, and there may be future use of this construction with more canonical choice for specific modules. Examples are:
 - if the input is a `HahnSeries Γ R`, the canonical choice for the `stratum` would be `HahnSeries.single`
 - for the field version of Hahn embedding theorem ("every linearly ordered field can be embedded in `HahnSeries` as a field", not implemented), the canonical choice should ensure that all `stratum` form a graded ring, and the `coeff` should map `(1 : M)` to `(1 : R)`.

But if the argument is not strong enough, I am OK with converting everything to a classical choose.