Aschbacher 1971
The Nonexistence of Rank Three Permutation Groups of Degree 3250 and Subdegree 57
J. Algebra 19 (1971), 538–540. DOI: 10.1016/0021-8693(71)90087-1.
23 formalized · 0 pending · 0 out of scope · total 23 · all papers · browse source on GitHub
Lemma 1.1 — regular or star
Aschbacher 1971, Lemma 1.1 — 2/2 formalized .lean
- Lemma 1.1 (regular-or-star dichotomy). — A finite simple graph satisfying the strong (λ = 0, μ = 1) common-neighbour condition is either regular or a star with some centre Formalized auto L36
- Lemma 1.1, Moore57 instance. — Moore57 satisfies the strong (0, 1) condition (`IsSRGWith 3250 57 0 1` ⊆ `IsStrongZeroOne`), so the dichotomy applies. In this concrete case the regular branch is realised (Moore57 is 57-regular by definition) Formalized auto L46
Lemma 1.2 — fix inherits star
Aschbacher 1971, Lemma 1.2 — 2/2 formalized .lean
- Lemma 1.2 (Fix inherits strong (0,1)), single-element case. — For any σ ∈ Aut(Γ), the σ-fixed induced subgraph satisfies the strong (λ = 0, μ = 1) common-neighbour condition Formalized auto L37
- Lemma 1.2 (Fix inherits strong (0,1)), subgroup case. — For any finite subgroup `G ≤ Equiv.Perm V` whose elements are all graph automorphisms of a Moore57 graph `Γ`, the induced subgraph on `MulAction.fixedPoints G V` satisfies the strong `(λ=0, μ=1)` common-neighbour cond… Formalized done L50
Lemma 1.3 — valence classification
Aschbacher 1971, Lemma 1.3 — 6/6 formalized .lean
- Lemma 1.3 (`v = k² + 1`). — For any `IsSRGWith n k 0 1` graph with at least one vertex, the vertex count satisfies `n = k² + 1` Formalized auto L52
- Lemma 1.3 arithmetic core — (via Higman 1964 Theorem 1). Given the integrality data `4·k = e² + 3` (equivalently `4k − 3 = e²`) and `e² ∣ 225`, the only possible `k` values are `{1, 3, 7, 57}`. This wraps `Moore57.Papers.Higman1964.theorem1_arit… Formalized done L92
- Lemma 1.3 (full `k ∈ {2, 3, 7, 57}` classification) — discharged `a ≠ b` branch — The paper's content: the `(a ≠ b)` integrality branch of the eigenvalue analysis classifies `k ∈ {1, 3, 7, 57}`. Given the integrality data `4k = e² + 3` and `e² ∣ 225` (the Higman 1964 Theorem 1 integrality hypothese… Formalized done L110
- Lemma 1.3 (paper-faithful conditional dispatch, `a ≠ b` branch). — Proper-signature paper-faithful packaging of the `(a ≠ b)` integrality branch: given the eigenvalue integrality data `4k = e² + 3` and `e² ∣ 225`, conclude `k ∈ {1, 3, 7, 57}`. This is the proper-signature variant of… Formalized done L128
- Lemma 1.3 (`k = 57` instance for Moore57). Formalized auto L134
- Lemma 1.3 (`v = k² + 1 = 3250` instance for Moore57). Formalized auto L139
Lemma 1.4 — involution fix
Aschbacher 1971, Lemma 1.4 — 8/8 formalized .lean
- Lemma 1.4 (1), `k = 57` instance. — For an involution `σ ∈ Aut(Γ)` with `σ ≠ 1`, the existence of a moved adjacent pair `A ~ σA` forces `|Fix(σ)| = k − 1 = 56` Formalized auto L45
- Lemma 1.4 (2), `k = 57` instance — the "minus" branch is realised. — For a non-trivial involution `σ ∈ Aut(Γ)`, `Fix(σ)` is a star (by part 1 combined with Moore57's structural lemma) and `|Fix(σ)| = 56 = k − 1`. So the Moore57 instance of Aschbacher's Lemma 1.4 (2) sits in the `f = k… Formalized auto L59
- Aschbacher 1.4 (2) algebraic core (factored form) — from the quadratic identity `(f − k − 1)(f − k + 1) = 0`, conclude `f = k − 1 ∨ f = k + 1` Formalized done L89
- Aschbacher 1.4 (2) algebraic core (square form) — from `(f − k)² = 1`, conclude `f = k − 1 ∨ f = k + 1`. Equivalent to `asc1_4_arithmetic_core` via the identity `(f − k − 1)(f − k + 1) = (f − k)² − 1` Formalized done L101
- Aschbacher 1.4 (2) iff form — the dichotomy `f = k − 1 ∨ f = k + 1` is equivalent to the quadratic `(f − k − 1)(f − k + 1) = 0` Formalized done L111
- Aschbacher 1.4 (2) Moore57 instance via the algebraic core — for `f = 56, k = 57`, the quadratic identity `(56 − 57)² = 1` gives the dichotomy branch `f = k − 1` (the "minus" branch realised by Moore57). Formalized done L121
- Lemma 1.4 (2) (general star-fix dichotomy `f = k ± 1`) — discharged conditional dispatch — The paper's general dichotomy as a conditional: given the quadratic identity `(f − k)² = 1` from the spectral trace computation, conclude `f = k − 1 ∨ f = k + 1`. Replaces the prior backward-compat True-stub with the… Formalized done L137
- Lemma 1.4 (2) (paper-faithful conditional dispatch). — Proper-signature paper-faithful packaging: given the quadratic identity `(f − k)² = 1` from the spectral trace computation (the deferred-heavy input), conclude the dichotomy `f = k − 1 ∨ f = k + 1`. Delegates to `asc1… Formalized done L151
Main theorem
Aschbacher 1971 — main theorem — 5/5 formalized .lean
- Main theorem (rank-3 non-existence on degree 3250 / subdegree 57). — Formalized in the project-facing form needed for Moore57: a rank-3 action is vertex-transitive, and the stronger `Moore57.Papers.MacajSiran2010.S2.cor_lem2_no_vertex_transitive_aut` rules out any vertex-transitive sub… Formalized done L87
- Main theorem (paper-faithful via vertex-transitivity). — Proper-signature paper-faithful packaging: since any rank-3 transitive permutation group is in particular vertex-transitive (`MulAction.IsPretransitive` on the underlying set), the stronger `MacajSiran2010.S2.cor_lem2… Formalized done L109
- Main theorem (proven form, via vertex-transitivity). — The rank-3 hypothesis implies vertex-transitivity (rank-3 transitive groups are 2-transitive on orbital partitions, hence in particular transitive on `Ω`). Hence the stronger `MacajSiran2010.S2.cor_lem2_no_vertex_tran… Formalized auto L128
- Aschbacher Cor (D4.1, combined classification) — under the Case II arithmetic + involution quadratic, the `(k, f)` pair is fully classified. Inputs: * `4·k = e² + 3` (perfect square discriminant — Case II Lem 7). * `2·(e·f₂) = k·(k·(e + 1) − 2)` (integer multiplicit… Formalized done L175
- Aschbacher Cor Moore57 instance — for `(k, f) = (57, 56)`, the combined classification holds (k = 57 from Higman Thm 1; f = k − 1 from Lem 1.4 part 1) Formalized done L190