diff --git a/docs/case-studies/index.md b/docs/case-studies/index.md deleted file mode 100644 index 1cf0262..0000000 --- a/docs/case-studies/index.md +++ /dev/null @@ -1,9 +0,0 @@ -# Case studies - -This page contains links to various case studies of how the [Semigroups -package for GAP][] and/or [libsemigroups_pybind11][] have been used in -mathematical research. - -Please use the menu at the left or the links below: - -* [Short presentations for transformation monoids](short.md) diff --git a/docs/examples/atlas/index.md b/docs/examples/atlas/index.md new file mode 100644 index 0000000..5c19066 --- /dev/null +++ b/docs/examples/atlas/index.md @@ -0,0 +1,185 @@ +# Verifying presentations in the ATLAS of Finite Groups + +In this example, we will verify the validity of the presentations of the +sporadic groups as given in [this ATLAS][atlas]. +In particular, where possible, we will use the Todd-Coxeter algorithm to check +that the size of group defined by the presentations is equal to the claimed +size. Where the claimed size of the group is very large, we will instead +calculate the size of small-index subgroups. + +??? info "libsemigroups_pybind11 version" + + All examples provided on the subsequent subpages were run using + libsemigroups_pybind11 version 1.4.4 on a laptop with a 13th Gen Intel(R) + Core(TM) i7-13700H processor and 64 GB RAM. + +??? info "Defining groups with monoid presentations" + + The presentations provided for the groups in the ATLAS are + *group presentations*. This means that it is assumed that there is + multiplicative identity $1$, and that each generator $a$ has an inverse + $a^{-1}$ such that $aa^{-1} = a^{-1}a = 1$. In [libsemigroups_pybind11][], + however, presentations are either *semigroup presentations* or + *monoid presentations*, depending whether the relations of the presentation + are allowed to contain the empty word $\varepsilon$. Therefore, we will need + to add extra generators and relations to a monoid presentation to define a + group. + + Suppose that a group $G$ is defined by the group presentation + $\langle{A \mid R }\rangle_{\text{grp}}$. Then $G$ can also be defined by + the monoid presentation + $\langle{A \sqcup A^{-1} \mid R \cup R' }\rangle_{\text{mon}}$ where + $A^{-1}$ is a set disjoint from $A$ containing letters that will be treated + as inverses for the letters in $A$, and $R'$ is the set of relations of the + form $aa^{-1} = \varepsilon$ and $a^{-1}a = \varepsilon$. + + In the subsequent subpages, we will use lowercase letters for the + generators that are given in the presentations in the ATLAS, and their + uppercase counterparts to represent their inverses. Therefore, many of our + examples will in a similar way to: + + ```py + from libsemigroups_pybind11 import presentation, Presentation + p = presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") + ``` + + The algorithms in [libsemigroups_pybind11][] were written for semigroups and + monoids. This means that there are no group-specific optimisations. + +The following tables summarise the results of this project. Click on a group +to see more information. + +
+
+
+ + + + + + + + + + + +
Mathieu groups
+ M11 + + M12 + + M22 + + M23 + + M24 +
+
+
+ + + + + + + + + + + + + +
Leech lattice groups
HS + J2 + Co1 + Co2 + Co3McLSuz
+
+
+ + + + + + + + + + + + + + +
Monster sections
HeHNTh + Fi22 + Fi23Fi24'BM
+
+
+ + + + + + + + + + + + +
Pariahs
+ J1 + O'N + J3 + Ru + J4 + Ly
+
+
+ + + + + + + +
Miscellaneous
T
+
+
+ +
+
+ + + + + + + + + + + + + + + + + + + +
Legend
+ The presentation defines a group of the correct size +
+ The presentation has a subgroup of the correct size +
+ The presentation defines a group of the incorrect size +
Todd-Coxeter did not terminate
No presentation is provided
+
+
+
+ +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/leech-lattice/co2/index.md b/docs/examples/atlas/leech-lattice/co2/index.md new file mode 100644 index 0000000..0c900db --- /dev/null +++ b/docs/examples/atlas/leech-lattice/co2/index.md @@ -0,0 +1,12 @@ +# Conway group Co~2~ + +> Order: $42,305,421,312,000$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the Conway group Co~2~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/examples/atlas/leech-lattice/hs.md b/docs/examples/atlas/leech-lattice/hs.md new file mode 100644 index 0000000..01d3061 --- /dev/null +++ b/docs/examples/atlas/leech-lattice/hs.md @@ -0,0 +1,28 @@ +# Higman-Sims group HS + +> Order: $44,352,000$ + +> Presentation: TODO + +On this page, we verify that the above claimed presentation of the Higman-Sims group HS +defines a group of order $44,352,000$. + +## The code + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/leech-lattice/j2.md b/docs/examples/atlas/leech-lattice/j2.md new file mode 100644 index 0000000..ad93c5e --- /dev/null +++ b/docs/examples/atlas/leech-lattice/j2.md @@ -0,0 +1,28 @@ +# Janko group J~2~ + +> Order: $604,800$ + +> Presentation: TODO + +On this page, we verify that the above claimed presentation of the Janko group J~2~ +defines a group of order $604,800$. + +## The code + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/leech-lattice/mcl/index.md b/docs/examples/atlas/leech-lattice/mcl/index.md new file mode 100644 index 0000000..5db3fb3 --- /dev/null +++ b/docs/examples/atlas/leech-lattice/mcl/index.md @@ -0,0 +1,12 @@ +# McLaughlin group McL + +> Order: $898,128,000$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the McLaughlin group McL define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/examples/atlas/mathieu/m11.md b/docs/examples/atlas/mathieu/m11.md new file mode 100644 index 0000000..cfd7a84 --- /dev/null +++ b/docs/examples/atlas/mathieu/m11.md @@ -0,0 +1,105 @@ +# Mathieu group M~11~ + +> Order: $7,920$ + +> Presentation: +> $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^6 = ababab^{−1}abab^2ab^{−1}abab^{−1}ab^{−1} = 1 }\rangle$ + +On this page, we verify that the above claimed presentation of the Mathieu group +M~11~ defines a group of order $7,920$. + +## The code + +=== "Python" + + In [libsemigroups_pybind11][], the following script constructs the + presentation for M~11~ and runs the Todd-Coxeter algorithm. + + ```python + from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation + from libsemigroups_pybind11.words import parse_relations + + # Setup the presentation object with the empty and inverses, so it can represent a group + p = Presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") + + # Add the defining relations + presentation.add_rule(p, parse_relations("a^2"), "") + presentation.add_rule(p, parse_relations("b^4"), "") + presentation.add_rule(p, parse_relations("(ab)^11"), "") + presentation.add_rule(p, parse_relations("(ab^2)^6"), "") + presentation.add_rule(p, parse_relations("ababaBabab^2aBabaBaB"), "") + + # Run the Todd-Coxeter algorithm + tc = ToddCoxeter(congruence_kind.twosided, p) + tc.run() + + assert tc.number_of_classes() == 7920 + ``` + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Running the above Python script produces the following output: + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 22], ∑(|u| + |v|) = 73 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 28µs | all runs = 28µs | elapsed = 92µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 + #0: ToddCoxeter: diff 0.0.0 | +7,919 | +1,992,427 | +2,000,346 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 31,680 | 0 | 100.0% + #0: ToddCoxeter: diff 0.0.0 | +31,680 | -4 | +100.0% + #0: ToddCoxeter: phase 0.0 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.1.2 | active | killed | defined + #0: ToddCoxeter: nodes | 7,920 | 1,992,427 | 2,000,347 + #0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.1.0 | +7,919 | +1,992,427 | +2,000,346 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 31,680 | 0 | 100.0% + #0: ToddCoxeter: diff 0.1.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.1.0 | +31,680 | -4 | +100.0% + #0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 0 | 0 | 1 | 0 + #0: ToddCoxeter: time spent in phases | - (0%) | - (0%) | 176ms (100%) | - (0%) + #0: ToddCoxeter: phase 0.1 = 176ms | run 0 = 176ms | all runs = 176ms | elapsed = 176ms + ``` + +=== "ACE" + + Coming soon! + +:simple-ticktick: The computed size of the group matches the size of the group +provided on [the ATLAS][atlas]: $7,920$. + +!!! note + + The output you see when you run the script yourself might be different from + the above; the numbers produced and time taken will depend on the machine + you are using. However, the size of the group that is reported should be + the same as above. + +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: + https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m12.md b/docs/examples/atlas/mathieu/m12.md new file mode 100644 index 0000000..999046f --- /dev/null +++ b/docs/examples/atlas/mathieu/m12.md @@ -0,0 +1,143 @@ +# Mathieu group M~12~ + +> Order: $95,040$ + +> Presentation: +> $\langle{ a, b \mid a^2 = b^3 = (ab)^{11} = [a, b]^6 = (ababab^{−1})^6 = 1 }\rangle$ + +On this page, we verify that the above claimed presentation of the Mathieu group +M~12~ defines a group of order $95,040$. + +## The code + +=== "Python" + + In [libsemigroups_pybind11][], the following script constructs the + presentation for M~12~ and runs the Todd-Coxeter algorithm. + + ```python + from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation + from libsemigroups_pybind11.words import parse_relations + + # Setup the presentation object with the empty and inverses, so it can represent a group + p = Presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") + + # Add the defining relations + presentation.add_rule(p, parse_relations("a^2"), "") + presentation.add_rule(p, parse_relations("b^3"), "") + presentation.add_rule(p, parse_relations("(ab)^11"), "") + presentation.add_rule(p, parse_relations("(a,b)^6"), "") + presentation.add_rule(p, parse_relations("(ababaB)^6"), "") + + + # Run the Todd-Coxeter algorithm + tc = ToddCoxeter(congruence_kind.twosided, p) + tc.run() + + assert tc.number_of_classes() == 95040 + ``` + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Running the above script produces the following output: + + ??? info "Output from the Python script" + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 9, |u| + |v| ∈ [2, 36], ∑(|u| + |v|) = 95 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 24µs | all runs = 24µs | elapsed = 84µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 + #0: ToddCoxeter: diff 0.0.0 | +5,000,003 | +2,964,327 | +7,964,330 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% + #0: ToddCoxeter: diff 0.0.0 | +5,782,533 | +14,217,479 | +28.9% + #0: ToddCoxeter: phase 0.0 = 489ms | run 0 = 489ms | all runs = 489ms | elapsed = 489ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,004 | 2,964,327 | 7,964,331 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,782,533 | 14,217,483 | 28.9% + #0: ToddCoxeter: time | run 0 = 489ms | all runs = 489ms | elapsed = 489ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,004 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + #0: ToddCoxeter: large collapse, number of coincidences 100,002 >= 100,000 = large_collapse()! + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 STOP + #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: diff 0.1.0 | -4,904,958 | +4,904,958 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: diff 0.1.0 | -5,402,356 | -14,217,476 | +71.1% + #0: ToddCoxeter: phase 0.1 = 449ms | run 0 = 939ms | all runs = 939ms | elapsed = 939ms + #0: ToddCoxeter: lookahead_next() is now max(f x a = 190,092, m = 10,000) (-4,809,908) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 95,046 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 START + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 95,046 | 7,869,285 | 7,964,331 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,177 | 7 | 100.0% + #0: ToddCoxeter: time | run 0 = 939ms | all runs = 939ms | elapsed = 939ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 STOP + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.2.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.2.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.2 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.3.2 | active | killed | defined + #0: ToddCoxeter: nodes | 95,040 | 7,869,292 | 7,964,332 + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.3.0 | -6 | +7 | +1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 380,160 | 0 | 100.0% + #0: ToddCoxeter: diff 0.3.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.3.0 | -17 | -7 | +0.0% + #0: ToddCoxeter: phase 0.3 = 13ms | run 0 = 952ms | all runs = 952ms | elapsed = 952ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 1 | 0 | 2 | 0 + #0: ToddCoxeter: time spent in phases | 449ms (47%) | - (0%) | 502ms (53%) | - (0%) + #0: ToddCoxeter: phase 0.3 = 14ms | run 0 = 953ms | all runs = 953ms | elapsed = 953ms + ``` + +=== "ACE" + + Coming soon! + +:simple-ticktick: The computed size of the group matches the size of the group +provided on [the ATLAS][atlas]: $95,040$. + +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: + https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m22.md b/docs/examples/atlas/mathieu/m22.md new file mode 100644 index 0000000..160309e --- /dev/null +++ b/docs/examples/atlas/mathieu/m22.md @@ -0,0 +1,536 @@ +# Mathieu group M~22~ + +> Order: $443,520$ + +> Presentation: +> $\langle{ a, b \mid a^2 = b^4 = (ab)^{11} = (ab^2)^5 = [a,bab]^3 = (ababab^{−1})^5 = 1 }\rangle$ + +On this page, we verify that the above claimed presentation of the Mathieu group +M~22~ defines a group of order $443,520$. + +## The code + +=== "Python" + + In [libsemigroups_pybind11][], the following script constructs the presentation + for M~11~ and runs the Todd-Coxeter algorithm. + + ```python + from libsemigroups_pybind11 import Presentation, ToddCoxeter, congruence_kind, presentation + from libsemigroups_pybind11.words import parse_relations + + # Setup the presentation object with the empty and inverses, so it can represent a group + p = Presentation("abAB") + p.contains_empty_word(True) + presentation.add_inverse_rules(p, "ABab") + + # Add the defining relations + presentation.add_rule(p, parse_relations("a^2"), "") + presentation.add_rule(p, parse_relations("b^4"), "") + presentation.add_rule(p, parse_relations("(ab)^11"), "") + presentation.add_rule(p, parse_relations("(ab^2)^5"), "") + presentation.add_rule(p, parse_relations("(a,bab)^3"), "") + presentation.add_rule(p, parse_relations("(ababaB)^5"), "") + + + # Run the Todd-Coxeter algorithm + tc = ToddCoxeter(congruence_kind.twosided, p) + tc.run() + + assert tc.number_of_classes() == 443520 + ``` + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Running the above script produces the following output: + + ??? info "Output from the Python script" + + ``` + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 START (strategy() = hlt) + #0: ToddCoxeter: |A| = 4, |R| = 10, |u| + |v| ∈ [2, 30], ∑(|u| + |v|) = 105 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 START + #0: ToddCoxeter: HLT 0.0.0 | active | killed | defined + #0: ToddCoxeter: nodes | 1 | 0 | 1 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 0 | 4 | 0.0% + #0: ToddCoxeter: time | run 0 = 23µs | all runs = 23µs | elapsed = 78µs + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.0 STOP + #0: ToddCoxeter: HLT 0.0.1 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 + #0: ToddCoxeter: diff 0.0.0 | +5,000,017 | +1,632,158 | +6,632,175 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% + #0: ToddCoxeter: diff 0.0.0 | +5,679,076 | +14,320,992 | +28.4% + #0: ToddCoxeter: phase 0.0 = 418ms | run 0 = 418ms | all runs = 418ms | elapsed = 418ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.1.0 | active | killed | defined + #0: ToddCoxeter: nodes | 5,000,018 | 1,632,158 | 6,632,176 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 5,679,076 | 14,320,996 | 28.4% + #0: ToddCoxeter: time | run 0 = 418ms | all runs = 418ms | elapsed = 418ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 5,000,018 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.1 STOP + #0: ToddCoxeter: LOOKAHEAD 0.1.1 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: diff 0.1.0 | -2,576,305 | +2,576,305 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: diff 0.1.0 | +2,136,367 | -12,441,587 | +52.2% + #0: ToddCoxeter: phase 0.1 = 398ms | run 0 = 816ms | all runs = 816ms | elapsed = 816ms + #0: ToddCoxeter: lookahead_next() is now max(f x a = 4,847,426, m = 10,000) (-152,574) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 2,423,713 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 5,000,000 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 START + #0: ToddCoxeter: HLT 0.2.0 | active | killed | defined + #0: ToddCoxeter: nodes | 2,423,713 | 4,208,463 | 6,632,176 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 7,815,443 | 1,879,409 | 80.6% + #0: ToddCoxeter: time | run 0 = 816ms | all runs = 816ms | elapsed = 816ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.2 STOP + #0: ToddCoxeter: HLT 0.2.1 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: diff 0.2.0 | +2,423,761 | +111,995 | +2,535,756 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: diff 0.2.0 | +2,607,394 | +7,087,650 | -26.9% + #0: ToddCoxeter: phase 0.2 = 78ms | run 0 = 894ms | all runs = 894ms | elapsed = 894ms + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.3 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.3.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,474 | 4,320,458 | 9,167,932 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 10,422,837 | 8,967,059 | 53.8% + #0: ToddCoxeter: time | run 0 = 894ms | all runs = 894ms | elapsed = 894ms + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,474 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.3.1 | active | killed | defined + #1: ToddCoxeter: nodes | 4,720,512 | 4,447,422 | 9,167,932 + #1: ToddCoxeter: diff 0.3.0 | -126,962 | +126,964 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 10,288,113 | 8,593,935 | 54.5% + #1: ToddCoxeter: diff 0.3.0 | -134,724 | -373,124 | +0.7% + #1: ToddCoxeter: phase 0.3 = 105ms | run 0 = 1.000s | all runs = 1.000s | elapsed = 1.000s + #1: ToddCoxeter: lookahead progress | ~17.5% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.3 STOP + #0: ToddCoxeter: LOOKAHEAD 0.3.2 | active | killed | defined + #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 + #0: ToddCoxeter: diff 0.3.1 | -1,208,112 | +1,208,110 | +0 + #0: ToddCoxeter: diff 0.3.0 | -1,335,074 | +1,335,074 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% + #0: ToddCoxeter: diff 0.3.1 | +1,203,674 | -6,036,122 | +27.3% + #0: ToddCoxeter: diff 0.3.0 | +1,068,950 | -6,409,246 | +28.0% + #0: ToddCoxeter: phase 0.3 = 556ms | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s + #0: ToddCoxeter: lookahead_next() is now 4,847,426 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 7,024,800 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 1,211,868 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 3,512,400 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 1,335,074 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.4 START + #0: ToddCoxeter: HLT 0.4.0 | active | killed | defined + #0: ToddCoxeter: nodes | 3,512,400 | 5,655,532 | 9,167,932 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 11,491,787 | 2,557,813 | 81.8% + #0: ToddCoxeter: time | run 0 = 1.451s | all runs = 1.451s | elapsed = 1.451s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.4 STOP + #0: ToddCoxeter: HLT 0.4.1 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 + #0: ToddCoxeter: diff 0.4.0 | +1,335,049 | +48,097 | +1,383,146 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% + #0: ToddCoxeter: diff 0.4.0 | +1,442,482 | +3,897,714 | -15.1% + #0: ToddCoxeter: phase 0.4 = 62ms | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.5 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.5.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,847,449 | 5,703,629 | 10,551,078 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 12,934,269 | 6,455,527 | 66.7% + #0: ToddCoxeter: time | run 0 = 1.513s | all runs = 1.513s | elapsed = 1.514s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,847,449 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.5.1 | active | killed | defined + #1: ToddCoxeter: nodes | 4,565,240 | 5,985,863 | 10,551,078 + #1: ToddCoxeter: diff 0.5.0 | -282,209 | +282,234 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 13,023,236 | 5,237,724 | 71.3% + #1: ToddCoxeter: diff 0.5.0 | +88,967 | -1,217,803 | +4.6% + #1: ToddCoxeter: phase 0.5 = 487ms | run 0 = 2.001s | all runs = 2.001s | elapsed = 2.001s + #1: ToddCoxeter: lookahead progress | ~77.2% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.5 STOP + #0: ToddCoxeter: LOOKAHEAD 0.5.2 | active | killed | defined + #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 + #0: ToddCoxeter: diff 0.5.1 | -431,134 | +431,109 | +0 + #0: ToddCoxeter: diff 0.5.0 | -713,343 | +713,343 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% + #0: ToddCoxeter: diff 0.5.1 | +534,316 | -2,258,852 | +10.7% + #0: ToddCoxeter: diff 0.5.0 | +623,283 | -3,476,655 | +15.3% + #0: ToddCoxeter: phase 0.5 = 642ms | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s + #0: ToddCoxeter: lookahead_next() is now n x f = 9,694,852 (+4,847,426) + #0: ToddCoxeter: because: l < (l + a) / t = 1,211,862 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 4,134,106 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 713,343 + #0: ToddCoxeter: n = lookahead_next() = 4,847,426 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.6 START + #0: ToddCoxeter: HLT 0.6.0 | active | killed | defined + #0: ToddCoxeter: nodes | 4,134,106 | 6,416,972 | 10,551,078 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 13,557,552 | 2,978,872 | 82.0% + #0: ToddCoxeter: time | run 0 = 2.156s | all runs = 2.156s | elapsed = 2.156s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.6 STOP + #0: ToddCoxeter: HLT 0.6.1 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 + #0: ToddCoxeter: diff 0.6.0 | +5,560,767 | +240,133 | +5,800,900 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% + #0: ToddCoxeter: diff 0.6.0 | +6,017,818 | +16,225,250 | -31.5% + #0: ToddCoxeter: phase 0.6 = 425ms | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.7 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.7.0 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,873 | 6,657,105 | 16,351,978 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 19,575,370 | 19,204,122 | 50.5% + #0: ToddCoxeter: time | run 0 = 2.582s | all runs = 2.582s | elapsed = 2.582s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,873 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.7.1 | active | killed | defined + #1: ToddCoxeter: nodes | 9,521,847 | 6,830,131 | 16,351,978 + #1: ToddCoxeter: diff 0.7.0 | -173,026 | +173,026 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 19,432,594 | 18,654,794 | 51.0% + #1: ToddCoxeter: diff 0.7.0 | -142,776 | -549,328 | +0.5% + #1: ToddCoxeter: phase 0.7 = 418ms | run 0 = 3.001s | all runs = 3.001s | elapsed = 3.001s + #1: ToddCoxeter: lookahead progress | ~33.5% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.7 STOP + #0: ToddCoxeter: LOOKAHEAD 0.7.2 | active | killed | defined + #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 + #0: ToddCoxeter: diff 0.7.1 | -2,737,817 | +2,737,817 | +0 + #0: ToddCoxeter: diff 0.7.0 | -2,910,843 | +2,910,843 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% + #0: ToddCoxeter: diff 0.7.1 | +2,722,205 | -13,673,473 | +30.6% + #0: ToddCoxeter: diff 0.7.0 | +2,579,429 | -14,222,801 | +31.2% + #0: ToddCoxeter: phase 0.7 = 1.109s | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s + #0: ToddCoxeter: lookahead_next() is now 9,694,852 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 13,568,060 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 2,423,718 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 6,784,030 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 2,910,843 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.8 START + #0: ToddCoxeter: HLT 0.8.0 | active | killed | defined + #0: ToddCoxeter: nodes | 6,784,030 | 9,567,948 | 16,351,978 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 22,154,799 | 4,981,321 | 81.6% + #0: ToddCoxeter: time | run 0 = 3.691s | all runs = 3.691s | elapsed = 3.691s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.8 STOP + #0: ToddCoxeter: HLT 0.8.1 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 + #0: ToddCoxeter: diff 0.8.0 | +2,910,824 | +107,771 | +3,018,595 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% + #0: ToddCoxeter: diff 0.8.0 | +3,142,459 | +8,500,837 | -16.4% + #0: ToddCoxeter: phase 0.8 = 113ms | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.9 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.9.0 | active | killed | defined + #0: ToddCoxeter: nodes | 9,694,854 | 9,675,719 | 19,370,573 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 25,297,258 | 13,482,158 | 65.2% + #0: ToddCoxeter: time | run 0 = 3.805s | all runs = 3.805s | elapsed = 3.805s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 9,694,854 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.9.1 | active | killed | defined + #1: ToddCoxeter: nodes | 9,601,434 | 9,769,139 | 19,370,573 + #1: ToddCoxeter: diff 0.9.0 | -93,420 | +93,420 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 25,215,676 | 13,190,060 | 65.7% + #1: ToddCoxeter: diff 0.9.0 | -81,582 | -292,098 | +0.4% + #1: ToddCoxeter: phase 0.9 = 196ms | run 0 = 4.001s | all runs = 4.001s | elapsed = 4.001s + #1: ToddCoxeter: lookahead progress | ~16.5% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.9.2 | active | killed | defined + #1: ToddCoxeter: nodes | 8,331,834 | 11,038,768 | 19,370,573 + #1: ToddCoxeter: diff 0.9.1 | -1,269,600 | +1,269,629 | +0 + #1: ToddCoxeter: diff 0.9.0 | -1,363,020 | +1,363,049 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 26,231,811 | 7,095,525 | 78.7% + #1: ToddCoxeter: diff 0.9.1 | +1,016,135 | -6,094,535 | +13.1% + #1: ToddCoxeter: diff 0.9.0 | +934,553 | -6,386,633 | +13.5% + #1: ToddCoxeter: phase 0.9 = 1.197s | run 0 = 5.001s | all runs = 5.001s | elapsed = 5.001s + #1: ToddCoxeter: lookahead progress | ~87.1% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.9 STOP + #0: ToddCoxeter: LOOKAHEAD 0.9.3 | active | killed | defined + #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 + #0: ToddCoxeter: diff 0.9.2 | -245,311 | +245,282 | +0 + #0: ToddCoxeter: diff 0.9.0 | -1,608,331 | +1,608,331 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% + #0: ToddCoxeter: diff 0.9.2 | +323,277 | -1,304,521 | +3.4% + #0: ToddCoxeter: diff 0.9.0 | +1,257,830 | -7,691,154 | +16.9% + #0: ToddCoxeter: phase 0.9 = 1.320s | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s + #0: ToddCoxeter: lookahead_next() is now n x f = 19,389,704 (+9,694,852) + #0: ToddCoxeter: because: l < (l + a) / t = 2,423,713 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 8,086,523 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 1,608,331 + #0: ToddCoxeter: n = lookahead_next() = 9,694,852 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.10 START + #0: ToddCoxeter: HLT 0.10.0 | active | killed | defined + #0: ToddCoxeter: nodes | 8,086,523 | 11,284,050 | 19,370,573 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 26,555,088 | 5,791,004 | 82.1% + #0: ToddCoxeter: time | run 0 = 5.125s | all runs = 5.125s | elapsed = 5.125s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.10 STOP + #0: ToddCoxeter: HLT 0.10.1 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 + #0: ToddCoxeter: diff 0.10.0 | +11,303,227 | +489,785 | +11,793,012 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% + #0: ToddCoxeter: diff 0.10.0 | +12,231,652 | +32,981,256 | -32.1% + #0: ToddCoxeter: phase 0.10 = 829ms | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.11 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.11.0 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,750 | 11,773,835 | 31,163,585 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 38,786,740 | 38,772,260 | 50.0% + #0: ToddCoxeter: time | run 0 = 5.955s | all runs = 5.955s | elapsed = 5.955s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,750 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.1 | active | killed | defined + #1: ToddCoxeter: nodes | 19,361,711 | 11,801,893 | 31,163,585 + #1: ToddCoxeter: diff 0.11.0 | -28,039 | +28,058 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 38,761,553 | 38,685,291 | 50.0% + #1: ToddCoxeter: diff 0.11.0 | -25,187 | -86,969 | +0.0% + #1: ToddCoxeter: phase 0.11 = 46ms | run 0 = 6.002s | all runs = 6.002s | elapsed = 6.002s + #1: ToddCoxeter: lookahead progress | ~4.6% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.2 | active | killed | defined + #1: ToddCoxeter: nodes | 18,900,346 | 12,263,243 | 31,163,585 + #1: ToddCoxeter: diff 0.11.1 | -461,365 | +461,350 | +0 + #1: ToddCoxeter: diff 0.11.0 | -489,404 | +489,408 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 38,376,840 | 37,224,544 | 50.8% + #1: ToddCoxeter: diff 0.11.1 | -384,713 | -1,460,747 | +0.7% + #1: ToddCoxeter: diff 0.11.0 | -409,900 | -1,547,716 | +0.8% + #1: ToddCoxeter: phase 0.11 = 1.047s | run 0 = 7.002s | all runs = 7.002s | elapsed = 7.002s + #1: ToddCoxeter: lookahead progress | ~38.4% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.11.3 | active | killed | defined + #1: ToddCoxeter: nodes | 14,438,129 | 16,725,554 | 31,163,585 + #1: ToddCoxeter: diff 0.11.2 | -4,462,217 | +4,462,311 | +0 + #1: ToddCoxeter: diff 0.11.0 | -4,951,621 | +4,951,719 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 42,716,669 | 15,035,847 | 74.0% + #1: ToddCoxeter: diff 0.11.2 | +4,339,829 | -22,188,697 | +23.2% + #1: ToddCoxeter: diff 0.11.0 | +3,929,929 | -23,736,413 | +24.0% + #1: ToddCoxeter: phase 0.11 = 2.047s | run 0 = 8.002s | all runs = 8.002s | elapsed = 8.002s + #1: ToddCoxeter: lookahead progress | ~72.2% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.11 STOP + #0: ToddCoxeter: LOOKAHEAD 0.11.4 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: diff 0.11.3 | -1,010,619 | +1,010,521 | +0 + #0: ToddCoxeter: diff 0.11.0 | -5,962,240 | +5,962,240 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: diff 0.11.3 | +1,165,844 | -5,208,320 | +7.7% + #0: ToddCoxeter: diff 0.11.0 | +5,095,773 | -28,944,733 | +31.7% + #0: ToddCoxeter: phase 0.11 = 2.208s | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s + #0: ToddCoxeter: lookahead_next() is now 19,389,704 (+0) + #0: ToddCoxeter: because: + #0: ToddCoxeter: 1. n <= f x a = 26,855,020 + #0: ToddCoxeter: 2. a <= n + #0: ToddCoxeter: 3. l >= (l + a) / t = 4,847,437 + #0: ToddCoxeter: where: a = number_of_nodes_active() = 13,427,510 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: l = nodes killed in lookahead = 5,962,240 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + #0: ToddCoxeter: t = lookahead_growth_threshold() = 4 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.12 START + #0: ToddCoxeter: HLT 0.12.0 | active | killed | defined + #0: ToddCoxeter: nodes | 13,427,510 | 17,736,075 | 31,163,585 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 43,882,513 | 9,827,527 | 81.7% + #0: ToddCoxeter: time | run 0 = 8.163s | all runs = 8.163s | elapsed = 8.163s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.12 STOP + #0: ToddCoxeter: HLT 0.12.1 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: diff 0.12.0 | +5,962,266 | +223,813 | +6,186,079 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: diff 0.12.0 | +6,442,067 | +17,406,997 | -16.8% + #0: ToddCoxeter: phase 0.12 = 230ms | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.13 START (lookahead_extent() = partial, lookahead_style() = hlt) + #0: ToddCoxeter: LOOKAHEAD 0.13.0 | active | killed | defined + #0: ToddCoxeter: nodes | 19,389,776 | 17,959,888 | 37,349,664 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 50,324,580 | 27,234,524 | 64.9% + #0: ToddCoxeter: time | run 0 = 8.393s | all runs = 8.393s | elapsed = 8.393s + #0: ToddCoxeter: because a >= n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 19,389,776 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.1 | active | killed | defined + #1: ToddCoxeter: nodes | 19,186,302 | 18,163,362 | 37,349,664 + #1: ToddCoxeter: diff 0.13.0 | -203,474 | +203,474 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 50,106,203 | 26,639,005 | 65.3% + #1: ToddCoxeter: diff 0.13.0 | -218,377 | -595,519 | +0.4% + #1: ToddCoxeter: phase 0.13 = 609ms | run 0 = 9.002s | all runs = 9.002s | elapsed = 9.002s + #1: ToddCoxeter: lookahead progress | ~20.7% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.2 | active | killed | defined + #1: ToddCoxeter: nodes | 18,905,330 | 18,444,334 | 37,349,664 + #1: ToddCoxeter: diff 0.13.1 | -280,972 | +280,972 | +0 + #1: ToddCoxeter: diff 0.13.0 | -484,446 | +484,446 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 49,829,308 | 25,792,012 | 65.9% + #1: ToddCoxeter: diff 0.13.1 | -276,895 | -846,993 | +0.6% + #1: ToddCoxeter: diff 0.13.0 | -495,272 | -1,442,512 | +1.0% + #1: ToddCoxeter: phase 0.13 = 1.610s | run 0 = 10.003s | all runs = 10.003s | elapsed = 10.003s + #1: ToddCoxeter: lookahead progress | ~54.1% + #0: ToddCoxeter: large collapse, number of coincidences 100,000 >= 100,000 = large_collapse()! + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.3 | active | killed | defined + #1: ToddCoxeter: nodes | 11,154,426 | 26,195,391 | 37,349,664 + #1: ToddCoxeter: diff 0.13.2 | -7,750,904 | +7,751,057 | +0 + #1: ToddCoxeter: diff 0.13.0 | -8,235,350 | +8,235,503 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 0 | 44,617,704 | 0.0% + #1: ToddCoxeter: diff 0.13.2 | -49,829,308 | +18,825,692 | -65.9% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | +17,383,180 | -64.9% + #1: ToddCoxeter: phase 0.13 = 2.610s | run 0 = 11.003s | all runs = 11.003s | elapsed = 11.003s + #1: ToddCoxeter: lookahead progress | ~66.6% + ++++++++++++++++++++++++++++++++ + #1: ToddCoxeter: LOOKAHEAD 0.13.4 | active | killed | defined + #1: ToddCoxeter: nodes | 2,148,036 | 35,201,729 | 37,349,664 + #1: ToddCoxeter: diff 0.13.3 | -9,006,390 | +9,006,338 | +0 + #1: ToddCoxeter: diff 0.13.0 | -17,241,740 | +17,241,841 | +0 + #1: ToddCoxeter: | active | missing | % complete + #1: ToddCoxeter: edges | 0 | 8,592,144 | 0.0% + #1: ToddCoxeter: diff 0.13.3 | +0 | -36,025,560 | +0.0% + #1: ToddCoxeter: diff 0.13.0 | -50,324,580 | -18,642,380 | -64.9% + #1: ToddCoxeter: phase 0.13 = 3.610s | run 0 = 12.003s | all runs = 12.003s | elapsed = 12.003s + #1: ToddCoxeter: lookahead progress | ~66.6% + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: LOOKAHEAD 0.13 STOP + #0: ToddCoxeter: LOOKAHEAD 0.13.5 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.13.4 | -1,704,516 | +1,704,415 | +0 + #0: ToddCoxeter: diff 0.13.0 | -18,946,256 | +18,946,256 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.13.4 | +1,774,080 | -8,592,144 | +100.0% + #0: ToddCoxeter: diff 0.13.0 | -48,550,500 | -27,234,524 | +35.1% + #0: ToddCoxeter: phase 0.13 = 3.928s | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s + #0: ToddCoxeter: lookahead_next() is now max(f x a = 887,040, m = 10,000) (-18,502,664) + #0: ToddCoxeter: because f x a < n + #0: ToddCoxeter: where: a = number_of_nodes_active() = 443,520 + #0: ToddCoxeter: f = lookahead_growth_factor() = 2 + #0: ToddCoxeter: m = lookahead_min() = 10,000 + #0: ToddCoxeter: n = lookahead_next() = 19,389,704 + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.14 START + #0: ToddCoxeter: HLT 0.14.0 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: time | run 0 = 12.321s | all runs = 12.321s | elapsed = 12.321s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.14 STOP + #0: ToddCoxeter: HLT 0.14.1 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.14.0 | +0 | +0 | +0.0% + #0: ToddCoxeter: phase 0.14 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: HLT 0.15.2 | active | killed | defined + #0: ToddCoxeter: nodes | 443,520 | 36,906,144 | 37,349,664 + #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0 + #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0 + #0: ToddCoxeter: | active | missing | % complete + #0: ToddCoxeter: edges | 1,774,080 | 0 | 100.0% + #0: ToddCoxeter: diff 0.15.1 | +0 | +0 | +0.0% + #0: ToddCoxeter: diff 0.15.0 | +0 | +0 | +0.0% + #0: ToddCoxeter: phase 0.15 = 108ms | run 0 = 12.430s | all runs = 12.430s | elapsed = 12.430s + ++++++++++++++++++++++++++++++++ + #0: ToddCoxeter: RUN 0 STOP (finished) + #0: ToddCoxeter: run 0 | lookahead | lookbehind | hlt | felsch + #0: ToddCoxeter: num. phases | 7 | 0 | 8 | 0 + #0: ToddCoxeter: time spent in phases | 10.163s (82%) | - (0%) | 2.267s (18%) | - (0%) + #0: ToddCoxeter: phase 0.15 = 114ms | run 0 = 12.436s | all runs = 12.436s | elapsed = 12.436s + ``` + +=== "ACE" + + Coming soon! + +:simple-ticktick: The computed size of the group matches the size of the group +provided on [the ATLAS][atlas]: $443,520$. + +[atlas]: https://brauer.maths.qmul.ac.uk/Atlas/v3/spor/ +[libsemigroups_pybind11]: + https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/examples/atlas/mathieu/m23/index.md b/docs/examples/atlas/mathieu/m23/index.md new file mode 100644 index 0000000..6d877fa --- /dev/null +++ b/docs/examples/atlas/mathieu/m23/index.md @@ -0,0 +1,12 @@ +# Mathieu group M~23~ + +> Order: $10,200,960$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the Mathieu group M~23~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/examples/atlas/mathieu/m24/index.md b/docs/examples/atlas/mathieu/m24/index.md new file mode 100644 index 0000000..99166da --- /dev/null +++ b/docs/examples/atlas/mathieu/m24/index.md @@ -0,0 +1,12 @@ +# Mathieu group M~24~ + +> Order: $244,823,040$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the Mathieu group M~24~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/examples/atlas/misc/t.md b/docs/examples/atlas/misc/t.md new file mode 100644 index 0000000..512ded2 --- /dev/null +++ b/docs/examples/atlas/misc/t.md @@ -0,0 +1,28 @@ +# Tits group T + +> Order: $17,971,200$ + +> Presentation: TODO + +On this page, we verify that the above claimed presentation of the Tits group T +defines a group of order $17,971,200$. + +## The code + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/monster-sections/fi22/index.md b/docs/examples/atlas/monster-sections/fi22/index.md new file mode 100644 index 0000000..042bca6 --- /dev/null +++ b/docs/examples/atlas/monster-sections/fi22/index.md @@ -0,0 +1,12 @@ +# Fischer group Fi~22~ + +> Order: $64,561,751,654,400$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the Fischer group Fi~22~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/examples/atlas/monster-sections/he/index.md b/docs/examples/atlas/monster-sections/he/index.md new file mode 100644 index 0000000..c2f88a7 --- /dev/null +++ b/docs/examples/atlas/monster-sections/he/index.md @@ -0,0 +1,12 @@ +# Held group He + +> Order: $4,030,387,200$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the Held group He define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/examples/atlas/pariahs/j1.md b/docs/examples/atlas/pariahs/j1.md new file mode 100644 index 0000000..ef2c3d5 --- /dev/null +++ b/docs/examples/atlas/pariahs/j1.md @@ -0,0 +1,28 @@ +# Janko group J~1~ + +> Order: $175,560$ + +> Presentation: TODO + +On this page, we verify that the above claimed presentation of the Janko group J~1~ +defines a group of order $175,560$. + +## The code + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/pariahs/j3.md b/docs/examples/atlas/pariahs/j3.md new file mode 100644 index 0000000..4962867 --- /dev/null +++ b/docs/examples/atlas/pariahs/j3.md @@ -0,0 +1,28 @@ +# Janko group J~3~ + +> Order: $50,232,960$ + +> Presentation: TODO + +On this page, we verify that the above claimed presentation of the Janko group J~3~ +defines a group of order $50,232,960$. + +## The code + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! + +## The output + +=== "Python" + + Coming soon! + +=== "ACE" + + Coming soon! diff --git a/docs/examples/atlas/pariahs/j4/index.md b/docs/examples/atlas/pariahs/j4/index.md new file mode 100644 index 0000000..5907a8d --- /dev/null +++ b/docs/examples/atlas/pariahs/j4/index.md @@ -0,0 +1,12 @@ +# Janko group J~4~ + +> Order: $86,775,571,046,077,562,880$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the Janko group J~4~ define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/examples/atlas/pariahs/ru/index.md b/docs/examples/atlas/pariahs/ru/index.md new file mode 100644 index 0000000..8bc0864 --- /dev/null +++ b/docs/examples/atlas/pariahs/ru/index.md @@ -0,0 +1,12 @@ +# Rudvalis group Ru + +> Order: $145,926,144,000$ + +> Presentation: TODO + +On this page, we provide links to verifications that the maximal subgroups of +the Rudvalis group Ru define groups of the correct order. + +## Maximal subgroups + +The following are maximal subgroups that have been verified: diff --git a/docs/case-studies/cong-latt.md b/docs/examples/cong-latt.md similarity index 100% rename from docs/case-studies/cong-latt.md rename to docs/examples/cong-latt.md diff --git a/docs/case-studies/gis.md b/docs/examples/gis.md similarity index 100% rename from docs/case-studies/gis.md rename to docs/examples/gis.md diff --git a/docs/examples/index.md b/docs/examples/index.md new file mode 100644 index 0000000..e258f97 --- /dev/null +++ b/docs/examples/index.md @@ -0,0 +1,13 @@ +# Examples + +This page contains various links that explain how the +[Semigroups package for GAP][] and/or [libsemigroups_pybind11][] have been used +to conduct mathematical research. + +Please use the menu at the left or the links below: + +- [Short presentations for transformation monoids](short.md) +- [Verifying presentations in the ATLAS of Finite Groups](atlas/index.md) + +[Semigroups package for GAP]: https://semigroups.github.io/Semigroups/ +[libsemigroups_pybind11]: https://libsemigroups.github.io/libsemigroups_pybind11/index.html diff --git a/docs/case-studies/short.md b/docs/examples/short.md similarity index 100% rename from docs/case-studies/short.md rename to docs/examples/short.md diff --git a/docs/case-studies/stephen.md b/docs/examples/stephen.md similarity index 100% rename from docs/case-studies/stephen.md rename to docs/examples/stephen.md diff --git a/docs/case-studies/trans-rep.md b/docs/examples/trans-rep.md similarity index 100% rename from docs/case-studies/trans-rep.md rename to docs/examples/trans-rep.md diff --git a/docs/stylesheets/extra.css b/docs/stylesheets/extra.css new file mode 100644 index 0000000..8f73613 --- /dev/null +++ b/docs/stylesheets/extra.css @@ -0,0 +1,47 @@ +/* .atlas-summary { + text-align: center; +} */ + +.column { + float: left; + width: 50%; +} + +/* Clear floats after the columns */ +.row:after { + content: ""; + display: table; + clear: both; +} + +.atlas-summary table:not([class]) { + th:not([align]), + td:not([align]) { + text-align: center; /* Reset alignment for table cells */ + } +} + +.atlas-summary a { + color: #000000; + text-decoration: none; +} + +.correct-size { + background-color: #4dac26; +} + +.correct-index { + background-color: #b8e186; +} + +.incorrect-size { + background-color: #f1b6da; +} + +.could-not-verify { + background-color: #cccccc; +} + +.no-presentation { + background-color: grey; +} diff --git a/mkdocs.yml b/mkdocs.yml index a802fc4..18b827c 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -16,9 +16,40 @@ nav: - "Python: Semigroups defined by generators": py/generated.md - "Python: Finitely presented semigroups": py/fp.md - "Python: Worksheet": py/worksheet.md - - Case studies: - - case-studies/index.md - - case-studies/short.md + - Examples: + - examples/index.md + - examples/short.md + - "Verifying presentations in the ATLAS of Finite Groups": + - examples/atlas/index.md + - "Mathieu groups": + - examples/atlas/mathieu/m11.md + - examples/atlas/mathieu/m12.md + - examples/atlas/mathieu/m22.md + - "Mathieu group M23": + - examples/atlas/mathieu/m23/index.md + - "Mathieu group M24": + - examples/atlas/mathieu/m24/index.md + - "Leech lattice groups": + - examples/atlas/leech-lattice/hs.md + - examples/atlas/leech-lattice/j2.md + - "Conway group Co2": + - examples/atlas/leech-lattice/co2/index.md + - "McLaughlin group McL": + - examples/atlas/leech-lattice/mcl/index.md + - "Monster sections": + - "Held group He": + - examples/atlas/monster-sections/he/index.md + - "Fischer group Fi22": + - examples/atlas/monster-sections/fi22/index.md + - "Pariahs": + - examples/atlas/pariahs/j1.md + - examples/atlas/pariahs/j3.md + - "Rudvalis group Ru": + - examples/atlas/pariahs/ru/index.md + - "Janko group J4": + - examples/atlas/pariahs/j4/index.md + - "Miscellaneous": + - examples/atlas/misc/t.md theme: name: material @@ -45,6 +76,7 @@ theme: - content.code.copy - content.code.select - content.footnote.tooltips + - content.tabs.link plugins: # - optimize @@ -71,6 +103,10 @@ markdown_extensions: - pymdownx.keys - pymdownx.arithmatex: generic: true + - pymdownx.emoji: + emoji_index: !!python/name:material.extensions.emoji.twemoji + emoji_generator: !!python/name:material.extensions.emoji.to_svg + - pymdownx.tilde copyright: Copyright © 2026 Reinis Cirpons, Joe Edwards and James Mitchell @@ -83,6 +119,9 @@ extra: icon: fontawesome/brands/github link: https://www.github.com/libsemigroups/libsemigroups_pybind11 +extra_css: + - stylesheets/extra.css + extra_javascript: - javascripts/mathjax.js - https://unpkg.com/mathjax@3/es5/tex-mml-chtml.js diff --git a/problem-1.gap b/worksheet/gap-solutions/problem-1.gap similarity index 100% rename from problem-1.gap rename to worksheet/gap-solutions/problem-1.gap diff --git a/problem-2.gap b/worksheet/gap-solutions/problem-2.gap similarity index 100% rename from problem-2.gap rename to worksheet/gap-solutions/problem-2.gap diff --git a/problem-3.gap b/worksheet/gap-solutions/problem-3.gap similarity index 100% rename from problem-3.gap rename to worksheet/gap-solutions/problem-3.gap diff --git a/problem-4.gap b/worksheet/gap-solutions/problem-4.gap similarity index 100% rename from problem-4.gap rename to worksheet/gap-solutions/problem-4.gap diff --git a/problem-5.gap b/worksheet/gap-solutions/problem-5.gap similarity index 100% rename from problem-5.gap rename to worksheet/gap-solutions/problem-5.gap diff --git a/problem-6.gap b/worksheet/gap-solutions/problem-6.gap similarity index 100% rename from problem-6.gap rename to worksheet/gap-solutions/problem-6.gap diff --git a/problem-7.gap b/worksheet/gap-solutions/problem-7.gap similarity index 100% rename from problem-7.gap rename to worksheet/gap-solutions/problem-7.gap diff --git a/problem-8.gap b/worksheet/gap-solutions/problem-8.gap similarity index 100% rename from problem-8.gap rename to worksheet/gap-solutions/problem-8.gap diff --git a/problem_1.py b/worksheet/python-solutions/problem_1.py similarity index 100% rename from problem_1.py rename to worksheet/python-solutions/problem_1.py diff --git a/problem_2.py b/worksheet/python-solutions/problem_2.py similarity index 100% rename from problem_2.py rename to worksheet/python-solutions/problem_2.py diff --git a/problem_3.py b/worksheet/python-solutions/problem_3.py similarity index 100% rename from problem_3.py rename to worksheet/python-solutions/problem_3.py diff --git a/problem_4.py b/worksheet/python-solutions/problem_4.py similarity index 100% rename from problem_4.py rename to worksheet/python-solutions/problem_4.py diff --git a/problem_5.py b/worksheet/python-solutions/problem_5.py similarity index 100% rename from problem_5.py rename to worksheet/python-solutions/problem_5.py diff --git a/problem_6.py b/worksheet/python-solutions/problem_6.py similarity index 100% rename from problem_6.py rename to worksheet/python-solutions/problem_6.py diff --git a/worksheet.pdf b/worksheet/worksheet.pdf similarity index 100% rename from worksheet.pdf rename to worksheet/worksheet.pdf diff --git a/worksheet.tex b/worksheet/worksheet.tex similarity index 100% rename from worksheet.tex rename to worksheet/worksheet.tex