Makhnev–Paduchikh 2001
Automorphisms of Aschbacher Graphs
Algebra and Logic 40 (2) (2001), 69–74. DOI: 10.1023/A:1010217919915.
45 formalized · 0 pending · 0 out of scope · total 45 · all papers · browse source on GitHub
Lemma 1 — strong fix
Makhnev–Paduchikh 2001, Lemma 1 — 2/2 formalized .lean
- Lemma 1 (1) (strong (0,1) ⇒ regular or star). — Any finite strong-`(λ = 0, µ = 1)` graph is either regular (every vertex has the same degree, the "Moore graph" branch) or a star with some centre. The Moore-graph branch of the paper's formulation is captured here by… Formalized done L46
- Lemma 1 (2) (`Fix(σ)` is also strong (0,1), single-element case). — For a Moore57 graph Γ and any σ ∈ Aut(Γ), the σ-fixed induced subgraph satisfies the strong (λ = 0, µ = 1) condition Formalized auto L61
Lemma 2 — involution fix
Makhnev–Paduchikh 2001, Lemma 2 — 1/1 formalized .lean
- Lemma 2 (involution fixes a star). — For a Moore57 graph Γ and a non-trivial involution `σ ∈ Aut(Γ)`, the σ-fixed induced subgraph is a star with some center `c`. Wraps `aut_involution_fixedInducedGraph_isStarWithCenter` Formalized auto L37
Lemma 3 — odd-prime fix
Makhnev–Paduchikh 2001, Lemma 3 — 17/17 formalized .lean
- Lemma 3, case (2): order 19, `|Fix| = 1`. — Any order-19 automorphism of Moore57 has exactly one fixed vertex Formalized auto L44
- Lemma 3, case (4): order 11, `|Fix|` is a pentagon (5 vertices). — Any order-11 automorphism of Moore57 has fixed-vertex set of size 5 (induced subgraph is the pentagon `C₅`) Formalized auto L53
- Lemma 3, case (1) arithmetic core: odd prime divisors of `3250`. — For `p` an odd prime dividing `3250`, conclude `p ∈ {5, 13}`. Proof: factor `3250 = 2 · 5^3 · 13` and apply `Nat.Prime.dvd_mul` / `Nat.Prime.dvd_of_dvd_pow` plus `Nat.Prime.eq_one_or_self_of_dvd` for the prime factors Formalized done L65
- Lemma 3, case (1) conditional: empty fix odd-prime is in `{5, 13}`. — For a Moore57 graph automorphism `σ` of odd prime order `p` with `Fix(σ) = ∅`, conclude `p ∈ {5, 13}`. Proof: combine the generic mod-`p` constraint `fixedVertexCount σ ≡ |V| [MOD p]` (= `3250` for Moore57) with `fixe… Formalized done L105
- Lemma 3, case (6) arithmetic core: odd prime divisors of `3200`. — For `p` an odd prime dividing `3200 = 2^7 · 5^2`, conclude `p = 5`. Proof: factor `3200 = 2^7 · 5^2`, apply `Nat.Prime.dvd_mul` / `Nat.Prime.dvd_of_dvd_pow`; the 2-power branch gives `p ≤ 2` (excluded by `p > 2`), and… Formalized done L122
- Lemma 3, case (6) conditional: Hoffman-Singleton fix forces `p = 5`. — For a Moore57 graph automorphism `σ` of odd prime order `p` with `|Fix(σ)| = 50` (the Hoffman-Singleton case), conclude `p = 5`. Proof: the generic mod-`p` constraint gives `50 ≡ 3250 [MOD p]`, so `p ∣ 3200 = 3250 − 5… Formalized done L147
- Lemma 3, case (2) arithmetic core: odd prime divisors of `3249`. — For `p` an odd prime dividing `3249 = 3^2 · 19^2`, conclude `p ∈ {3, 19}`. Proof: factor `3249 = 3^2 · 19^2`, apply `Nat.Prime.dvd_mul` / `Nat.Prime.dvd_of_dvd_pow`; each branch gives a prime-divides-prime collapse vi… Formalized done L167
- Lemma 3, case (2) conditional: singleton fix forces `p ∈ {3, 19}`. — For a Moore57 graph automorphism `σ` of odd prime order `p` with `|Fix(σ)| = 1` (singleton), conclude `p ∈ {3, 19}` (matching the paper's `|X| ∣ 3·19 = 57`). Proof: the generic mod-`p` constraint gives `1 ≡ 3250 [MOD… Formalized done L196
- Lemma 3, case (5) arithmetic core: odd prime divisors of `54`. — For `p` an odd prime dividing `54 = 2 · 3^3`, conclude `p = 3`. Proof: factor `54 = 2 · 3^3`; the 2-branch is excluded by `p > 2`, and the 3-power branch gives `p = 3` Formalized done L214
- Lemma 3, case (5) conditional: Petersen fix forces `p = 3`. — For a Moore57 graph automorphism `σ` of odd prime order `p` fixing a vertex `a` whose σ-fixed-neighbour count is 3 (the Petersen-degree restriction: in Fix(σ) ≅ Petersen, every vertex has 3 neighbours in Fix), conclud… Formalized done L244
- Lemma 3, case (3) arithmetic core: odd prime divisors of `56`. — For `p` an odd prime dividing `56 = 2^3 · 7`, conclude `p = 7` Formalized done L264
- Lemma 3, case (3) conditional: star-leaf fix forces `p = 7`. — For a Moore57 graph automorphism `σ` of odd prime order `p` fixing a star-leaf vertex `a` whose σ-fixed-neighbour count is 1 (only the star centre is fixed and adjacent to `a`), conclude `p = 7`. This is the paper-tig… Formalized done L291
- Lemma 3, case (4) arithmetic core: odd prime divisors of `55`. — For `p` an odd prime dividing `55 = 5 · 11`, conclude `p ∈ {5, 11}` Formalized done L311
- Lemma 3, case (4) conditional: pentagon-vertex fix forces `p ∈ {5, 11}`. — For a Moore57 graph automorphism `σ` of odd prime order `p` fixing a pentagon-vertex `a` whose σ-fixed-neighbour count is 2 (the pentagon `C_5` has degree 2), conclude `p ∈ {5, 11}`. This is the paper-tight restrictio… Formalized done L340
- Lemma 3 unified: any of the 5 shape-degree values forces `p` into the Moore57 odd-prime list `{3, 5, 7, 11, 13, 19}`. — For a Moore57 graph automorphism `σ` of odd prime order `p` fixing some vertex `a` whose σ-fixed-neighbour count `c` is one of the paper-cited Fix-shape degrees `c ∈ {0, 1, 2, 3, 7}` (matching singleton / star-leaf /… Formalized done L370
- Lemma 3 (paper-faithful conditional dispatch). — Proper-signature paper-faithful packaging of three cases of the classification: for σ an odd-prime-order graph automorphism of Moore57, the global fixed-vertex count `fixedVertexCount σ ∈ {0, 1, 50}` determines `p` to… Formalized done L450
- Lemma 3 (general 6-way classification, proper-signature global Fix dispatch). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Three of the six paper cases — case (1) empty fix, case (2) singleton fix, case (6) HS-fix — are fully dispatched here via the globa… Formalized done L476
Lemma 4 — involution good
Makhnev–Paduchikh 2001, Lemma 4 — 1/1 formalized .lean
- Lemma 4 (involution is "good": `|Fix(t)| = 56`). — Every non-trivial involution of a Moore57 graph fixes exactly 56 vertices — this is the `k = 57` instance of the paper's "good" definition `|Fix(t)| = k − 1` Formalized auto L38
Lemmas 5–9 — involution structure
Makhnev–Paduchikh 2001, Lemmas 5–9 (involution-centric structure) [deferred-heavy] — 16/16 formalized .lean
- Lemma 5 abstract conclusion. — Given an involution `t` of `Γ`, two vertices `b, c` with `t b = c` (and hence `t c = b`), and the geometric hypothesis that both `b, c` lie in the closed neighbourhood `[a]` of some star centre `a` (which the structur… Formalized auto L53
- Lemma 5 (paper-faithful conditional). — [done — conditional] Proper-signature paper-faithful: given a graph automorphism involution `t` (`t^2 = 1`), two vertices `b, c` with `t b = c`, and the (deferred- heavy) structural hypothesis that this transposed pai… Formalized auto L64
- Lemma 5 (transposed `b, c ∈ [a]` adjacency, proper-signature). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Given a graph automorphism involution `t`, transposed pair `b, c` (`t b = c`), and the structural hypothesis that the pair is adjace… Formalized done L80
- Lemma 6 abstract conclusion. — The paper's structural conclusion: if `t, s` are both involutions of `G`, both having fix contained in the closed neighbourhood of (their respective) star centres, and `s ≠ t`, then we derive a contradiction Formalized auto L100
- Lemma 6 (paper-faithful conditional uniqueness). — [done — conditional] Proper-signature paper-faithful: given a graph automorphism involution `t` and the (deferred-heavy) structural hypothesis `s = t` (which the paper extracts from the centraliser-of-`t` analysis usi… Formalized auto L110
- Lemma 6 (no second involution, proper-signature). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Given two graph automorphism involutions `s, t` and the structural hypothesis `s = t` (the deferred-heavy content), conclude the pap… Formalized done L126
- Lemma 7 abstract conclusion. — The paper's structural conclusion: a non-identity odd-order element `g ∈ C(t)` has `|Fix(g)| = 50` (the HS-vertex count) Formalized auto L145
- Lemma 7 (paper-faithful conditional HS fix). — [done — conditional] Proper-signature paper-faithful: given a graph automorphism `g` of odd order coprime to 2 with `g ≠ 1`, commuting with the fixed involution `t`, and the (deferred-heavy) structural hypothesis `|Fi… Formalized auto L156
- Lemma 7 (centraliser-of-`t` odd-order HS fix, proper-signature). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Given a graph automorphism `g ≠ 1` commuting with an involution `t` and the structural hypothesis `|Fix(g)| = 50` (the HS-fix conten… Formalized done L173
- Lemma 8 abstract conclusion. — The paper's structural conclusion: `(s * t)^n = 1` for some `n` in the paper's restricted list (`n ∈ {1, 2, 3, 5, 6, 7, 10, 14, 15, 21, 25, 35}`). We package the weaker conclusion `(s * t)^n = 1` with the witness `n`… Formalized auto L194
- Lemma 8 (paper-faithful conditional `st`-order bound). — [done — conditional] Proper-signature paper-faithful: given involutions `s ≠ t` and the (deferred-heavy) structural witness `n ≥ 1` with `(s * t)^n = 1`, the paper claim follows by packaging the witness Formalized auto L204
- Lemma 8 (second involution `st`-order bound, proper-signature). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Given a second involution `s ≠ t` and the structural witness `n ≥ 1` with `(s * t)^n = 1` (the deferred-heavy paper content), conclu… Formalized done L222
- Lemma 9 abstract conclusion. — The paper's combinatorial output: a divisibility `n ∣ 5 ∨ n ∣ 57 ∨ n ∣ 21` for the odd-order subgroup parameter `n` (which becomes `|Y|` in the main decomposition) Formalized auto L244
- Lemma 9 (paper-faithful conditional `|Y|` dispatch). — [done — conditional] Proper-signature paper-faithful: given the (deferred-heavy) divisibility witness produced by the combinatorial argument, the paper's three-way dispatch follows by re-export. This feeds directly in… Formalized auto L254
- Lemma 9 (final structure `|Y|` dispatch, proper-signature). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Given the combinatorial dispatch `n ∣ 5 ∨ n ∣ 57 ∨ n ∣ 21` (the deferred-heavy combinatorial argument output), conclude the paper's… Formalized done L268
- Lemma 9 arithmetic envelope. — The combined divisibility implies `n ≤ 57`, which is the numeric input to the main decomposition Formalized done L279
Main theorem
Makhnev–Paduchikh 2001 — main theorem — 8/8 formalized .lean
- Main theorem (1) (`Fix(t)` is a 56-vertex star). — For any non-trivial involution `t ∈ Aut(Γ)`, `|Fix(t)| = 56` and `Fix(t)` is a star (centered at some vertex) Formalized auto L55
- Main theorem (2) `|Y|` arithmetic bound — Given the paper's structural conclusion `|Y| ∣ 5 ∨ |Y| ∣ 57 ∨ |Y| ∣ 21` (the three possibilities for the odd subgroup `Y` of `G = ⟨Y, t⟩ × X`), conclude `|Y| ≤ 57`. This is the arithmetic envelope of the `|Y|` constra… Formalized done L73
- Main theorem (2) (paper-faithful conditional Y bound). — Proper-signature paper-faithful packaging of the `|Y|` bound: given the paper's three-way dispatch (`|Y| ∣ 5`, `|Y| ∣ 57`, or `|Y| ∣ 21`) for the odd subgroup `Y` of the decomposition `G = ⟨Y, t⟩ × X`, conclude `|Y| ≤… Formalized done L87
- Main theorem (2) (decomposition `G = ⟨Y, t⟩ × X`, proper-signature). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Given the paper's three-way dispatch `|Y| ∣ 5 ∨ |Y| ∣ 57 ∨ |Y| ∣ 21` (the structural decomposition output for `G = ⟨Y, t⟩ × X`, defe… Formalized done L99
- Main theorem (3) `|X|` arithmetic dispatch — Given the paper's four-way dispatch for `Fix(X)` shape and `|X|`: * Star case: `|Y| = 1, |X| = 7`. * Pentagon case: `|Y| ∣ 5, |X| ∣ 55`. * Petersen case: `|Y| ∣ 3, |X| ∣ 27`. * Hoffman-Singleton case: `|Y| ∣ 5 or 7, |… Formalized done L114
- Main theorem (3) `|X|` numeric bound — The `|X|` dispatch gives `|X| ≤ 55` Formalized done L131
- Main theorem (3) (paper-faithful conditional `|X|` dispatch). — Proper-signature paper-faithful packaging of the `|X|` bound: given the paper's four-way dispatch for `Fix(X)` shape and `(|Y|, |X|)` pair (star, pentagon, Petersen, Hoffman-Singleton cases), conclude `|X| ≤ 55`. Dele… Formalized done L153
- Main theorem (3) (`Fix(X)` cases when `X ≠ 1`, proper-signature). — Replaces the prior backward-compat True-stub with a proper-signature proven theorem. Given the paper's four-way dispatch for `Fix(X)` shape and `(|Y|, |X|)` pair (star, pentagon, Petersen, Hoffman-Singleton cases — th… Formalized done L170