API checks for leading-class primality transfer #
This separately compiled client exercises both residue branches of the generic set-level core of LM24, Proposition 9.2.2. The residue-one branch needs no fraction-field hypothesis; the residue-zero branch requires exactly that the embedded inner integer part generate the coefficient Hahn field.
theorem
Tests.primalityTransfer_residue_one
{K : Type u_1}
{G : Type u_2}
{R : Type u_3}
[DivisionRing K]
[LinearOrder K]
[IsOrderedRing K]
[Archimedean K]
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[Module K G]
[IsOrderedModule K G]
[Field R]
(u : HahnEmbedding.ArchimedeanStrata K G)
(Z : Subring R)
(b : ↥(HahnSeries.truncationIntegerPart G Z))
(hb0 : ↑b ≠ 0)
(horder : (↑↑b).order ≠ 0)
(htau : HahnSeries.Nonpositive.tauBall ((↑b).leadingClass horder) ↑b = 1)
:
theorem
Tests.primalityTransfer_residue_zero
{K : Type u_1}
{G : Type u_2}
{R : Type u_3}
[DivisionRing K]
[LinearOrder K]
[IsOrderedRing K]
[Archimedean K]
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[Module K G]
[IsOrderedModule K G]
[Field R]
(u : HahnEmbedding.ArchimedeanStrata K G)
(Z : Subring R)
(b : ↥(HahnSeries.truncationIntegerPart G Z))
(hb0 : ↑b ≠ 0)
(horder : (↑↑b).order ≠ 0)
(hfrac : (HahnSeries.Nonpositive.innerIntegerPartSubring ((↑b).leadingClass horder) Z).fracSubring = ⊤)
(htau : HahnSeries.Nonpositive.tauBall ((↑b).leadingClass horder) ↑b = 0)
:
theorem
Tests.primalityTransfer_reduced
{K : Type u_1}
{G : Type u_2}
{R : Type u_3}
[DivisionRing K]
[LinearOrder K]
[IsOrderedRing K]
[Archimedean K]
[AddCommGroup G]
[LinearOrder G]
[IsOrderedAddMonoid G]
[Module K G]
[IsOrderedModule K G]
[Field R]
(u : HahnEmbedding.ArchimedeanStrata K G)
(Z : Subring R)
(b : ↥(HahnSeries.truncationIntegerPart G Z))
(hb0 : ↑b ≠ 0)
(horder : (↑↑b).order ≠ 0)
(hbReduced : (↑b).IsReduced)
(hfrac :
HahnSeries.Nonpositive.tauBall ((↑b).leadingClass horder) ↑b = 0 →
(HahnSeries.Nonpositive.innerIntegerPartSubring ((↑b).leadingClass horder) Z).fracSubring = ⊤)
: