Mačaj–Širáň 2010

Search for properties of the missing Moore graph

Linear Algebra Appl. 432 (2010), 2381–2398. DOI: 10.1016/j.laa.2009.07.018.

869 formalized · 13 pending · 0 out of scope · total 882 · all papers · browse source on GitHub

§2 State of the art

33 formalized · 2 pending · 0 out of scope · total 35

Mačaj–Širáň 2010, §2, Lemma 1 [deferred-heavy] — 0/1 formalized, 1 pending .lean
  • Lemma 1. — For any group `X ≤ Aut(Γ)`, the fixed subgraph `Fix(X)` has one of six shapes (six-way classification) Pending deferred L35
Mačaj–Širáň 2010, §2, Lemma 2 — 6/6 formalized .lean
  • Lemma 2 (involution `a₀ = 56`). — The number of fixed points of any involutory automorphism `σ` (with `σ ≠ 1`) of a Moore57 graph equals 56 Formalized auto L42
  • Lemma 2 (involution `a₁ = 112`). — For any involutory automorphism `σ ≠ 1`, `adjacentMovedCount Γ σ = 112` Formalized auto L50
  • Lemma 2 (corollary: no order-4 automorphism). — There is no element of `Aut(Γ)` with order 4. Proof. If `σ ∈ Aut(Γ)` has `orderOf σ = 4`, then `σ ^ 2` is a non-trivial involution-automorphism, so by `CameronCh3.step5_moore57_involution_sign`, `sign (σ ^ 2) = −1`. B… Formalized auto L76
  • Lemma 2 (corollary: no Klein-4 in Aut(Γ)). — For two distinct commuting non-trivial involution-automorphisms `σ, τ`, False follows: `στ` is also a non-trivial involution-automorphism with `sign (στ) = (sign σ)(sign τ) = (−1)(−1) = +1`, contradicting `sign(στ) =… Formalized auto L106
  • Lemma 2 (3): `4 ∤ |G|` for any subgroup `G ≤ Aut(Γ)`. — If `G` is a subgroup of `Equiv.Perm V` whose elements all preserve adjacency of a Moore57 graph `Γ`, then `4 ∤ Fintype.card G`. Proof. The sign homomorphism `signG : G →* ℤˣ`, obtained by restricting `Equiv.Perm.sign`… Formalized auto L158
  • Corollary of Lemma 2: no vertex-transitive subgroup of `Aut(Γ)`. — This is Cameron Ch.3 Theorem 3.13, proved by combining `lem2_four_not_dvd_aut` with orbit-stabilizer. If `G ≤ Aut(Γ)` acts transitively on `V`, then `|G| = |V| · |Stab_v|` for any `v`. Cauchy (`2 ∣ |G|` since `2 ∣ 325… Formalized auto L233
Mačaj–Širáň 2010, §2, Lemma 3 — 3/3 formalized .lean
  • Lemma 3 (χ₁ formula). — χ₁(σ) := trace(E_7 · P_σ) = (1/15)(8 a₀(σ) + a₁(σ) − 65)` Formalized auto L33
  • Lemma 3 (mod-15 congruence). — Once `χ₁(σ)` is known to be an integer `z`, we get `a₁(σ) ≡ 7 a₀(σ) + 5 (mod 15)` Formalized auto L41
  • Lemma 3 (mod-15 congruence, no order hypothesis) — — B4.3 specialization. The integer-trace hypothesis is discharged automatically by `Moore57.aut_E7_trace_int` (B4.3 Step 5 strongest form), which provides `tr(E₇·P_σ) ∈ ℤ` for **any** σ ∈ Aut(Γ) using `orderOf σ` inte… Formalized auto L59
Mačaj–Širáň 2010, §2, Lemma 4 [deferred-heavy] — 8/9 formalized, 1 pending .lean
  • Lemma 4 (six-way classification for prime-order automorphism groups). Pending deferred L48
  • Lemma 4 case (1) [empty Fix odd-prime in {5, 13}]. — Re-exports `Moore57.Papers.MakhnevPaduchikh2001.lem3_case1_empty_fix` Formalized done L59
  • Lemma 4 case (2) [singleton Fix in {3, 19}]. — Re-exports `Moore57.Papers.MakhnevPaduchikh2001.lem3_case2_singleton_fix` Formalized done L70
  • Lemma 4 case (3) [star-leaf Fix = 7]. — Re-exports `Moore57.Papers.MakhnevPaduchikh2001.lem3_case3_star_leaf_fix` Formalized done L81
  • Lemma 4 case (4) [pentagon Fix in {5, 11}]. — Re-exports `Moore57.Papers.MakhnevPaduchikh2001.lem3_case4_pentagon_fix` Formalized done L94
  • Lemma 4 case (5) [Petersen Fix = 3]. — Re-exports `Moore57.Papers.MakhnevPaduchikh2001.lem3_case5_petersen_fix` Formalized done L107
  • Lemma 4 case (6) [Hoffman-Singleton Fix = 5]. — Re-exports `Moore57.Papers.MakhnevPaduchikh2001.lem3_case6_hs_fix` Formalized done L120
  • Lemma 4 unified: any of the 5 N(a)-shape-degree values forces `p` into the Moore57 odd-prime list `{3, 5, 7, 11, 13, 19}`. — Re-exports `Moore57.Papers.MakhnevPaduchikh2001.lem3_unified_p_in_moore57_primes`. For a Moore57 graph automorphism `σ` of odd prime order `p` fixing some vertex `a` whose σ-fixed-neighbour count `c` is one of the pap… Formalized done L138
  • Lemma 4 disjunction-of-cases — combined `Fix`-shape dispatch over the six Lemma-4 cases, yielding `|X| = p ∈ {3, 5, 7, 11, 13, 19}`. The hypothesis structure mirrors the paper's six-way classification: each branch supplies the appropriate `fixedVer… Formalized done L163
Mačaj–Širáň 2010, §2, Proposition 1 — 5/5 formalized .lean
  • Proposition 1, vertex count: — |V| = 3250` Formalized auto L31
  • Proposition 1, SRG identity in the paper's form: — A² + A − 56I = J` Formalized auto L35
  • Proposition 1, eigenvalue 57 multiplicity 1. — The 57-eigenspace projection `E_57` has trace 1 Formalized auto L70
  • Proposition 1, eigenvalue 7 multiplicity 1729. — The 7-eigenspace projection `E_7` has trace 1729 Formalized auto L78
  • Proposition 1, eigenvalue −8 multiplicity 1520. — The −8-eigenspace projection `E_-8` has trace 1520 Formalized auto L88
Mačaj–Širáň 2010, §2, Theorem 1 (Higman trace identity) — 6/6 formalized .lean
  • Theorem 1 (χ₀ component). — χ₀(σ) = trace(E_57 · P_σ) = 1` Formalized auto L40
  • Theorem 1 (χ₁ component). — For any automorphism `σ` of Γ, `χ₁(σ) = (1/15)(8 a₀(σ) + a₁(σ) − 65)` Formalized auto L47
  • Theorem 1 (χ₂ component). — χ₂(σ) = (1/15)(7 a₀(σ) − a₁(σ) + 50)` Formalized auto L54
  • Theorem 1 inverse, a₀ row. — a₀(σ) = χ₀(σ) + χ₁(σ) + χ₂(σ)`. Proof: pure trace decomposition `tr P_σ = tr((E_57+E_7+E_{−8})·P_σ)` Formalized auto L87
  • Theorem 1 inverse, a₁ row. — a₁(σ) = 57·χ₀(σ) + 7·χ₁(σ) − 8·χ₂(σ)`. Proof: from `A = 57·E_57 + 7·E_7 − 8·E_{−8}`, `tr(A·P_σ) = 57·tr(E_57·P_σ) + 7·tr(E_7·P_σ) − 8·tr(E_{−8}·P_σ)`, and `tr(A·P_σ) = a₁(σ)` by `trace_adjMatrix_mul_permMatrix_eq_adja… Formalized auto L105
  • Theorem 1 inverse, a₂ row. — a₂(σ) = 3192·χ₀(σ) − 8·χ₁(σ) + 7·χ₂(σ)`. Where `a₂(σ) := |V| − a₀(σ) − a₁(σ)` is the count of vertices at distance 2 (diameter 2 ⟹ every vertex is at distance 0, 1, or 2 from its image). Derivation: combine `a₀ = χ₀ +… Formalized auto L132
Mačaj–Širáň 2010, §2, Theorem 2 (Makhnev–Paduchikh) [external] — 5/5 formalized .lean
  • Theorem 2 part (1) (paper-faithful): `Fix(t)` is a 56-vertex star. — [done — delegates to MP 2001 main_fix_t_star] For any non-trivial involution `t ∈ Aut(Γ)`, `|Fix(t)| = 56` and the induced graph on `Fix(t)` is a star. This is the **unconditional** part of MP 2001's Theorem 2 — Part… Formalized auto L39
  • Theorem 2 part (a) `|Y| ≤ 57` (paper-faithful, conditional). — [done — delegates to MP 2001 main_decomposition_paper] 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| ≤ 57`. T… Formalized auto L57
  • Theorem 2 part (b) `|X| ≤ 55` (paper-faithful, conditional). — [done — delegates to MP 2001 main_fix_X_cases_paper] Given the paper's four-way dispatch for `Fix(X)` shape and `(|Y|, |X|)` pair (star, pentagon, Petersen, Hoffman-Singleton cases), conclude `|X| ≤ 55` Formalized auto L68
  • Theorem 2 (Makhnev–Paduchikh) abstract conclusion. — Encodes the full MP 2001 paper claim for an involution `t ∈ Aut(Γ)`: * Part (1): `Fix(t)` is a 56-vertex star. * Part (a): the decomposition `G = ⟨Y, t⟩ × X` exists with `|Y|` bounded. * Part (b): `Fix(X)` falls into… Formalized auto L87
  • Theorem 2 (Makhnev–Paduchikh): Part (1) witnesses `Conclusion`. — [done — partial] The unconditional Part (1) (`Fix(t)` is a 56-vertex star) provides the first conjunct of `Thm2MakhnevPaduchikhConclusion Γ`. Parts (a)/(b) Y/X bounds are accessible separately via `thm2_part_a_Y_card_… Formalized auto L102

§3 Equitable partitions

41 formalized · 0 pending · 0 out of scope · total 41

Mačaj–Širáň 2010, §3, Corollary 1 — 2/2 formalized .lean
  • Corollary 1 (`a₁(x) ≤ 500`). — For any automorphism `x` of a Moore57 graph, `a₁(x) ≤ 500`. Wraps `Moore57.adjacentMovedCount_le_500` (which combines the Mohar lower trace bound from Lemma 10 with the `Tr(S) ≤ 2` no-quadrangle argument) Formalized done L35
  • Corollary 1 (alternative name: `adjacentMovedCount Γ x ≤ 500`). — Re-export of `cor1_a1_le_500` under the `adjacentMovedCount`-prefixed name Formalized done L42
Mačaj–Širáň 2010, §3 — Equitable partitions (definition) — no paper-tied statements .lean
Mačaj–Širáň 2010, §3, Lemma 10 [deferred-heavy] — 2/2 formalized .lean
  • Lemma 10 (spectral trace bounds for Moore57). — For any nonempty vertex subset `S` of a Moore57 graph, `−8 + |S|/50 ≤ inducedTrace Γ S ≤ 7 + |S|/65`. Wraps `Moore57.mohar_trace_bounds` (spectral decomposition + PSD argument) Formalized done L54
  • Lemma 10 (alternative name: `inducedTrace`-prefixed). Formalized done L61
Mačaj–Širáň 2010, §3, Lemma 5 — 7/7 formalized .lean
  • Lemma 5 (1) (reciprocal counts). — sᵢ · b_{i,j} = sⱼ · b_{j,i}`. Both sides count the number of edges between cells `Sᵢ` and `Sⱼ`: `|{(v, w) ∈ Sᵢ × Sⱼ : Γ.Adj v w}|`. Combining the equitable-partition identity with `SimpleGraph.adj_comm` (symmetry of a… Formalized auto L38
  • Lemma 5 (2) (57 as eigenvalue, row-sum form). — Each row of `B` sums to 57 (assuming all cells are non-empty). This is the all-ones eigenvector statement: `B · (1,1,…,1)ᵀ = 57 · (1,1,…,1)ᵀ` Formalized auto L84
  • Lemma 5 (3) (paper-signature, proper-signature, proven bridge). — [done — Conclusion-Prop bridge] Given the Conclusion-Prop `Lemma5CharpolyConclusion P`, conclude that the characteristic polynomial of `partitionAdjMatrixℤ P` divides the canonical product `(X - 57)(X - 7)^{1729}(X +… Formalized auto L154
  • Lemma 5 (4) (paper-signature, proper-signature, proven bridge). — [done — Conclusion-Prop bridge] Given the Conclusion-Prop `Lemma5WalksConclusion P` and a parameter `k`, expose the walks claim. This is the bridge from the Conclusion-Prop to the per-`k` statement, parallel to `lem5_… Formalized auto L208
  • Lemma 5 (3) (characteristic polynomial divides). — [done — Conclusion-Prop bridge] Proper-signature form: given the Conclusion-Prop `Lemma5CharpolyConclusion P` (the spectral divisibility claim), the characteristic polynomial of the integer-lifted partition matrix `B`… Formalized auto L248
  • Lemma 5 (4) (entries of `Bᵏ` count `k`-walks). — [done — unconditional via `_holds`] Proper-signature form, unconditional via `lem5_walks_conclusion_holds`: for every `k : ℕ`, `i j : ι`, and `v ∈ P.cell i`, the `(i, j)`-entry of `Bᵏ` satisfies the Conclusion-Prop bo… Formalized auto L268
  • Lemma 5 (5) (matrix identity `B² + B − 56·I = 1·sᵀ`). — For a Moore57 equitable partition with non-empty cells, the entrywise matrix identity `(B²)_{ij} + B_{ij} = 56·δ_{ij} + sⱼ` holds. Proof: sum the pointwise Moore57 SRG identity (`lem5_pointwise_srg`) over `w ∈ Sⱼ`, fo… Formalized auto L333
Mačaj–Širáň 2010, §3, Lemma 6 — 15/15 formalized .lean
  • Lemma 6 (1) (inverse also contributes). — If `x` is an automorphism of `Γ`, `O ⊆ V` is invariant under `x` (i.e. `x · v ∈ O` for `v ∈ O`), and there exists `v ∈ O` with `Γ.Adj v (x v)`, then there also exists `w ∈ O` with `Γ.Adj w (x⁻¹ w)`. Proof: take `w :=… Formalized auto L51
  • Lemma 6 (2) (odd `|X|` ⇒ `Σ_{x ∈ X} a₁(x)` even). — Pairing argument: for `X` a subgroup of `Equiv.Perm V` with odd order, the involution `x ↦ x⁻¹` is fixed-point-free except at `x = 1` (odd-order groups have no order-2 elements: `orderOf x ∣ |X|` is odd, so `orderOf x… Formalized auto L78
  • Lemma 6 (3) (central ⇒ `Tr(O) ≤ 2`). — Paper-faithful proper signature: if `O ⊆ adjMovedSet Γ x` (geometric content of `x` being central + contributing to `O`), then `Tr(O) ≤ 2`. Re-export of `lem6_central_inducedTrace_le_two` Formalized done L90
  • Lemma 6 (3) (proper signature: central element ⇒ `Tr(O) ≤ 2`). — If `O ⊆ adjMovedSet Γ x` (every vertex of `O` is adjacency-moved by `x`), then the induced trace of `O` is at most `2`. In the paper context, this hypothesis comes from `x` being central in the group `X` and contribut… Formalized auto L111
  • Lemma 6 (4) abstract conclusion (`Tr(O)² < |O|` for all orbits). — The paper's full claim: for any orbit `O` of size `≥ 2`, the induced trace satisfies `(inducedTrace Γ O)² < |O|`. We package it as a proposition; the dispatcher handles all currently-proven cases Formalized auto L124
  • Singleton induced trace is zero. — For any simple graph `Γ` (loopless) and any vertex `v`, `inducedTrace Γ {v} = 0`. The induced subgraph on a singleton has no edges (irreflexivity of `Γ.Adj`), so the degree sum is `0` Formalized done L133
  • Lemma 6 (4) corner case: `|O| = 1`. — For a singleton `O = {v}`, `(inducedTrace Γ O)² = 0 < 1 = |O|` Formalized done L142
  • Induced trace of a pair. — For two distinct vertices `v ≠ w`, `inducedTrace Γ {v, w}` equals `1` if `v ~ w` and `0` otherwise. This is the doubleton analogue of `inducedTrace_singleton_eq_zero` Formalized done L155
  • Lemma 6 (4) corner case: `|O| = 2`. — For a pair `O = {v, w}` (v ≠ w), `(inducedTrace Γ O)² ≤ 1 < 2 = |O|` Formalized done L190
  • Lemma 6 (4) corner case: `|O| = 3`. — For three distinct vertices `{a, b, c}`, the induced subgraph in Moore57 has at most 2 edges (no triangle), so the induced degree sum is at most 4, giving `Tr(O) ≤ 4/3` and `Tr(O)² ≤ 16/9 < 3` Formalized done L206
  • Lemma 6 (4) corner case: `|O| = 4`. — For four distinct vertices `{a, b, c, d}`, the induced subgraph in Moore57 has at most 3 edges (no triangle + no 4-cycle ⟹ induced subgraph on 4 vertices is a forest, hence ≤ 3 edges), so the induced degree sum is at… Formalized done L283
  • Lemma 6 (4) (proper signature: `Tr(O)² < |O|` for `|O| ≥ 64`). — For any nonempty `O ⊆ V` of cardinality at least 64, `(inducedTrace Γ O)² < |O|`. This follows from the Mohar upper bound `Tr(O) ≤ 7 + |O|/65` (Lemma 10) plus the algebraic fact `(7 + n/65)² < n` for `n ∈ [64, 3250]`… Formalized done L405
  • Lemma 6 (4) (dispatcher: `Tr(O)² < |O|` for known cases). — Paper-faithful proper-signature dispatcher: combines the four corner cases (`|O| ∈ {1, 2, 3, 4}`) and the Mohar bound `|O| ≥ 64` into one proper-signature wrapper. Small orbits `5 ≤ |O| ≤ 63` are deferred Formalized done L416
  • Lemma 6 (4) (paper-faithful conditional). — [done — conditional] Proper-signature paper-faithful wrapper: given the orbit size constraint (`|O| ∈ {1, 2, 3, 4}` or `|O| ≥ 64`) which the dispatcher currently covers, conclude `Lemma6TraceSqLtSizeConclusion`. Small… Formalized auto L435
  • Lemma 6 (4) (`Tr(O)² < |O|`). — [done — conditional] Paper-faithful proper-signature form: delegating to the dispatcher `lem6_inducedTrace_sq_lt_card_dispatch`, which currently handles the proven cases (`|O| ∈ {1, 2, 3, 4}` or `|O| ≥ 64`). Small orb… Formalized auto L452
Mačaj–Širáň 2010, §3, Lemma 7 — 1/1 formalized .lean
  • Lemma 7 (central contribution is total on the orbit). — Let `X ≤ Aut(Γ)` be a group of automorphisms acting transitively on `O ⊆ V`, and let `x ∈ X` be central (commutes with every `g ∈ X`). If there exists `v₀ ∈ O` with `Γ.Adj v₀ (x v₀)`, then this holds for every `v ∈ O` Formalized auto L32
Mačaj–Širáň 2010, §3, Lemma 8 — 8/8 formalized .lean
  • Spectrum-trace identity. — For the X-orbit adjacency matrix of a Moore57 graph with `k` orbits, eigenvalue `57` (multiplicity `1`), `7` (multiplicity `a`), and `−8` (multiplicity `k − 1 − a`), the trace equals `65 + 15·a − 8·k`. This packages t… Formalized done L50
  • Lemma 8 (arithmetic core: `Tr + 8·(k − 10) ≡ 0 (mod 15)`). — Pure ℤ form: given the spectrum equation `Tr = 65 + 15·a − 8·k`, the quantity `Tr + 8·(k − 10) = 15·(a − 1)` is divisible by 15. No Moore57 / spectral hypothesis is needed — this is the bare arithmetic that the paper'… Formalized done L61
  • Lemma 8 (arithmetic core, `Int.ModEq` form). — Equivalent statement using the standard `a ≡ b [ZMOD n]` notation: `Tr ≡ −8 · (k − 10) (mod 15)` Formalized done L70
  • Lemma 8 (eigenvalue-swap invariance). — The paper's remark "any swap of `−8` and `7` changes the trace by 15" formalised: if `Tr_a` and `Tr_{a+1}` are the traces for multiplicity-of-7 values `a` and `a + 1` respectively (with the multiplicity of `−8` adjust… Formalized done L82
  • Lemma 8 (paper-faithful conditional form). — [done — conditional] Proper-signature form: given the spectrum equation `Tr = 65 + 15·a − 8·k` (the geometric/spectral input from the orbit-adjacency matrix), the paper's mod-15 statement `Tr ≡ −8·(k − 10) (mod 15)` h… Formalized auto L96
  • Lemma 8 abstract conclusion (`Tr(X) ≡ −8(k − 10) mod 15`). — Paper's mod-15 trace congruence packaged as a `Prop` — `Tr` is the trace of the orbit-adjacency matrix and `k` is the number of orbits Formalized auto L105
  • Lemma 8 (`Tr(X) ≡ −8(k − 10) mod 15`). — [done — conditional] Paper-faithful Moore57-conditional statement. Given the spectrum equation `Tr = 65 + 15·a − 8·k` (the geometric/spectral input from the orbit-adjacency matrix) — the deferred-heavy geometric conte… Formalized auto L118
  • Lemma 8 (paper-faithful conclusion instance). — [done — conditional] Re-states `lem8_trace_mod_fifteen_paper` using the abstract conclusion Prop `Lemma8TraceMod15Conclusion` Formalized auto L127
Mačaj–Širáň 2010, §3, Lemma 9 — 6/6 formalized .lean
  • Lemma 9 (1) (orbit trace formula). — Finite-subgroup orbit-stabilizer count form. The related transitivity/degree form is `lem9_orbit_inducedTrace_eq_neighborhood`. For `v ∈ O` an `X`-orbit, the induced-subgraph trace `Tr(O)` (the average in-orbit degree… Formalized done L48
  • Lemma 9 (1) (proper signature: `Tr(O) = deg_{Γ[O]}(v)` for any `v ∈ O`). — For a vertex subset `O ⊆ V` that is transitively acted upon by graph automorphisms (each `w ∈ O` is the image of `v` under some graph automorphism `φ_w` preserving `O`), the induced-subgraph trace `Tr(Γ[O])` equals th… Formalized auto L72
  • Lemma 9 (1) (full count form): `Tr(O) = count · |O| / |X|`. — Given: * `O` a vertex subset transitively acted upon by graph automorphisms (the geometric data; see `lem9_orbit_inducedTrace_eq_neighborhood`), * `Xfs : Finset (Equiv.Perm V)` modelling the (finite) automorphism grou… Formalized auto L97
  • Lemma 9 (1) (finite subgroup form). — For a finite subgroup `X ≤ Sym(V)` acting by graph automorphisms and `O = X · v`, the orbit trace formula needs no separate fiber-uniformity hypothesis: the uniform fiber count is supplied by orbit-stabilizer. This is… Formalized auto L123
  • Lemma 9 (2) (ℕ-form: double-counting `Σ_x a₁(x) = |{(x, v) : v ~ x v}|`). — Pure double-counting identity (no Moore57 hypothesis needed). The LHS counts pairs `(x, v)` with `v ~ x v`, where `x` ranges over a finite set `X` of permutations. By `Finset.card_filter` and `Finset.sum_product`, thi… Formalized auto L140
  • Lemma 9 (2) (ℚ-form: `|X| · Tr(X) = Σ a₁(x)`). — The rational form using `groupTrace Γ X` from `Moore57.Foundations.GraphTheory.InducedTrace` Formalized auto L154

§4 Characters

17 formalized · 0 pending · 0 out of scope · total 17

Mačaj–Širáň 2010, §4, Lemma 11 — 10/10 formalized .lean
  • Lemma 11 for `a₀` (`fixedVertexCount` constant on rational classes). — If `y = τ · σ^k · τ⁻¹` with `k` coprime to `orderOf σ`, then `fixedVertexCount y = fixedVertexCount σ`. Proof: conjugation invariance followed by coprime-power invariance. This is a *purely permutation-theoretic* resu… Formalized done L51
  • Lemma 11 for `a₁`, conjugation part (no power) — If `τ` is a graph automorphism of `Γ` and `σ` any permutation, then `adjacentMovedCount Γ (τ · σ · τ⁻¹) = adjacentMovedCount Γ σ`. Wraps `Moore57.adjacentMovedCount_conj`. This is the conjugation- invariance half of L… Formalized done L66
  • Lemma 11 for `a₁`, inverse symmetry — `a₁(σ⁻¹) = a₁(σ)` for any permutation `σ`. This is the `k = -1` (equivalently `k = orderOf σ - 1`) coprime-power instance; the only coprime-power case that does NOT require character theory. Wraps `Moore57.adjacentMov… Formalized done L79
  • Lemma 11 character conj-invariance for `χ₀`. Formalized done L93
  • Lemma 11 character conj-invariance for `χ₁`. — Requires the conjugator `τ` to be a graph automorphism of `Γ` Formalized done L100
  • Lemma 11 character conj-invariance for `χ₂`. Formalized done L107
  • Lemma 11 `a₀` conj-invariance via character chain. — `a₀(τστ⁻¹) = χ₀(τστ⁻¹) + χ₁(τστ⁻¹) + χ₂(τστ⁻¹)` (Theorem 1 row 0) `= χ₀(σ) + χ₁(σ) + χ₂(σ)` (chi conj invariance) `= a₀(σ)` Formalized done L126
  • Lemma 11 `a₁` conj-invariance via character chain. — `a₁(τστ⁻¹) = 57·χ₀ + 7·χ₁ − 8·χ₂` evaluated at `τστ⁻¹` `= 57·χ₀(σ) + 7·χ₁(σ) − 8·χ₂(σ)` (chi conj invariance) `= a₁(σ)` Formalized done L140
  • Lemma 11 `a₂` conj-invariance via character chain. — `a₂(τστ⁻¹) = |V| − a₀(τστ⁻¹) − a₁(τστ⁻¹) = |V| − a₀(σ) − a₁(σ) = a₂(σ)`. Direct consequence of `a₀` and `a₁` conj-invariance. Since the project defines `a₂` arithmetically as `|V| − a₀ − a₁`, no separate character for… Formalized done L157
  • Lemma 11 (`aᵢ` constant on rational classes — via `χⱼ` constancy). — [conditional] Assuming the (deferred) Theorem 3 (Curtis–Reiner) input `h_chi_const`, that each spectral character `χⱼ` is constant on rational classes of graph automorphisms, conclude that `a₀, a₁` are likewise consta… Formalized auto L185
Mačaj–Širáň 2010, §4, Proposition 2 [deferred-heavy] — 4/4 formalized .lean
  • Proposition 2 (character system, abstract conclusion as a `Prop`). — For any rational representation `ρ : G → GL(V)` over `ℚ`, the vector of character values `(ρ.character x₁, …, ρ.character x_u)` (indexed by a rational-class representative system) is a non-negative-integer linear comb… Formalized auto L51
  • Proposition 2 (paper-faithful conditional re-export). — [done — conditional] Proper-signature paper-faithful form: given the `Proposition2CharacterSystem ρ` hypothesis as input, for any `g : G`, the character value `ρ.character g` is expressed as a non-negative integer lin… Formalized auto L70
  • Proposition 2 (non-negative integer character system). — [done — conditional] Paper-faithful proper-signature form: given the `Proposition2CharacterSystem ρ` hypothesis as input (the deferred-heavy content of which depends on Theorem 3 + Maschke + the ℚ-irreducible decompos… Formalized auto L89
  • Lem 15 starred row `pq = 35, a₀ = 1` paper-faithful conditional. — Proper-signature paper-faithful packaging: given the abstract `Lemma15Pq35A0Eq1ForcesA1Eq206Conclusion Γ σ` instance hypothesis, expose the paper-derived equality `a₁(σ) = 206` for an order-35 graph automorphism `σ` w… Formalized done L152
Mačaj–Širáň 2010, §4, Theorem 3 (Curtis–Reiner) [external] — 3/3 formalized .lean
  • Theorem 3 (Curtis–Reiner) — abstract conclusion as a `Prop`. — For any finite group `G` and any rational representation `ρ : G →* GL(V)` over `ℚ`, the character `Representation.character ρ` is constant on rational classes of `G`. Equivalently, for any `σ : G` and any integer `k`… Formalized auto L47
  • Theorem 3 (paper-faithful conditional re-export). — [done — conditional] Proper-signature paper-faithful form: given the Curtis–Reiner-style hypothesis `Theorem3RationalClasses ρ` (rational character constant on rational classes) as input, for any `σ : G` and integer `… Formalized auto L66
  • Theorem 3 (rational characters constant on rational classes). — [done — conditional] Paper-faithful proper-signature form: given the `Theorem3RationalClasses ρ` hypothesis (the unmigrated Curtis–Reiner content), for any `σ : G` and integer `k` coprime to `orderOf σ`, conclude `ρ.c… Formalized auto L82

§5 Tables

282 formalized · 1 pending · 0 out of scope · total 283

Mačaj–Širáň 2010, §5, Lemma 12 — 48/48 formalized .lean
  • Lemma 12 (p=2 row): `a₀(x) = 56` for an involution `σ ≠ 1`. — Re-exports `Section02.Lemma2.lem2_involution_a0` Formalized done L50
  • Lemma 12 (p=2 row, a₁): `a₁(x) = 112` for an involution `σ ≠ 1`. — Re-exports `Section02.Lemma2.lem2_involution_a1` Formalized done L58
  • Lemma 12 (p=19 row): `a₀(x) = 1` for an order-19 automorphism. Formalized auto L65
  • Lemma 12 (p=11 row): `a₀(x) = 5` for an order-11 automorphism. Formalized auto L72
  • Lemma 12 (p=3 row, `a₁` part): any order-3 graph automorphism has `a₁ = 0` on Moore57. — Paper argument (§5, p=3 starred row): if `a₁(σ) > 0`, then some vertex `v` satisfies `v ~ σ v`. Applying the graph-automorphism hypothesis twice yields `σ v ~ σ² v` and `σ² v ~ σ³ v = v` (using `σ ^ 3 = 1`), so `v`, `… Formalized done L90
  • Lemma 12 abstract conclusion (17-row table for prime-order auto). — For an order-`p` graph automorphism `σ` (prime `p`), the tuple `(p, a₀(σ), a₁(σ), χ₁(σ))` lies in the paper's 17-row table. Rows marked `*` (`p = 3, a₀ = 1`; `p = 7, a₀ = 58`) cannot occur and are excluded in `lem12_n… Formalized auto L124
  • Lemma 12 (prime-order `(a₀, a₁, χ₁)` table — full statement). — [done — delegates to `_paper`] The full 17-row classification of admissible `(p, a₀, a₁, χ₁)` tuples. Substantive content in `Lemma12PrimeTableConclusion` plus the individual row lemmas above; this theorem delegates t… Formalized auto L134
  • Lemma 12 (paper-faithful `Lemma12PrimeTableConclusion` instance). — Proper-signature paper-faithful: any non-identity σ with `σ ^ p = 1` for some prime `p` satisfies the (abstract) `Lemma12PrimeTableConclusion` Prop. This packages the existence claim that "there is some prime p with σ… Formalized done L146
  • Lemma 12 (starred row `p = 3, a₀ = 1` cannot occur). — For any order-3 graph automorphism `σ` of a Moore57 graph, `a₀(σ) = 1` leads to a contradiction. Proof (mod-15 character-theoretic): 1. `aut_pow_prime_E7_trace_int` (with `p = 3`): `tr(E₇·P_σ) ∈ ℤ`. 2. `lem3_a1_mod_15… Formalized done L163
  • Lemma 12 (conditional, starred row `p = 3, a₀ = 1`): geometric step plus character constraint forces False. — Conditional paper-faithful contradiction: given an order-3 graph automorphism `σ` and the (deferred) character-theoretic lower bound `a₁(σ) ≥ 27` for the case `a₀(σ) = 1`, combine with the geometric `lem12_p3_a1_eq_ze… Formalized done L195
  • Lemma 12 (p=7 starred row): if `Fix(σ)` contains the closed neighbourhood of some vertex, then `a₁(σ) = 0`. — Geometric core of the `p = 7, a₀ = 58` starred case (and more generally, any case where the star center `c` and all of `N(c)` are fixed). The proof uses Moore57 diameter 2: * If `v ~ σv` with `v ≠ c` and `v ∉ N(c)`, t… Formalized done L224
  • Lemma 12 (p=5 row) via FixedData dispatch. — Given an order-5 graph automorphism σ and a FixedData dispatch over the three Lem 4 cases for p=5 (empty / pentagon / HS), conclude `a₀(σ) ∈ {0, 5, 50}` matching the Lem 12 p=5 row. Note: Lem 4 case 4 (pentagon p ∈ {5… Formalized done L291
  • Lemma 12 (p=13 row) via EmptyFixedData. — For order 13, Lem 4 forces case 1 (empty fix) — the only case consistent with `p = 13` is case 1 (p ∈ {5, 13}). Given the geometric `EmptyFixedData σ` (which encodes empty fix), `a₀(σ) = 0`. The deferred piece is show… Formalized done L310
  • Lemma 12 (p=3 row, a₀ = 10) via PetersenFixedData. — Non-starred Lem 12 p=3 row: a₀ = 10 (Petersen fix). Given `PetersenFixedData Γ σ`, `a₀(σ) = 10` Formalized done L320
  • Lemma 12 (p=7 row, a₀ = 2) via SingletonFixedData (lone fix vertex). — Lem 12 p=7 starred row has a₀ = 58 (closed neighbourhood fixed). The non-starred a₀ = 2 case corresponds to a "lone fix + leaf" (star with one leaf), where `|N(a) ∩ Fix(σ)| = 1`. Given `SingletonFixedData σ` (only one… Formalized done L334
  • Lemma 12 (starred row `p = 7, a₀ = 58` cannot occur). — For any order-7 graph automorphism `σ` of a Moore57 graph fixing the closed neighbourhood of some vertex `c` (so `a₀(σ) = 58 = 1 + 57`), we derive a contradiction. Proof (mod-15 character-theoretic, mirroring `lem12_n… Formalized done L356
  • Lemma 12 (conditional, starred row `p = 7, a₀ = 58`): closed neighbourhood geometric step plus character constraint forces False. — Conditional paper-faithful contradiction: given a graph automorphism `σ` fixing some vertex `c` and all of its 57 neighbours (the geometric content of `a₀(σ) = 58 = 1 + 57`), and the (deferred) character- theoretic lo… Formalized done L390
  • Lemma 12 (paper-faithful): fix-neighbour count `≡ 57 (mod p)` at any fixed vertex of a prime-order graph automorphism. — Re-exports `lem14_moore57_semiRegular_congruence_of_prime` (session 9 unconditional) in the Lem 12 namespace. For a Moore57 graph and any prime-order graph automorphism `σ` (with `σ ≠ 1` so `orderOf σ = p`) fixing a v… Formalized done L425
  • Lemma 12 (unconditional, `a₀ = 1` with prime `p ∤ 57` impossible). — **New unconditional row exclusion** combining the session-9 Lem 14 single-prime semi-regular congruence with the singleton-fix lemma `aut_fixedNeighborFinset_card_eq_zero_of_fixedVertexCount_eq_one`. For a prime-order… Formalized done L456
  • Lemma 12 (unconditional, `p = 5, a₀ = 1` impossible). — Specialization of `lem12_no_a0_one_of_prime_not_dvd_57` to `p = 5`: since `5 ∤ 57`, the row `(p = 5, a₀ = 1)` cannot occur Formalized done L492
  • Lemma 12 (unconditional, `p = 7, a₀ = 1` impossible). — Specialization to `p = 7`: since `7 ∤ 57`, the row `(p = 7, a₀ = 1)` cannot occur Formalized done L505
  • Lemma 12 (unconditional, `p = 11, a₀ = 1` impossible). — Specialization to `p = 11`: since `11 ∤ 57`, the row `(p = 11, a₀ = 1)` cannot occur. Note: the existing `lem12_p11_a0_five` proves the unique non-trivial p=11 row gives `a₀ = 5`, so `a₀ = 1` was already excluded; thi… Formalized done L520
  • Lemma 12 (unconditional, `p = 13, a₀ = 1` impossible). — Specialization to `p = 13`: since `13 ∤ 57`, the row `(p = 13, a₀ = 1)` cannot occur Formalized done L533
  • Lemma 12 (orderOf σ divides |V| - a₀(σ) for prime-order σ). — Generic divisibility constraint at any prime-order graph automorphism σ of Moore57: `orderOf σ ∣ Fintype.card V - fixedVertexCount σ`. For Moore57, `Fintype.card V = 3250`, so `orderOf σ = p ∣ 3250 - a₀(σ)`. Proof: co… Formalized done L590
  • Lemma 12 (unconditional, `a₀ = 0` with prime `p ∤ 3250` impossible). — **New unconditional row exclusion.** For a prime-order graph automorphism `σ` of Moore57 (`σ^p = 1`, `σ ≠ 1`, `p` prime) with `a₀(σ) = 0` (no fixed vertex, i.e. σ acts semi-regularly on all of V): the bridge `orderOf… Formalized done L616
  • Lemma 12 (unconditional, `a₀ = 2` with prime `p ∤ 3248` impossible). — **New unconditional row exclusion.** For a prime-order graph automorphism `σ` of Moore57 with `a₀(σ) = 2`: the bridge `orderOf σ ∣ |V| - 2 = 3248` combined with `orderOf σ = p` forces `p ∣ 3248 = 2⁴ · 7 · 29`. Thus fo… Formalized done L645
  • Lemma 12 (unconditional, `p = 3, a₀ = 0` impossible). — Specialization of `lem12_no_a0_zero_of_prime_not_dvd_3250` to `p = 3`: since `3 ∤ 3250`, the row `(p = 3, a₀ = 0)` cannot occur Formalized done L666
  • Lemma 12 (unconditional, `p = 7, a₀ = 0` impossible). — Specialization to `p = 7`: since `7 ∤ 3250`, the row cannot occur Formalized done L678
  • Lemma 12 (unconditional, `p = 11, a₀ = 0` impossible). — Specialization to `p = 11`: since `11 ∤ 3250`, the row cannot occur Formalized done L690
  • Lemma 12 (unconditional, `p = 19, a₀ = 0` impossible). — Specialization to `p = 19`: since `19 ∤ 3250`, the row `(p = 19, a₀ = 0)` cannot occur. Note: the existing `lem12_p19_a0_one` proves `a₀ = 1` is forced for `p = 19`, so this gives an independent exclusion of `a₀ = 0`… Formalized done L705
  • Lemma 12 (unconditional, `p = 3, a₀ = 2` impossible). — Specialization of `lem12_no_a0_two_of_prime_not_dvd_3248` to `p = 3`: since `3 ∤ 3248`, the row cannot occur Formalized done L718
  • Lemma 12 (unconditional, `p = 5, a₀ = 2` impossible). — Specialization to `p = 5`: since `5 ∤ 3248`, the row cannot occur Formalized done L730
  • Lemma 12 (unconditional, `p = 11, a₀ = 2` impossible). — Specialization to `p = 11`: since `11 ∤ 3248`, the row cannot occur Formalized done L742
  • Lemma 12 (unconditional, `p = 13, a₀ = 2` impossible). — Specialization to `p = 13`: since `13 ∤ 3248`, the row cannot occur Formalized done L754
  • Lemma 12 (unconditional, `p = 19, a₀ = 2` impossible). — Specialization to `p = 19`: since `19 ∤ 3248`, the row cannot occur Formalized done L766
  • Lemma 12 (unconditional, `a₀ = 3` with prime `p ∤ 3247` impossible). — **New unconditional row exclusion.** For a prime-order graph automorphism `σ` of Moore57 with `a₀(σ) = 3`: the bridge `orderOf σ ∣ |V| - 3 = 3247` combined with `orderOf σ = p` forces `p ∣ 3247 = 17 · 191`. Thus for a… Formalized done L796
  • Lemma 12 (unconditional, `a₀ = 4` with prime `p ∤ 3246` impossible). — **New unconditional row exclusion.** For a prime-order graph automorphism `σ` of Moore57 with `a₀(σ) = 4`: the bridge `orderOf σ ∣ |V| - 4 = 3246` combined with `orderOf σ = p` forces `p ∣ 3246 = 2 · 3 · 541`. Thus fo… Formalized done L820
  • Lemma 12 (unconditional, `a₀ = 5` with prime `p ∤ 3245` impossible). — **New unconditional row exclusion.** For a prime-order graph automorphism `σ` of Moore57 with `a₀(σ) = 5`: the bridge `orderOf σ ∣ |V| - 5 = 3245` combined with `orderOf σ = p` forces `p ∣ 3245 = 5 · 11 · 59`. Thus fo… Formalized done L848
  • Lemma 12 (unconditional, `p = 3, a₀ = 5` impossible). — Specialization to `p = 3`: since `3 ∤ 3245`, the row cannot occur Formalized done L866
  • Lemma 12 (unconditional, `p = 7, a₀ = 5` impossible). — Specialization to `p = 7`: since `7 ∤ 3245`, the row cannot occur Formalized done L878
  • Lemma 12 (unconditional, `p = 13, a₀ = 5` impossible). — Specialization to `p = 13`: since `13 ∤ 3245`, the row cannot occur Formalized done L890
  • Lemma 12 (unconditional, `p = 19, a₀ = 5` impossible). — Specialization to `p = 19`: since `19 ∤ 3245`, the row cannot occur Formalized done L902
  • Lemma 12 (unconditional, `p = 5, a₀ = 4` impossible). — Specialization to `p = 5`: since `5 ∤ 3246`, the row cannot occur Formalized done L914
  • Lemma 12 (unconditional, `p = 7, a₀ = 4` impossible). — Specialization to `p = 7`: since `7 ∤ 3246`, the row cannot occur Formalized done L926
  • Lemma 12 (unconditional, `p = 11, a₀ = 4` impossible). — Specialization to `p = 11`: since `11 ∤ 3246`, the row cannot occur Formalized done L938
  • Lemma 12 (unconditional, `p = 3, a₀ = 3` impossible). — Specialization of `lem12_no_a0_three_of_prime_not_dvd_3247` to `p = 3`: since `3 ∤ 3247` (as `3247 = 17 · 191`), the row cannot occur Formalized done L951
  • Lemma 12 (unconditional, `p = 5, a₀ = 3` impossible). — Specialization to `p = 5`: since `5 ∤ 3247`, the row cannot occur Formalized done L963
  • Lemma 12 (unconditional, `p = 7, a₀ = 3` impossible). — Specialization to `p = 7`: since `7 ∤ 3247`, the row cannot occur Formalized done L975
Mačaj–Širáň 2010, §5, Lemma 13 — 35/35 formalized .lean
  • Lemma 13 (subset propagation): `a₀(σ) ≤ a₀(σ^p)` for `p²`-order auto. — The "fix-set inclusion under powers" lemma applied to `σ^p`. Useful for ruling out rows where `a₀(σ) > a₀(σ^p)` Formalized done L63
  • Lemma 13 (p=5 row `(0, 0)`) trivial propagation. — If `a₀(σ^5) = 0`, then `a₀(σ) = 0` Formalized done L71
  • Lemma 13 (p=3 row `(?, 1)`) singleton propagation. — If `a₀(σ^3) = 1`, then `a₀(σ) ∈ {0, 1}` (only those two satisfy `a₀(σ) ≤ 1`). In a `3`-group context the standard modular constraint `a₀(σ) ≡ 1 (mod 3)` further restricts to `a₀(σ) = 1`, matching the paper's starred r… Formalized done L85
  • Lemma 13 (p=3 row `(1, 1)` ⟹ Lem 12 starred for `σ³`). — If `σ` has order `9` and `a₀(σ³) = 1`, then `σ³` is an order-3 graph automorphism in the Lemma 12 starred row. Combined with the geometric `lem12_p3_a1_eq_zero` (no-triangle), this gives `a₁(σ³) = 0`, which is the geo… Formalized done L115
  • Lemma 13 (p=3 starred row `(?, 1)` cannot occur). — If `σ` has order dividing 9 (so `σ^9 = 1`) and `a₀(σ³) = 1`, then we derive a contradiction via Lemma 12 starred for `σ³`. This applies `lem12_no_p3_a0_one` (itself based on B4.1 cyclotomic trace integrality + mod-15… Formalized done L135
  • Lemma 13 (p=3 row `(?, 10)` via PetersenFixedData for `σ³`). — If `σ` has order 9 and `σ³` has Petersen fix (non-starred Lem 12 p=3), then `a₀(σ³) = 10` and `a₀(σ) ≤ 10` Formalized done L149
  • Lemma 13 (p=5 row `(?, 0)` via EmptyFixedData for `σ⁵`). — If `σ⁵` has empty fix (Lem 12 p=5 empty row), then `a₀(σ) = 0` Formalized done L160
  • Lemma 13 (p=5 row `(?, 50)` via HSFixedData for `σ⁵`). — If `σ⁵` has HS fix (Lem 12 p=5 HS row), then `a₀(σ) ≤ 50` Formalized done L170
  • Lemma 13 (p=5 row `(?, 5)` via C5FixedData for `σ⁵`). — If `σ⁵` has pentagon fix (Lem 12 p=5 pentagon row), then `a₀(σ) ≤ 5` Formalized done L181
  • Lemma 13 abstract conclusion (6-row table for `p²`-order auto). — For an order-`p²` graph automorphism `σ` (`p ∈ {3, 5}`), the tuple `(p, a₀(σ), a₀(σ^p), a₁(σ), a₁(σ^p), Tr(σ))` lies in the paper's 6-row table. Two rows marked `*` (`p = 5` with `(0, 5)` and `(5, 5)`) cannot occur du… Formalized auto L196
  • Lemma 13 (`p²`-order auto: `(a₁(x), a₁(x^p), Tr(x))` table). — [done — delegates to `_paper`] The full 6-row table requires Proposition 2 (character system) and Lemma 3 (character formula). Arithmetic cores for the two starred (non-integral) rows are proven above; substantive con… Formalized auto L208
  • Lemma 13 (paper-faithful `Lemma13PrimeSquaredConclusion` instance). — Proper-signature paper-faithful: any σ with `σ^(p²) = 1` for some prime `p` satisfies the abstract `Lemma13PrimeSquaredConclusion`. Packages the existence claim that "there is some prime p with σ^(p²) = 1" as the subs… Formalized done L219
  • Lemma 13 p=5 starred rows combined — abstract Conclusion Prop. — Packages both starred-row Prop 2 inputs together: for an order-25 graph automorphism, either of the two starred rows `(a₀(σ), a₀(σ^5)) ∈ {(0,5), (5,5)}` admits the paper's character-system arithmetic input. The Lem 13… Formalized auto L359
  • Lemma 13 p=5 starred-row dispatch — paper-faithful applicator (disjunction). — For an order-25 graph automorphism σ in either p=5 starred row `(a₀(σ), a₀(σ^5)) ∈ {(0,5), (5,5)}`, derive contradiction using the B4.3-internalized trace integrality. The disjunction input `h_row` is the deferred Pro… Formalized done L370
  • Lemma 13 p=5 starred-row dispatch — paper-faithful applicator (conjunction). — Same dispatch as `lem13_p5_starred_rows_no_aut_paper` but consuming the combined Conclusion Prop `Lemma13PrimeSquaredP5StarredRowsConclusion` plus an `h_row` indicator selecting which of the two starred rows is active… Formalized done L387
  • Lemma 13 (paper-faithful): fix-neighbour count `≡ 57 (mod p)` at any fixed vertex of `σ^p` for an order-`p²` graph automorphism `σ`. — For an order-`p²` graph automorphism `σ` (with `σ^(p²) = 1` and the non-degeneracy `σ^p ≠ 1` so that `σ^p` has order exactly `p`), at any σ^p-fixed vertex `a`, ``` (autFixedNeighborFinset Γ (σ^p) a).card ≡ 57 [MOD p].… Formalized done L427
  • Lemma 13 (unconditional, `a₀(σ^p) = 1` with prime `p ∤ 57` impossible). — **New unconditional row exclusion** combining the session-9 Lem 14 single-prime semi-regular congruence (lifted to `σ^p` via `graphAut_pow`) with the singleton-fix lemma `aut_fixedNeighborFinset_card_eq_zero_of_fixedV… Formalized done L457
  • Lemma 13 (unconditional, `p = 5`, `a₀(σ⁵) = 1` impossible). — Specialization of `lem13_no_pow_p_a0_one_of_prime_not_dvd_57` to `p = 5`: since `5 ∤ 57`, any order-25 graph automorphism `σ` (with `σ^5 ≠ 1`) having `a₀(σ⁵) = 1` is impossible. Note: the Lem 13 p=5 row table covers `… Formalized done L481
  • Lemma 13 (unconditional, `a₀(σ^p) = 0` with prime `p ∤ 3250` impossible). — **New unconditional row exclusion** mirroring `lem12_no_a0_zero_of_prime_not_dvd_3250`, applied to `σ^p` (which has order `p`). For an order-`p²` graph automorphism `σ` (with `σ^(p²) = 1`, `σ^p ≠ 1`) and `a₀(σ^p) = 0`… Formalized done L510
  • Lemma 13 (unconditional, `a₀(σ^p) = 2` with prime `p ∤ 3248` impossible). — **New unconditional row exclusion** mirroring `lem12_no_a0_two_of_prime_not_dvd_3248`, applied to `σ^p` Formalized done L530
  • Lemma 13 (unconditional, `p = 3, a₀(σ³) = 0` impossible). — Specialization to `p = 3`: for any order-9 graph automorphism `σ` (with `σ³ ≠ 1`), `a₀(σ³) = 0` is impossible since `3 ∤ 3250` Formalized done L547
  • Lemma 13 (unconditional, `p = 3, a₀(σ³) = 2` impossible). — Specialization to `p = 3`: `a₀(σ³) = 2` is impossible since `3 ∤ 3248` Formalized done L561
  • Lemma 13 (unconditional, `p = 5, a₀(σ⁵) = 2` impossible). — Specialization to `p = 5`: `a₀(σ⁵) = 2` is impossible since `5 ∤ 3248`. (Note: `5 ∣ 3250`, so the `a₀(σ⁵) = 0` row is NOT excluded by this bridge for `p = 5` — it remains as a permissible row in the table.) Formalized done L577
  • Lemma 13 (unconditional, `a₀(σ^p) = 3` with prime `p ∤ 3247` impossible). — **New unconditional row exclusion** mirroring `lem12_no_a0_three_of_prime_not_dvd_3247`, applied to `σ^p` Formalized done L599
  • Lemma 13 (unconditional, `a₀(σ^p) = 4` with prime `p ∤ 3246` impossible). — **New unconditional row exclusion** mirroring `lem12_no_a0_four_of_prime_not_dvd_3246`, applied to `σ^p` Formalized done L617
  • Lemma 13 (unconditional, `a₀(σ^p) = 5` with prime `p ∤ 3245` impossible). — **New unconditional row exclusion** mirroring `lem12_no_a0_five_of_prime_not_dvd_3245`, applied to `σ^p` Formalized done L635
  • Lemma 13 (unconditional, `p = 3, a₀(σ³) = 5` impossible). — Specialization to `p = 3`: since `3 ∤ 3245`, the row cannot occur Formalized done L651
  • Lemma 13 (unconditional, `p = 3, a₀(σ³) = 4` impossible). — Specialization to `p = 3`: since `3 ∣ 3246`, this is NOT excluded by the 4-row bridge... wait, `3 ∣ 3246`, so this specialization is impossible to instantiate. We instead provide the `p = 5` specialization for a₀(σ⁵)… Formalized done L671
  • Lemma 13 (unconditional, `p = 3, a₀(σ³) = 3` impossible). — Specialization to `p = 3`: since `3 ∤ 3247`, the row cannot occur Formalized done L685
  • Lemma 13 (unconditional, `p = 5, a₀(σ⁵) = 3` impossible). — Specialization to `p = 5`: since `5 ∤ 3247`, the row cannot occur Formalized done L699
  • Lemma 13 (unconditional, no σ of order 17² = 289). — By `aut_no_order_seventeen`: σ^17 has order 17 → σ^17 = 1, contradicting σ^17 ≠ 1 Formalized done L724
  • Lemma 13 (unconditional, generic `a₀(σ^p)` row exclusion via orbit-size). — For an order-`p²` graph automorphism `σ` (with `σ^(p²) = 1`, `σ^p ≠ 1`) and any value `α` such that `p² ∤ |V| - α`, the configuration `a₀(σ^p) = α` is impossible. Proof: by `p_sq_dvd_card_V_sub_fixedVertexCount_pow_p`… Formalized auto L760
  • Lemma 13 (unconditional, `p = 5`, `a₀(σ⁵) = 5` impossible). — Specialization of `lem13_no_pow_p_a0_of_p_sq_not_dvd` to Moore57 with `p = 5` and `α = 5`. Since `|V| - α = 3250 - 5 = 3245` and `3245 mod 25 = 20 ≠ 0`, the orbit-size divisibility `25 ∣ 3245` fails. This unconditiona… Formalized done L781
  • Lemma 13 p=5 starred-row dispatch — unconditional. — For any order-25 graph automorphism σ of Moore57 with `a₀(σ⁵) = 5` (covering both starred rows `(0, 5)` and `(5, 5)`), derive contradiction unconditionally. This replaces `lem13_p5_starred_rows_no_aut_paper` (which re… Formalized done L855
  • Lemma 13 (paper-novel extension to `p = 7`): `a₀(σ⁷) = 16` for order-49 σ. — [done — bypass via orbit-size, paper-novel] For any `σ : Equiv.Perm V` that is a graph automorphism of a Moore57 graph `Γ` with `σ^49 = 1` and `σ^7 ≠ 1` (i.e. `orderOf σ = 49`), `a₀(σ⁷) = 16`. Direct re-export of `Moo… Formalized auto L898
Mačaj–Širáň 2010, §5, Lemma 14 [deferred-heavy] — 6/7 formalized, 1 pending .lean
  • Lemma 14 arithmetic: `a₁ ≡ b₁_P + b₁_Q (mod |X|)` decomposition — The paper's congruence packaging: given `a₁ ≡ b₁ (mod n)` (the semi-regular congruence) and `b₁ = b₁_P + b₁_Q` (the additive decomposition by central `x = x_P · x_Q`), the combined statement is `a₁ ≡ b₁_P + b₁_Q (mod n)` Formalized done L40
  • Lemma 14 (`a₁ ≡ b₁ mod |X|` for semi-regular `P × Q`) — abstract conclusion. — For an automorphism group `X = P × Q` of Γ where `P` acts semi-regularly on `Γ \ Fix(P)` and `Q` on `Γ \ Fix(Q)` (and `(|P|, |Q|) = 1`), and any **central** element `x ∈ X` (which factorizes uniquely as `x = x_P · x_Q… Formalized auto L66
  • Lemma 14 (proper-signature conditional form). — [done — conditional] Paper-faithful proper-signature wrapper: given the (deferred) semi-regular orbit congruence `a₁ ≡ b₁ [ZMOD n]` and the additive decomposition `b₁ = b₁_P + b₁_Q` from the `P × Q` factorization of a… Formalized auto L80
  • Lemma 14 single-prime case (paper-faithful, unconditional from graph-aut + semi-regular hypothesis). — For a graph automorphism `σ` fixing vertex `a`, if σ acts semi-regularly on the moved neighbour set `N(a) \ Fix(σ)` (`hsemi`), then ``` (autFixedNeighborFinset Γ σ a).card ≡ Γ.degree a [MOD orderOf σ]. ``` This is the… Formalized auto L104
  • Lemma 14 prime-order version (fully automatic). — For a graph automorphism `σ` of prime order `p` (`σ^p = 1`, `p` prime) fixing vertex `a`, the semi-regular hypothesis is automatic, and so ``` (autFixedNeighborFinset Γ σ a).card ≡ Γ.degree a [MOD orderOf σ]. ``` The… Formalized auto L139
  • Lemma 14 Moore57 specialisation (paper-faithful, prime-order). — For a Moore57 graph and a prime-order graph automorphism `σ` fixing a vertex `a`, the σ-fixed-neighbour count of `a` satisfies ``` (autFixedNeighborFinset Γ σ a).card ≡ 57 [MOD orderOf σ]. ``` This is the Moore57 sing… Formalized auto L159
  • Lemma 14 (`a₁ ≡ b₁ mod |X|` for semi-regular `P × Q`). — Placeholder for the paper claim. The substantive conclusion is captured in `Lemma14SemiRegularConclusion`; the arithmetic core is already `lem14_arithmetic_decomp`. Proper-signature form is `lem14_semi_regular_congrue… Pending deferred L184
Mačaj–Širáň 2010, §5, Lemma 15 [deferred-heavy] — 62/62 formalized .lean
  • Lemma 15 abstract conclusion (`(pq, a₀, a₁(x), Tr(x))` table). — For an order-`pq` automorphism `σ` with `p ≤ q` primes, the tuple `(pq, a₀(σ), a₀(σ^p), a₀(σ^q))` lies in the paper's `(pq, a₀(x), a₀(x^p), a₀(x^q))` row table, and the corresponding `(a₁(σ), a₁(σ^p), a₁(σ^q), Tr(σ))`… Formalized auto L62
  • Lemma 15 (order `pq` automorphism table). — [done — delegates to `_paper`] The full pq table; substantive content in `Lemma15PQTableConclusion` plus dedicated `lem15_no_*` sub-theorems. Delegates to `lem15_pq_table_paper` Formalized auto L75
  • Lemma 15 (order `pq` automorphism table, paper-faithful conditional). — Proper-signature paper-faithful packaging: given the `Lemma15PQTableConclusion` instance hypothesis, expose the abstract order-`pq` table conclusion in proper-signature form. The conditional input `h_concl` packages t… Formalized done L94
  • Lemma 15 (row `pq = 22`): no Moore57 carries the combined data of an order-11 automorphism σ and an involution τ generating an order-22 group (cyclic or dihedral). — Wraps `no_Order22_acts_on_Moore57` Formalized auto L101
  • Lemma 15 starred row `pq = 35` arithmetic contradiction. — For the starred row `pq = 35, a₀(x) = 1, a₀(x⁵) = 51, a₀(x⁷) = 50`, the character system forces `Tr(x) = 206`, while the orbit-trace upper bound gives `Tr(x) ≤ 186`. These are mutually inconsistent Formalized done L110
  • Lemma 15 starred row `pq = 35` brute-force via `(a₀, a₁)` + χ₁ integrality. — Stronger packaging: the paper's character-system computation actually produces `a₁(σ) = 206` for the starred `pq = 35, a₀ = 1` row. Combined with Theorem 1's χ₁ formula `χ₁(σ) = (8·a₀ + a₁ - 65) / 15 ∈ ℤ`, we get `8·1… Formalized done L130
  • Lemma 15 starred row `pq = 35` brute-force via `(a₀, a₁)` + χ₂ integrality. — Alternative path: Theorem 1's χ₂ formula `χ₂(σ) = (7·a₀ - a₁ + 50) / 15 ∈ ℤ`. With `(a₀, a₁) = (1, 206)`: `7·1 - 206 + 50 = -149 ≡ 1 (mod 15)`, i.e. `≢ 0`, contradicting integrality of `χ₂`. Sister of `lem15_starred_r… Formalized done L148
  • Lemma 15 starred row `pq = 35` brute-force via `fixedVertexCount_le_pow` + paper row data. — If the starred row `pq = 35, a₀(σ) = 1, a₀(σ⁵) = 51, a₀(σ⁷) = 50` materialises as an actual graph automorphism σ of order 35, then by `fixedVertexCount_le_pow σ n`, `a₀(σ) ≤ a₀(σ^n)` for any `n`. This is satisfied (`1… Formalized done L173
  • Lemma 15 (no order-65 automorphism) — abstract conclusion. — For any Moore57 graph Γ and any graph automorphism `σ` of order 65, no such automorphism exists. Proof depends on Lem 12 p=5 and p=13 row tables (deferred-heavy) plus composite-order trace integrality (B4.3 for order… Formalized auto L190
  • Lemma 15 (no order-65 automorphism). — [done — delegates to `_paper`] Substantive content in `Lemma15NoOrder65Conclusion`. Delegates to `lem15_no_order_65_paper` Formalized auto L197
  • Lemma 15 (no order-65 automorphism, paper-faithful conditional). — Proper-signature paper-faithful packaging: given the `Lemma15NoOrder65Conclusion` instance hypothesis, derive that no order-65 graph automorphism exists. The conditional input `h_concl` packages the deferred-heavy con… Formalized done L211
  • Lemma 15 (no `pq = 14, a₀ = 49`) — abstract conclusion. — For any Moore57 graph Γ and any graph automorphism `σ` of order 14 with `a₀(σ) = 49`, contradiction. Implemented unconditionally by `lem15_no_pq_14_a0_49_conditional` modulo the Lem 12 p=7 row table dispatch `fixedVer… Formalized auto L222
  • Lemma 15 (no `pq = 14, a₀ = 49`). — [done — delegates to `_paper`] The conditional version `lem15_no_pq_14_a0_49_conditional` below provides the substantive arithmetic dispatch given the Lem 12 p=7 row enumeration. Delegates to `lem15_no_pq_14_a0_49_paper` Formalized auto L230
  • Lemma 15 (no `pq = 14, a₀ = 49`, paper-faithful conditional). — Proper-signature paper-faithful packaging: given the `Lemma15NoPQ14A049Conclusion` instance hypothesis, derive contradiction for an order-14 graph automorphism with `a₀(σ) = 49`. The conditional input `h_concl` packag… Formalized done L244
  • Lemma 15 starred row `pq = 35` paper-faithful arithmetic. — Proper-signature paper-faithful: given the character-system input `Tr(x) = 206` and the orbit-trace upper bound `Tr(x) ≤ 186`, derive contradiction. Re-export of `lem15_starred_row_pq35_trace_above_bound` Formalized done L254
  • Lemma 15 starred row `pq = 35` cleaner discharge via χ₁ integrality and Conclusion Prop input. — [done — conditional] Given an order-35 graph automorphism σ of a Moore (57, 2)-graph Γ with `a₀(σ) = 1`, and the §4 Conclusion Prop `Lemma15Pq35A0Eq1ForcesA1Eq206Conclusion Γ σ` (which encodes the paper's character-sy… Formalized auto L299
  • Lemma 15 (`pq = 14, a₀ = 49`) conditional contradiction. — For an order-14 graph automorphism `σ` with `a₀(σ) = 49`, the fixed-set inclusion `Fix(σ) ⊆ Fix(σ²)` gives `a₀(σ) ≤ a₀(σ²)`. Combined with the Lemma 12 `p = 7` table (non-starred rows `a₀ ∈ {2, 9}`, with `a₀ = 58` exc… Formalized done L349
  • Lemma 15 (`pq = 14, a₀ = 49`, a₀(σ²) = 50 case excluded). — For an order-14 graph automorphism `σ` with `a₀(σ) = 49`, the case `a₀(σ²) = 50` is excluded by the **involution-parity argument**: σ acts on `Fix(σ²)` (50 vertices) as an involution (since σ² = 1 on `Fix(σ²)` by defi… Formalized done L374
  • Lemma 15 (`pq = 14, a₀ = 49`, a₀(σ²) = 58 case excluded). — For an order-14 graph automorphism `σ` with `a₀(σ) = 49` and `a₀(σ²) = 58`: σ² has order 7 with `|Fix(σ²)| = 58 = K_{1, 57}` star. The structural extraction `aut_order_seven_a0_58_closed_nbhd_fix` gives a centre `c` w… Formalized done L398
  • Lemma 15 (`pq = 14, a₀ = 49`, a₀(σ²) = 51 case excluded — abstract conclusion). — For an order-14 graph automorphism σ of a Moore (57, 2)-graph with `a₀(σ) = 49` and `a₀(σ²) = 51`, contradiction. The σ²-fix is the star `K_{1, 50}` (51 = 1 + 50, regular `|Fix| ∈ {2, 50}` excluded by `51 ∉ {2, 50}`).… Formalized auto L435
  • Lemma 15 (no `pq = 14, a₀ = 49`, `a₀(σ²) = 51`, paper-faithful conditional). — Proper-signature paper-faithful packaging: given the `Lemma15NoPQ14A049Pow2A051Conclusion` instance hypothesis, derive contradiction for an order-14 graph automorphism σ with `a₀(σ) = 49` and `a₀(σ²) = 51`. The condit… Formalized done L450
  • Lemma 15 (`pq = 14, a₀ = 49`, a₀(σ²) = 51) — unconditional. — [done — paper-deferred orbit-trace closure delegated to the conclusion prop pattern, with structural extraction provided unconditionally] The third of three `a₀(σ²) ∈ {50, 51, 58}` sub-cases for the `pq = 14, a₀ = 49`… Formalized auto L484
  • Lemma 15 (unconditional, `a₀(σ^q) = 0` with prime `p ∤ 3250` impossible). — **New unconditional row exclusion via reduction to Lemma 12.** For an order-`pq` graph automorphism `σ` (`σ^(p*q) = 1`, `σ^q ≠ 1`, `p`, `q` distinct primes), `σ^q` has prime order `p`. Applying `lem12_no_a0_zero_of_pr… Formalized done L527
  • Lemma 15 (unconditional, `a₀(σ^q) = 1` with prime `p ∤ 57` impossible). — **New unconditional row exclusion** combining `lem12_no_a0_one_of_prime_not_dvd_57` with the σ^q sub-power lifting. For an order-`pq` graph automorphism `σ` with `σ^q ≠ 1`, `σ^q` has prime order `p`, and `a₀(σ^q) = 1`… Formalized done L551
  • Lemma 15 (unconditional, `a₀(σ^q) = 2` with prime `p ∤ 3248` impossible). — For an order-`pq` graph automorphism `σ` (with `σ^q ≠ 1`), `σ^q` has prime order `p`. Applying `lem12_no_a0_two_of_prime_not_dvd_3248` excludes `a₀(σ^q) = 2` whenever `p ∤ 3248 = 2⁴ · 7 · 29`. For `p ∉ {2, 7, 29}` thi… Formalized done L572
  • Lemma 15 (unconditional, `a₀(σ^p) = 0` with prime `q ∤ 3250` impossible). — Mirror of `lem15_no_pow_q_a0_zero_of_prime_not_dvd_3250` for the σ^p case (which has prime order `q`). `σ^p` has order `q`; `a₀(σ^p) = 0` forces `q ∣ 3250` Formalized done L591
  • Lemma 15 (unconditional, `a₀(σ^p) = 1` with prime `q ∤ 57` impossible). — Mirror for the σ^p case Formalized done L609
  • Lemma 15 (unconditional, `a₀(σ^p) = 2` with prime `q ∤ 3248` impossible). — Mirror for the σ^p case Formalized done L626
  • Lemma 15 (unconditional, `pq = 21, a₀(σ^7) = 0` impossible). — Specialization: σ of order 21 = 3·7; σ^7 has order 3; `3 ∤ 3250` Formalized done L658
  • Lemma 15 (unconditional, `pq = 21, a₀(σ^7) = 1` impossible). — Specialization: σ^7 has order 3; `3 ∣ 57` so this is **not** excluded by this route (need other tools). Skipped (no contradiction available through this bridge) Formalized done L674
  • Lemma 15 (unconditional, `pq = 35, a₀(σ^7) = 1` impossible). — Specialization: σ of order 35 = 5·7; σ^7 has order 5; `5 ∤ 57` Formalized done L688
  • Lemma 15 (unconditional, `pq = 35, a₀(σ^7) = 2` impossible). — Specialization: σ^7 has order 5; `5 ∤ 3248` Formalized done L702
  • Lemma 15 (unconditional, `pq = 39, a₀(σ^13) = 0` impossible). — Specialization: σ of order 39 = 3·13; σ^13 has order 3; `3 ∤ 3250` Formalized done L716
  • Lemma 15 (unconditional, `pq = 77, a₀(σ^11) = 0` impossible). — Specialization: σ of order 77 = 7·11; σ^11 has order 7; `7 ∤ 3250` Formalized done L730
  • Lemma 15 (unconditional, `pq = 33, a₀(σ^11) = 0` impossible). — σ of order 33 = 3·11; σ^11 has order 3; `3 ∤ 3250` Formalized done L751
  • Lemma 15 (unconditional, `pq = 33, a₀(σ^11) = 2` impossible). — σ^11 has order 3; `3 ∤ 3248` Formalized done L765
  • Lemma 15 (unconditional, `pq = 51, a₀(σ^17) = 0` impossible). — σ of order 51 = 3·17; σ^17 has order 3; `3 ∤ 3250` Formalized done L779
  • Lemma 15 (unconditional, `pq = 51, a₀(σ^17) = 2` impossible). — σ^17 has order 3; `3 ∤ 3248` Formalized done L793
  • Lemma 15 (unconditional, `pq = 55, a₀(σ^11) = 1` impossible). — σ of order 55 = 5·11; σ^11 has order 5; `5 ∤ 57` Formalized done L807
  • Lemma 15 (unconditional, `pq = 55, a₀(σ^11) = 2` impossible). — σ^11 has order 5; `5 ∤ 3248` Formalized done L821
  • Lemma 15 (unconditional, `pq = 57, a₀(σ^19) = 0` impossible). — σ of order 57 = 3·19; σ^19 has order 3; `3 ∤ 3250` Formalized done L835
  • Lemma 15 (unconditional, `pq = 57, a₀(σ^19) = 2` impossible). — σ^19 has order 3; `3 ∤ 3248` Formalized done L849
  • Lemma 15 (unconditional, `pq = 57, a₀(σ^19) = 10` impossible). — [done — substantive math] For σ a graph automorphism of a Moore57 graph with `σ^57 = 1`, `σ^3 ≠ 1`, `σ^19 ≠ 1`, and `fixedVertexCount (σ^19) = 10` (i.e., σ^19 of order 3 with the Petersen-SRG fix shape), contradiction… Formalized auto L891
  • Lemma 15 (unconditional, `pq = 65, a₀(σ^13) = 1` impossible). — σ of order 65 = 5·13; σ^13 has order 5; `5 ∤ 57` Formalized done L996
  • Lemma 15 (unconditional, `pq = 65, a₀(σ^13) = 2` impossible). — σ^13 has order 5; `5 ∤ 3248` Formalized done L1010
  • Lemma 15 (unconditional, `pq = 85, a₀(σ^17) = 1` impossible). — σ of order 85 = 5·17; σ^17 has order 5; `5 ∤ 57` Formalized done L1024
  • Lemma 15 (unconditional, `pq = 85, a₀(σ^17) = 2` impossible). — σ^17 has order 5; `5 ∤ 3248` Formalized done L1038
  • Lemma 15 (unconditional, `pq = 91, a₀(σ^13) = 0` impossible). — σ of order 91 = 7·13; σ^13 has order 7; `7 ∤ 3250` Formalized done L1052
  • Lemma 15 (unconditional, `pq = 91, a₀(σ^13) = 1` impossible). — σ^13 has order 7; `7 ∤ 57` Formalized done L1066
  • Lemma 15 (unconditional, `pq = 95, a₀(σ^19) = 1` impossible). — σ of order 95 = 5·19; σ^19 has order 5; `5 ∤ 57` Formalized done L1080
  • Lemma 15 (unconditional, `pq = 95, a₀(σ^19) = 2` impossible). — σ^19 has order 5; `5 ∤ 3248` Formalized done L1094
  • Lemma 15 (unconditional, `pq = 119, a₀(σ^17) = 0` impossible). — σ of order 119 = 7·17; σ^17 has order 7; `7 ∤ 3250` Formalized done L1108
  • Lemma 15 (unconditional, `pq = 119, a₀(σ^17) = 1` impossible). — σ^17 has order 7; `7 ∤ 57` Formalized done L1122
  • Lemma 15 (unconditional, `pq = 143, a₀(σ^13) = 0` impossible). — σ of order 143 = 11·13; σ^13 has order 11; `11 ∤ 3250` Formalized done L1136
  • Lemma 15 (unconditional, `pq = 209, a₀(σ^19) = 0` impossible). — σ of order 209 = 11·19; σ^19 has order 11; `11 ∤ 3250` Formalized done L1150
  • Lemma 15 (unconditional, `pq = 247, a₀(σ^19) = 1` impossible). — σ of order 247 = 13·19; σ^19 has order 13; `13 ∤ 57` Formalized done L1164
  • Lemma 15 (unconditional, no order-247 element on Moore57). — [done — substantive math] For σ a graph automorphism of a Moore57 graph with `σ^247 = 1`, `σ^13 ≠ 1`, `σ^19 ≠ 1`, contradiction. This excludes the order-247 cyclic case of the `(p, q) = (13, 19)` pair coexistence — th… Formalized auto L1200
  • Lemma 15 (unconditional, no order-209 element on Moore57). — [done — substantive math] For σ a graph automorphism of a Moore57 graph with `σ^209 = 1`, `σ^11 ≠ 1`, `σ^19 ≠ 1`, contradiction. This excludes the order-209 cyclic case of the `(p, q) = (11, 19)` pair coexistence — th… Formalized auto L1273
  • Lemma 15 (unconditional, no order-143 element on Moore57). — [done — substantive math] For σ a graph automorphism of a Moore57 graph with `σ^143 = 1`, `σ^11 ≠ 1`, `σ^13 ≠ 1`, contradiction. This excludes the order-143 cyclic case of the `(p, q) = (11, 13)` pair coexistence — th… Formalized auto L1414
  • Lemma 15 (unconditional, no order-39 element on Moore57). — [done — substantive math] For σ a graph automorphism of a Moore57 graph with `σ^39 = 1`, `σ^3 ≠ 1`, `σ^13 ≠ 1`, contradiction. This excludes the order-39 cyclic case of the `(p, q) = (3, 13)` pair coexistence — the or… Formalized auto L1544
  • Lemma 15 (unconditional, no order-33 element on Moore57). — [done — substantive math] For σ a graph automorphism of a Moore57 graph with `σ^33 = 1`, `σ^3 ≠ 1`, `σ^11 ≠ 1`, contradiction. This excludes the order-33 cyclic case of the `(p, q) = (3, 11)` pair coexistence — the or… Formalized auto L1758
  • Lemma 15 (unconditional, no order-26 element on Moore57). — [done — substantive math] For σ a graph automorphism of a Moore57 graph with `σ^26 = 1`, `σ^2 ≠ 1`, `σ^13 ≠ 1`, contradiction. This excludes the order-26 cyclic case of the `(p, q) = (2, 13)` pair coexistence — the or… Formalized auto L1989
Mačaj–Širáň 2010, §5, Lemma 15 — cycleType-based row exclusions — 63/63 formalized .lean
  • Lemma 15 (unconditional, `pq = 69, a₀(σ^23) = 0` impossible). — σ of order 69 = 3·23; σ^23 has order 3; `3 ∤ 3250` Formalized done L33
  • Lemma 15 (unconditional, `pq = 69, a₀(σ^23) = 2` impossible). — σ^23 has order 3; `3 ∤ 3248` Formalized done L47
  • Lemma 15 (unconditional, `pq = 87, a₀(σ^29) = 0` impossible). — σ of order 87 = 3·29; σ^29 has order 3; `3 ∤ 3250` Formalized done L61
  • Lemma 15 (unconditional, `pq = 93, a₀(σ^31) = 0` impossible). — σ of order 93 = 3·31; σ^31 has order 3; `3 ∤ 3250` Formalized done L75
  • Lemma 15 (unconditional, `pq = 93, a₀(σ^31) = 2` impossible). — σ^31 has order 3; `3 ∤ 3248` Formalized done L89
  • Lemma 15 (unconditional, `pq = 111, a₀(σ^37) = 0` impossible). — σ of order 111 = 3·37; σ^37 has order 3; `3 ∤ 3250` Formalized done L103
  • Lemma 15 (unconditional, `pq = 115, a₀(σ^23) = 1` impossible). — σ of order 115 = 5·23; σ^23 has order 5; `5 ∤ 57` Formalized done L117
  • Lemma 15 (unconditional, `pq = 115, a₀(σ^23) = 2` impossible). — σ^23 has order 5; `5 ∤ 3248` Formalized done L131
  • Lemma 15 (unconditional, `pq = 133, a₀(σ^19) = 0` impossible). — σ of order 133 = 7·19; σ^19 has order 7; `7 ∤ 3250` Formalized done L145
  • Lemma 15 (unconditional, `pq = 133, a₀(σ^19) = 1` impossible). — σ^19 has order 7; `7 ∤ 57` Formalized done L159
  • Lemma 15 (unconditional, `pq = 187, a₀(σ^17) = 0` impossible). — σ of order 187 = 11·17; σ^17 has order 11; `11 ∤ 3250` Formalized done L173
  • Lemma 15 (unconditional, `pq = 323, a₀(σ^19) = 0` impossible). — σ of order 323 = 17·19; σ^19 has order 17; `17 ∤ 3250` Formalized done L187
  • Lemma 15 (unconditional, `pq = 323, a₀(σ^19) = 1` impossible). — σ^19 has order 17; `17 ∤ 57` Formalized done L201
  • Lemma 15 (unconditional, `pq = 39, a₀(σ^13) = 2` impossible). — σ of order 39 = 3·13; σ^13 has order 3; `3 ∤ 3248` Formalized done L223
  • Lemma 15 (unconditional, `pq = 77, a₀(σ^11) = 1` impossible). — σ of order 77 = 7·11; σ^11 has order 7; `7 ∤ 57` Formalized done L237
  • Lemma 15 (unconditional, `pq = 87, a₀(σ^29) = 2` impossible). — σ of order 87 = 3·29; σ^29 has order 3; `3 ∤ 3248` Formalized done L251
  • Lemma 15 (unconditional, `pq = 111, a₀(σ^37) = 2` impossible). — σ of order 111 = 3·37; σ^37 has order 3; `3 ∤ 3248` Formalized done L265
  • Lemma 15 (unconditional, `pq = 187, a₀(σ^17) = 1` impossible). — σ of order 187 = 11·17; σ^17 has order 11; `11 ∤ 57` Formalized done L279
  • Lemma 15 (unconditional, `pq = 187, a₀(σ^17) = 2` impossible). — σ^17 has order 11; `11 ∤ 3248` Formalized done L293
  • Lemma 15 (unconditional, `pq = 323, a₀(σ^19) = 2` impossible). — σ^19 has order 17; `17 ∤ 3248` Formalized done L307
  • Lemma 15 (unconditional, `pq = 21, a₀(σ^3) = 0` impossible). — σ of order 21 = 3·7; σ^3 has order 7; `7 ∤ 3250` Formalized done L323
  • Lemma 15 (unconditional, `pq = 21, a₀(σ^3) = 1` impossible). — σ^3 has order 7; `7 ∤ 57` Formalized done L337
  • Lemma 15 (unconditional, `pq = 35, a₀(σ^5) = 0` impossible). — σ of order 35 = 5·7; σ^5 has order 7; `7 ∤ 3250` Formalized done L351
  • Lemma 15 (unconditional, `pq = 35, a₀(σ^5) = 1` impossible). — σ^5 has order 7; `7 ∤ 57` Formalized done L365
  • Lemma 15 (unconditional, `pq = 22, a₀(σ^2) = 0` impossible). — σ of order 22 = 2·11; σ^2 has order 11; `11 ∤ 3250` Formalized done L379
  • Lemma 15 (unconditional, `pq = 22, a₀(σ^2) = 1` impossible). — σ^2 has order 11; `11 ∤ 57` Formalized done L393
  • Lemma 15 (unconditional, `pq = 22, a₀(σ^2) = 2` impossible). — σ^2 has order 11; `11 ∤ 3248` Formalized done L407
  • Lemma 15 (unconditional, `pq = 26, a₀(σ^2) = 1` impossible). — σ of order 26 = 2·13; σ^2 has order 13; `13 ∤ 57` Formalized done L421
  • Lemma 15 (unconditional, `pq = 26, a₀(σ^2) = 2` impossible). — σ^2 has order 13; `13 ∤ 3248` Formalized done L435
  • Lemma 15 (unconditional, `pq = 38, a₀(σ^2) = 0` impossible). — σ of order 38 = 2·19; σ^2 has order 19; `19 ∤ 3250` Formalized done L449
  • Lemma 15 (unconditional, `pq = 38, a₀(σ^2) = 2` impossible). — σ^2 has order 19; `19 ∤ 3248` Formalized done L463
  • Lemma 15 (unconditional, `pq = 6, a₀(σ^2) = 0` impossible). — σ of order 6 = 2·3; σ^2 has order 3; `3 ∤ 3250` Formalized done L479
  • Lemma 15 (unconditional, `pq = 6, a₀(σ^2) = 2` impossible). — σ^2 has order 3; `3 ∤ 3248` Formalized done L493
  • Lemma 15 (unconditional, `pq = 10, a₀(σ^2) = 1` impossible). — σ of order 10 = 2·5; σ^2 has order 5; `5 ∤ 57` Formalized done L507
  • Lemma 15 (unconditional, `pq = 10, a₀(σ^2) = 2` impossible). — σ^2 has order 5; `5 ∤ 3248` Formalized done L521
  • Lemma 15 (unconditional, `pq = 14, a₀(σ^2) = 0` impossible). — σ of order 14 = 2·7; σ^2 has order 7; `7 ∤ 3250` Formalized done L535
  • Lemma 15 (unconditional, `pq = 14, a₀(σ^2) = 1` impossible). — σ^2 has order 7; `7 ∤ 57` Formalized done L549
  • Lemma 15 (unconditional, `pq = 15, a₀(σ^3) = 1` impossible). — σ of order 15 = 3·5; σ^3 has order 5; `5 ∤ 57` Formalized done L563
  • Lemma 15 (unconditional, `pq = 15, a₀(σ^3) = 2` impossible). — σ^3 has order 5; `5 ∤ 3248` Formalized done L577
  • Lemma 15 (unconditional, `pq = 15, a₀(σ^5) = 0` impossible). — σ of order 15 = 3·5; σ^5 has order 3; `3 ∤ 3250` Formalized done L591
  • Lemma 15 (unconditional, `pq = 15, a₀(σ^5) = 2` impossible). — σ^5 has order 3; `3 ∤ 3248` Formalized done L605
  • Lemma 15 (unconditional, `pq = 39, a₀(σ^3) = 1` impossible). — σ of order 39 = 3·13; σ^3 has order 13; `13 ∤ 57` Formalized done L621
  • Lemma 15 (unconditional, `pq = 39, a₀(σ^3) = 2` impossible). — σ^3 has order 13; `13 ∤ 3248` Formalized done L635
  • Lemma 15 (unconditional, `pq = 57, a₀(σ^3) = 0` impossible). — σ of order 57 = 3·19; σ^3 has order 19; `19 ∤ 3250` Formalized done L649
  • Lemma 15 (unconditional, `pq = 57, a₀(σ^3) = 2` impossible). — σ^3 has order 19; `19 ∤ 3248` Formalized done L663
  • Lemma 15 (unconditional, `pq = 143, a₀(σ^11) = 1` impossible). — σ of order 143 = 11·13; σ^11 has order 13; `13 ∤ 57` Formalized done L677
  • Lemma 15 (unconditional, `pq = 143, a₀(σ^11) = 2` impossible). — σ^11 has order 13; `13 ∤ 3248` Formalized done L691
  • Lemma 15 (unconditional, `pq = 209, a₀(σ^11) = 0` impossible). — σ of order 209 = 11·19; σ^11 has order 19; `19 ∤ 3250` Formalized done L705
  • Lemma 15 (unconditional, `pq = 209, a₀(σ^11) = 2` impossible). — σ^11 has order 19; `19 ∤ 3248` Formalized done L719
  • Lemma 15 (unconditional, `pq = 247, a₀(σ^13) = 0` impossible). — σ of order 247 = 13·19; σ^13 has order 19; `19 ∤ 3250` Formalized done L733
  • Lemma 15 (unconditional, `pq = 247, a₀(σ^13) = 2` impossible). — σ^13 has order 19; `19 ∤ 3248` Formalized done L747
  • Lemma 15 (unconditional, `pq = 65, a₀(σ^13) = 5` impossible). — [done — cycleType via σ^5 EmptyFix] σ of order 65 = 5·13; σ^5 has order 13 with EmptyFix (unconditional), so σ has no fixed point; cycleType gives `13 ∣ a₀(σ^13) = 5`, but `13 ∤ 5`. Rules out the pentagon sub-case for… Formalized auto L975
  • Lemma 15 (unconditional, `pq = 65, a₀(σ^13) = 50` impossible). — [done — cycleType via σ^5 EmptyFix] σ of order 65; σ^5 EmptyFix forces σ no fixed point; cycleType gives `13 ∣ a₀(σ^13) = 50`, but `13 ∤ 50`. Rules out the Hoffman-Singleton sub-case for σ^13 of order 5 (Lem 18 case (1)) Formalized auto L994
  • Lemma 15 (unconditional, `pq = 91, a₀(σ^13) = 2` impossible). — [done — cycleType via σ^7 EmptyFix] σ^13 of order 7 with `a₀ = 2` is excluded because `13 ∤ 2` Formalized auto L1022
  • Lemma 15 (unconditional, `pq = 91, a₀(σ^13) = 9` impossible). — [done — cycleType via σ^7 EmptyFix] σ^13 of order 7 with `a₀ = 9` (= 2 + 7) is the Lem 16 star K_{1, 8} sub-case; excluded by `13 ∤ 9` Formalized auto L1040
  • Lemma 15 (unconditional, `pq = 91, a₀(σ^13) = 50` impossible). — [done — cycleType via σ^7 EmptyFix] σ^13 of order 7 with `a₀ = 50` is the Lem 16 Hoffman-Singleton sub-case (p = 7); excluded by `13 ∤ 50` Formalized auto L1058
  • Lemma 15 (unconditional, `pq = 55, a₀(σ^11) = 50` impossible). — [done — cycleType via σ^5 Pentagon fix] σ of order 55 = 5·11; σ^5 has order 11 (Pentagon fix); cycleType gives `11 ∣ a₀(σ^11) - a₀(σ)` and `a₀(σ) ≤ 5`. For `a₀(σ^11) = 50`, `50 - a₀(σ) ∈ {45, …, 50}`, none divisible b… Formalized auto L1276
  • Lemma 15 (unconditional, `pq = 95, a₀(σ^19) = 0` impossible). — [done — cycleType via σ^5 SingletonFix] σ^19 of order 5 with `a₀ = 0` is excluded because `19 ∤ 0 - 1` (= `19 ∤ -1`, treated as `19 ∤ 3250 - 1`-style natural subtraction yielding `0 - 1 = 0` in ℕ but then the divisibi… Formalized auto L1303
  • Lemma 15 (unconditional, `pq = 95, a₀(σ^19) = 5` impossible). — [done — cycleType via σ^5 SingletonFix] σ^19 of order 5 with `a₀ = 5` (Lem 18 pentagon sub-case) is excluded because `19 ∤ 5 - 1 = 4` Formalized auto L1352
  • Lemma 15 (unconditional, `pq = 95, a₀(σ^19) = 50` impossible). — [done — cycleType via σ^5 SingletonFix] σ^19 of order 5 with `a₀ = 50` (Lem 18 Hoffman-Singleton sub-case) is excluded because `19 ∤ 50 - 1 = 49` Formalized auto L1370
  • Lemma 15 (unconditional, `pq = 133, a₀(σ^19) = 2` impossible). — [done — cycleType via σ^7 SingletonFix] σ^19 of order 7 with `a₀ = 2` (Lem 16 edge K_{1,1} sub-case); excluded by `19 ∤ 1` Formalized auto L1396
  • Lemma 15 (unconditional, `pq = 133, a₀(σ^19) = 9` impossible). — [done — cycleType via σ^7 SingletonFix] σ^19 of order 7 with `a₀ = 9` (Lem 16 star K_{1, 8} sub-case); excluded by `19 ∤ 8` Formalized auto L1414
  • Lemma 15 (unconditional, `pq = 133, a₀(σ^19) = 50` impossible). — [done — cycleType via σ^7 SingletonFix] σ^19 of order 7 with `a₀ = 50` (Lem 16 Hoffman-Singleton sub-case for p=7); excluded by `19 ∤ 49` Formalized auto L1432
Mačaj–Širáň 2010, §5, Lemma 15 — involution-side + partial a₀ closures — 26/26 formalized .lean
  • Lemma 15 (unconditional, `pq = 6` with σ no fixed point impossible). — [done — cycleType, no fix shape needed on σ^2] σ of order 6 with no fixed point: σ^3 has order 2 (involution), so `a₀(σ^3) = 56` by Lem 2. σ-action on `Fix(σ^3)` is fixed-point-free, so by cycleType `3 ∣ 56`. But `3 ∤… Formalized auto L231
  • Lemma 15 (unconditional, `pq = 6` with σ^2 Singleton impossible). — [done — cycleType + helper aut_one_fix_X_dvd_pow_sub_one] σ of order 6 with σ^2 having Singleton fix `{sfd.v}`: σ permutes `{sfd.v}` so σ fixes sfd.v. Since `Fix(σ) ⊆ Fix(σ^2) = {sfd.v}`, σ has exactly one fixed point… Formalized auto L263
  • Lemma 15 (unconditional, `pq = 14` with σ exactly one fixed point impossible). — [done — cycleType + helper aut_one_fix_X_dvd_pow_sub_one] σ of order 14 = 2·7 with `Fix(σ) = {v}` (exactly one fixed point): σ^7 has order 2 (involution), `a₀(σ^7) = 56` by Lem 2. Apply the single-fix cycleType helper… Formalized auto L307
  • Lemma 15 (unconditional, `pq = 10` with σ no fixed point impossible). — [done — cycleType, p ∤ 56] σ of order 10 = 2·5 with no fixed point: σ^5 is an involution with `a₀ = 56`. Helper gives `5 ∣ 56`, but `5 ∤ 56`. Contradiction. This rules out the σ-no-fix sub-case for pq = 10 Formalized auto L335
  • Lemma 15 (unconditional, `pq = 22` with σ no fixed point impossible). — [done — cycleType, p ∤ 56] σ of order 22 with no fixed point: σ^11 involution gives a₀ = 56, and `11 ∤ 56`. Contradiction. (Parallel to the full `no_Order22_acts_on_Moore57` closure, which covers the σ-fixed-point cas… Formalized auto L362
  • Lemma 15 (unconditional, `pq = 26` with σ no fixed point impossible). — [done — cycleType, p ∤ 56] σ of order 26 with no fixed point: σ^13 involution gives a₀ = 56, but `13 ∤ 56`. Contradiction. Complements `lem15_no_order_26_unconditional` (which closes the σ-has-no-fix case via the orde… Formalized auto L389
  • Lemma 15 (unconditional, `pq = 38` with σ no fixed point impossible). — [done — cycleType, p ∤ 56] σ of order 38 with no fixed point: σ^19 involution gives a₀ = 56, but `19 ∤ 56`. Contradiction. Complements `no_C38_acts_on_Moore57_unconditional` which covers the full cyclic-38 closure via… Formalized auto L415
  • Lemma 15 (unconditional, `pq = 26` with σ exactly one fixed point impossible). — [done — cycleType + single-fix helper] σ of order 26 with exactly one fixed point: helper gives `13 ∣ 55`, but `13 ∤ 55`. Contradiction Formalized auto L438
  • Lemma 15 (unconditional, `pq = 22` forces `a₀(σ) = 1`). — For σ of order 22 with σ^2 ≠ 1, σ^11 ≠ 1: * σ^2 has order 11, PentagonFix unconditional, so `a₀(σ^2) = 5`. Hence `a₀(σ) ≤ 5`. * Positive helper: `11 ∣ 56 - a₀(σ)`. Combined with `a₀(σ) ≤ 5`: `56 - a₀(σ) ∈ {51, 52, 53,… Formalized done L470
  • Lemma 15 (unconditional, `pq = 38` with σ exactly one fixed point impossible). — [done — cycleType + single-fix helper] σ of order 38 with exactly one fixed point: helper gives `19 ∣ 55`, but `19 ∤ 55`. Contradiction Formalized auto L610
  • Lemma 15 (unconditional, no order-57 σ in the Petersen subcase). — [done — subtypePerm + coprime-order trick] For σ a graph automorphism of a Moore57 graph with `σ^57 = 1`, `σ^3 ≠ 1`, `σ^19 ≠ 1`, AND `σ^19` having Petersen fix count (`|Fix(σ^19)| = 10`), contradiction. **Proof sketch… Formalized auto L654
  • Lemma 15 (order-57 dichotomy wrapper). — [done — Petersen branch closed] For σ of order 57 on a Moore57 graph, the Lem 17 dichotomy on `σ^19` (order 3) gives either SingletonFix or PetersenSRG fix. The PetersenSRG branch is closed unconditionally via `lem15_… Formalized auto L773
  • Lemma 15 (unconditional, `pq = 57`, a₀(σ) = 1 forced). — For σ of order 57 = 3·19 with σ^3 ≠ 1 (so σ^3 has order 19): * σ^3 has order 19, SingletonFix unconditional (Lem 19 case 2). * By the general helper `lem15_a0_eq_one_of_pow_singleton_fix_and_prime` with `X = 3`, `a₀(σ… Formalized done L889
  • Lemma 15 (unconditional, `pq = 95`, a₀(σ) = 1 forced). — For σ of order 95 = 5·19 with σ^5 ≠ 1 (so σ^5 has order 19): σ^5 has SingletonFix (Lem 19 case 2); general helper at `X = 5` gives `a₀(σ) = 1` Formalized done L908
  • Lemma 15 (unconditional, `pq = 133`, a₀(σ) = 1 forced). — For σ of order 133 = 7·19 with σ^7 ≠ 1 (so σ^7 has order 19): σ^7 has SingletonFix (Lem 19 case 2); general helper at `X = 7` gives `a₀(σ) = 1` Formalized done L927
  • Lemma 15 (unconditional, `pq = 77`, a₀(σ) = 5 forced). — For σ of order 77 = 7·11 with σ^7 ≠ 1 (so σ^7 has order 11): σ^7 has PentagonFix (Lem 19 case 3); general helper at `X = 7` (prime > 5) gives `a₀(σ) = 5` Formalized done L946
  • Lemma 15 (unconditional, `pq = 57` ⟹ σ^19 has SingletonFix). — For σ of order 57 with `σ^3 ≠ 1` and `σ^19 ≠ 1`, the Lem 17 dichotomy on `σ^19` (order 3) gives either SingletonFix or Petersen-SRG fix. The Petersen branch is **unconditionally excluded** by `lem15_no_order_57_pow19_… Formalized done L974
  • Lemma 15 (unconditional, `pq = 77` σ^11 a₀ mod 77 = 16). — For σ of order 77 = 7·11 with `σ^7 ≠ 1` and `σ^11 ≠ 1`: * `a₀(σ) = 5` (from `lem15_pq77_a0_eq_five_unconditional`, via σ^7 PentagonFix unconditional). * cycleType prime 11: `11 ∣ a₀(σ^11) - 5`. * Lem 12 / Moore57 mod-… Formalized done L1009
  • Lemma 15 (unconditional, `pq = 95` σ^19 a₀ mod 95 = 20). — For σ of order 95 = 5·19 with `σ^5 ≠ 1` and `σ^19 ≠ 1`: * `a₀(σ) = 1` (from `lem15_pq95_a0_eq_one_unconditional`). * cycleType prime 19: `19 ∣ a₀(σ^19) - 1`. * Lem 12 / Moore57 mod-5: `a₀(σ^19) ≡ 0 [MOD 5]` (3250 = 5·… Formalized done L1063
  • Lemma 15 (unconditional, `pq = 133` σ^19 a₀ mod 133 = 58). — For σ of order 133 = 7·19 with `σ^7 ≠ 1` and `σ^19 ≠ 1`: * `a₀(σ) = 1` (from `lem15_pq133_a0_eq_one_unconditional`). * cycleType prime 19: `19 ∣ a₀(σ^19) - 1`. * Lem 12 / Moore57 mod-7: `a₀(σ^19) ≡ 2 [MOD 7]` (3250 ≡… Formalized done L1116
  • Lemma 15 (general): `Fix(σ^X) = ∅ ⇒ a₀(σ) = 0`. — For σ : Equiv.Perm V with `σ^X` having empty fix (`Moore57.EmptyFixedData (σ^X)`), `Fix(σ) ⊆ Fix(σ^X) = ∅`, so `fixedVertexCount σ = 0`. No primality on X needed. Used by `lem15_pq91_a0_eq_zero_unconditional` (pq = 91… Formalized done L1164
  • Lemma 15 (unconditional, `pq = 65`, a₀(σ) = 0 forced). — For σ of order 65 = 5·13 with σ^5 ≠ 1 (so σ^5 has order 13): σ^5 has EmptyFix unconditionally (`aut_order_thirteen_EmptyFixedData_unconditional`, Lem 19 case 1). The generic helper `lem15_a0_eq_zero_of_pow_emptyFix` g… Formalized done L1183
  • Lemma 15 (unconditional, `pq = 91`, a₀(σ) = 0 forced). — For σ of order 91 = 7·13 with σ^7 ≠ 1 (so σ^7 has order 13): σ^7 has EmptyFix unconditionally (`aut_order_thirteen_EmptyFixedData_unconditional`, Lem 19 case 1). The generic helper `lem15_a0_eq_zero_of_pow_emptyFix` g… Formalized done L1207
  • Lemma 15 (unconditional, `pq = 91` σ^13 a₀ mod 91 = 65). — For σ of order 91 = 7·13 with `σ^7 ≠ 1` and `σ^13 ≠ 1`: * `a₀(σ) = 0` (from `lem15_pq91_a0_eq_zero_unconditional`, via σ^7 EmptyFix). * cycleType prime 13: `13 ∣ a₀(σ^13) - 0 = a₀(σ^13)`. * Lem 12 / Moore57 mod-7: `a₀… Formalized done L1238
  • Lemma 15 (pq=91) full unconditional non-existence. — For σ a graph automorphism of a Moore57 Γ with `σ^91 = 1, σ^7 ≠ 1, σ^13 ≠ 1` (i.e., σ of order exactly 91 = 7·13), contradiction. The proof combines: * `lem15_pq91_pow13_a0_modEq_65_unconditional`: gives `a₀(σ^13) ≡ 6… Formalized done L1314
  • Lemma 15 (pq=133) full unconditional non-existence. — For σ a graph automorphism of a Moore57 Γ with `σ^133 = 1, σ^7 ≠ 1, σ^19 ≠ 1` (i.e., σ of order exactly 133 = 7·19), contradiction. Proof: 1. `a₀(σ^19) ≡ 58 [MOD 133]` from `lem15_pq133_pow19_a0_modEq_58_unconditional… Formalized done L1379
Mačaj–Širáň 2010, §5, Lemma 15 — full unconditional + per-prime closures — 42/42 formalized .lean
  • Lemma 15 (pq=77) full unconditional non-existence. — For σ a graph automorphism of a Moore57 Γ with `σ^77 = 1, σ^7 ≠ 1, σ^11 ≠ 1` (i.e., σ of order exactly 77 = 7·11), contradiction by Pentagon-in-K_{1, 15} structural mismatch. Proof outline (see section docstring for f… Formalized done L68
  • Lemma 15 (unconditional, `pq = 57` Singleton-Singleton structural characterization). — For any surviving σ of order 57 (`σ^57 = 1, σ^3 ≠ 1, σ^19 ≠ 1`): * `a₀(σ) = 1` (unique fixed vertex; from `lem15_pq57_a0_eq_one_unconditional` via cycleType + σ^3 SingletonFix). * `σ^19` has SingletonFix (Petersen bra… Formalized done L228
  • Lemma 15 (pq=95) Lem 18 trichotomy specialised to σ^19. — For σ of order 95 (i.e., σ^95 = 1, σ^5 ≠ 1, σ^19 ≠ 1) acting as a graph automorphism of a Moore57 Γ, σ^19 has order 5, so by Lem 18 (prime case), `fixedVertexCount (σ^19) ∈ {0, 5, 50}` Formalized done L251
  • Lemma 15 (pq=95) full unconditional non-existence. — For σ a graph automorphism of a Moore57 Γ with `σ^95 = 1, σ^5 ≠ 1, σ^19 ≠ 1` (i.e., σ of order exactly 95 = 5·19), contradiction. The proof combines: * `lem15_pq95_pow19_fixedCount_dispatch_unconditional` (Lem 18 disp… Formalized done L280
  • Lemma 15 (pq=65) Lem 18 trichotomy specialised to σ^13. — For σ of order 65 (i.e., σ^65 = 1, σ^13 ≠ 1) acting as a graph automorphism of a Moore57 Γ, σ^13 has order 5, so by Lem 18 (prime case), `fixedVertexCount (σ^13) ∈ {0, 5, 50}` Formalized done L307
  • Lemma 15 (pq=65) partial reduction: σ^13 must have empty fix. — [done — partial unconditional] For σ a graph automorphism of a Moore57 Γ with `σ^65 = 1, σ^5 ≠ 1, σ^13 ≠ 1` (i.e., σ of order exactly 65 = 5·13), the Lem 18 dispatch on σ^13 combined with the existing `a₀(σ^13) ∈ {5,… Formalized auto L332
  • Lemma 15 (pq=55) Lem 18 trichotomy specialised to σ^11. — For σ of order 55 (i.e., σ^55 = 1, σ^11 ≠ 1) acting as a graph automorphism of a Moore57 Γ, σ^11 has order 5, so by Lem 18 (prime case), `fixedVertexCount (σ^11) ∈ {0, 5, 50}` Formalized done L364
  • Lemma 15 (pq=55) partial reduction: σ^11 has Empty or Pentagon fix. — [done — partial unconditional] For σ a graph automorphism of a Moore57 Γ with `σ^55 = 1, σ^5 ≠ 1, σ^11 ≠ 1` (i.e., σ of order exactly 55 = 5·11), the Lem 18 dispatch on σ^11 combined with `lem15_no_pq55_pow11_a0_fifty… Formalized auto L395
  • Lemma 15 (pq=21) Lem 17 trichotomy specialised to σ^7. — For σ of order 21 (i.e., σ^21 = 1, σ^7 ≠ 1) acting as a graph automorphism of a Moore57 Γ, σ^7 has order 3, so by Lem 17 (prime case, Order-3 trichotomy), `fixedVertexCount (σ^7) ∈ {1, 10}` (Singleton or Petersen-SRG… Formalized done L430
  • Lemma 15 (pq=21) partial reduction: σ^7 has Singleton or Petersen fix. — [done — partial unconditional] For σ a graph automorphism of a Moore57 Γ with `σ^21 = 1, σ^3 ≠ 1, σ^7 ≠ 1` (i.e., σ of order exactly 21 = 3·7), the Lem 17 dispatch on σ^7 forces **`fixedVertexCount (σ^7) ∈ {1, 10}`**.… Formalized auto L455
  • Lemma 15 (pq=35) Lem 18 trichotomy specialised to σ^7. — For σ of order 35 (i.e., σ^35 = 1, σ^7 ≠ 1) acting as a graph automorphism of a Moore57 Γ, σ^7 has order 5, so by Lem 18 (prime case, Order-5 trichotomy), `fixedVertexCount (σ^7) ∈ {0, 5, 50}` (Empty / Pentagon / Hoff… Formalized done L487
  • Lemma 15 (pq=35) partial reduction: σ^7 has Empty/Pentagon/HS fix. — [done — partial unconditional] For σ a graph automorphism of a Moore57 Γ with `σ^35 = 1, σ^5 ≠ 1, σ^7 ≠ 1` (i.e., σ of order exactly 35 = 5·7), the Lem 18 dispatch on σ^7 forces **`fixedVertexCount (σ^7) ∈ {0, 5, 50}`… Formalized auto L515
  • Lemma 15 (pq=187) full unconditional non-existence. — For σ of order 187 = 11·17, `σ^11` has order 17. Since Moore57 has no order-17 automorphism (`aut_no_order_seventeen`), `σ^11 = 1`, contradicting the order-187 hypothesis `σ^11 ≠ 1`. Conceptually closes paper §9 Lem 2… Formalized done L547
  • Lemma 15 (pq=221) full unconditional non-existence. — For σ of order 221 = 13·17, `σ^13` has order 17. Direct application of `aut_no_order_seventeen` to `σ^13` Formalized done L565
  • Lemma 15 (pq=323) full unconditional non-existence. — For σ of order 323 = 17·19, `σ^19` has order 17. Direct application of `aut_no_order_seventeen` to `σ^19` Formalized done L581
  • Lemma 15 (pq=51) full unconditional non-existence. — For σ of order 51 = 3·17, `σ^3` has order 17. Direct application of `aut_no_order_seventeen` to `σ^3` Formalized done L597
  • Lemma 15 (pq=85) full unconditional non-existence. — For σ of order 85 = 5·17, `σ^5` has order 17 Formalized done L611
  • Lemma 15 (pq=119) full unconditional non-existence. — For σ of order 119 = 7·17, `σ^7` has order 17. Direct application of `aut_no_order_seventeen` to `σ^7` Formalized done L626
  • Lemma 15 (pq=115) full unconditional non-existence. — For σ of order 115 = 5·23, `σ^5` has order 23. Direct application of `aut_no_order_twentyThree` Formalized done L660
  • Lemma 15 (pq=161) full unconditional non-existence. — For σ of order 161 = 7·23, `σ^7` has order 23 Formalized done L675
  • Lemma 15 (pq=253) full unconditional non-existence. — For σ of order 253 = 11·23, `σ^11` has order 23 Formalized done L690
  • Lemma 15 (pq=299) full unconditional non-existence. — For σ of order 299 = 13·23, `σ^13` has order 23 Formalized done L705
  • Lemma 15 (pq=87) full unconditional non-existence. Formalized done L724
  • Lemma 15 (pq=145) full unconditional non-existence. Formalized done L736
  • Lemma 15 (pq=203) full unconditional non-existence. Formalized done L748
  • Lemma 15 (pq=319) full unconditional non-existence. Formalized done L760
  • Lemma 15 (pq=93) full unconditional non-existence. Formalized done L774
  • Lemma 15 (pq=155) full unconditional non-existence. Formalized done L786
  • Lemma 15 (pq=217) full unconditional non-existence. Formalized done L798
  • Lemma 15 (pq=341) full unconditional non-existence. Formalized done L810
  • Lemma 15 (pq=111) full unconditional non-existence. Formalized done L824
  • Lemma 15 (pq=185) full unconditional non-existence. Formalized done L836
  • Lemma 15 (pq=259) full unconditional non-existence. Formalized done L848
  • Lemma 15 (pq=123) full unconditional non-existence. Formalized done L862
  • Lemma 15 (pq=205) full unconditional non-existence. Formalized done L874
  • Lemma 15 (pq=287) full unconditional non-existence. Formalized done L886
  • Lemma 15 (pq=129) full unconditional non-existence. Formalized done L898
  • Lemma 15 (pq=215) full unconditional non-existence. Formalized done L910
  • Lemma 15 (pq=301) full unconditional non-existence. Formalized done L922
  • Lemma 15 (pq=141) full unconditional non-existence. Formalized done L934
  • Lemma 15 (pq=235) full unconditional non-existence. Formalized done L946
  • Lemma 15 (pq=329) full unconditional non-existence. Formalized done L958
Mačaj–Širáň 2010, §5, Lemma 15 [deferred-heavy] — no paper-tied statements .lean

§6 p-groups (overview)

218 formalized · 0 pending · 0 out of scope · total 218

Mačaj–Širáň 2010, §6, Lemma 16 [deferred-heavy] — 65/65 formalized .lean
  • Lemma 16 modular brace (vertex set + N(a) for prime `p`). — For a single graph-automorphism `σ` with `σ^(p^k) = 1` (a cyclic `p`-group element) and any `σ`-fixed vertex `a`, the global and neighbourhood fixed-vertex counts satisfy the standard mod-`p` constraints: ``` fixedVer… Formalized done L62
  • Lemma 16 case (1) [p = 13]: `Fix(σ)` must be empty. — Combining the mod-13 constraint `fixedVertexCount σ ≡ 0 (mod 13)` with the standard Fix-size candidates (≤ 58: ∅, singleton, edge, pentagon, Petersen, HS, stars), only `Fix(σ) = ∅` satisfies the congruence (all other… Formalized done L84
  • Lemma 16 case (1) [p = 5]: small `Fix(σ)` ⇒ empty. — For `σ^(5^k) = 1`, count ≡ 0 (mod 5). If count ≤ 4 then count = 0. Used to rule out non-empty Fix sizes below the pentagon Formalized done L102
  • Lemma 16 case (2) [p = 3]: small `Fix(σ)` ⇒ singleton. — For `σ^(3^k) = 1`, count ≡ 1 (mod 3) (since 3250 = 3·1083 + 1). If count ≤ 3 then count = 1. Mod-3 narrowing of the §6 Lem 16 case (2) which says `Fix(σ)` is a singleton for `p ∈ {3, 19}` Formalized done L117
  • Lemma 16 case (2) [p = 19]: small `Fix(σ)` ⇒ singleton. — For `σ^(19^k) = 1`, count ≡ 1 (mod 19) (since 3250 = 19·171 + 1). If count ≤ 19 then count = 1. Mod-19 narrowing of the §6 Lem 16 case (2) which says `Fix(σ)` is a singleton for `p ∈ {3, 19}` Formalized done L132
  • Lemma 16 case (3) [p = 7]: small `Fix(σ)` ⇒ edge (`|Fix| = 2`). — For `σ^(7^k) = 1`, count ≡ 2 (mod 7) (since 3250 = 7·464 + 2). If count ≤ 8 then count = 2. Mod-7 narrowing of the §6 Lem 16 case (3) which says `Fix(σ)` is a star `K_{1, 1+7l}` with `|Fix| = 2 + 7l` for `p = 7` Formalized done L148
  • Lemma 16 case (4) [p = 5]: non-empty small `Fix(σ)` ⇒ pentagon (`|Fix| = 5`). — For `σ^(5^k) = 1`, count ≡ 0 (mod 5). If `1 ≤ count ≤ 9` then `count = 5`. Mod-5 narrowing of the §6 Lem 16 case (4) which says `Fix(σ)` is a pentagon for `p ∈ {5, 11}` (size 5) Formalized done L164
  • Lemma 16 case (4) [p = 11]: small `Fix(σ)` ⇒ pentagon (`|Fix| = 5`). — For `σ^(11^k) = 1`, count ≡ 5 (mod 11) (since 3250 = 11·295 + 5). If count ≤ 15 then count = 5. Mod-11 narrowing of the §6 Lem 16 case (4) which says `Fix(σ)` is a pentagon for `p ∈ {5, 11}` Formalized done L181
  • Lemma 16 prime from singleton-Fix N(a) = 0. — For σ a p-group element (`σ^(p^k) = 1`) fixing a vertex `a` with no fixed neighbours (the singleton-Fix case), `p ∈ {3, 19}` Formalized done L212
  • Lemma 16 prime from star-leaf N(a) = 1. — For σ a p-group element fixing a star-leaf vertex (one fixed neighbour), `p = 7` Formalized done L244
  • Lemma 16 prime from pentagon N(a) = 2. — For σ a p-group element fixing a pentagon-vertex, `p ∈ {5, 11}` Formalized done L265
  • Lemma 16 prime from Petersen N(a) = 3. — For σ a p-group element fixing a Petersen-vertex, `p = 3` Formalized done L286
  • Lemma 16 prime from HS N(a) = 7. — For σ a p-group element fixing a HS-vertex, `p = 5` Formalized done L307
  • Lemma 16 (paper-faithful conditional fix-shape dispatch). — Proper-signature paper-faithful packaging: for σ a `p^k`-element with odd prime `p > 2` fixing a vertex `a`, the σ-fixed-neighbour count `c = |N(a) ∩ Fix(σ)|` constrains `p` to the Moore57 odd-prime list `{3, 5, 7, 11… Formalized done L346
  • Lemma 16 (odd-prime `p`-group fix shape, proper-signature paper-faithful form). — [done — paper-signature upgrade] Proper-signature replacement for the prior backward-compat True-stub. For an odd prime `p > 2` with `σ^(p^k) = 1` fixing vertex `a`, the σ-fixed-neighbour count `c = |N(a) ∩ Fix(σ)|` c… Formalized auto L375
  • Lemma 16 case (1) [p = 13] abstract conclusion — (Conclusion Prop) Formalized auto L411
  • Lemma 16 case (1) [p = 5] abstract conclusion — (Conclusion Prop) Formalized auto L415
  • Lemma 16 case (2) [p = 3] abstract conclusion — (Conclusion Prop) Formalized auto L419
  • Lemma 16 case (2) [p = 19] abstract conclusion — (Conclusion Prop) Formalized auto L423
  • Lemma 16 case (3) [p = 7] abstract conclusion — (Conclusion Prop) Formalized auto L427
  • Lemma 16 case (4) [p = 5] abstract conclusion — (Conclusion Prop) Formalized auto L431
  • Lemma 16 case (4) [p = 11] abstract conclusion — (Conclusion Prop) Formalized auto L435
  • Lemma 16 case (1) [p = 13] via Conclusion encoding (paper-faithful). Formalized auto L441
  • Lemma 16 case (1) [p = 5] via Conclusion encoding (paper-faithful). Formalized auto L448
  • Lemma 16 case (2) [p = 3] via Conclusion encoding (paper-faithful). Formalized auto L455
  • Lemma 16 case (2) [p = 19] via Conclusion encoding (paper-faithful). Formalized auto L462
  • Lemma 16 case (3) [p = 7] via Conclusion encoding (paper-faithful). Formalized auto L469
  • Lemma 16 case (4) [p = 5] via Conclusion encoding (paper-faithful). Formalized auto L476
  • Lemma 16 case (4) [p = 11] via Conclusion encoding (paper-faithful). Formalized auto L483
  • Lemma 16 case (1) [p = 13] Conclusion instance (small-Fix bound). Formalized auto L498
  • Lemma 16 case (1) [p = 5] Conclusion instance (small-Fix bound). Formalized auto L506
  • Lemma 16 case (2) [p = 3] Conclusion instance (small-Fix bound). Formalized auto L514
  • Lemma 16 case (2) [p = 19] Conclusion instance (small-Fix bound). Formalized auto L522
  • Lemma 16 case (3) [p = 7] Conclusion instance (small-Fix bound). Formalized auto L530
  • Lemma 16 case (4) [p = 5] Conclusion instance (small-Fix + non-empty). Formalized auto L538
  • Lemma 16 case (4) [p = 11] Conclusion instance (small-Fix bound). Formalized auto L547
  • Lemma 16 N(a) = 0 (singleton-Fix) abstract conclusion. Formalized auto L563
  • Lemma 16 N(a) = 1 (star-leaf) abstract conclusion. Formalized auto L567
  • Lemma 16 N(a) = 2 (pentagon-vertex) abstract conclusion. Formalized auto L571
  • Lemma 16 N(a) = 3 (Petersen-vertex) abstract conclusion. Formalized auto L575
  • Lemma 16 N(a) = 7 (HS-vertex) abstract conclusion. Formalized auto L579
  • Lemma 16 N(a) = 0 via Conclusion encoding (paper-faithful). Formalized auto L583
  • Lemma 16 N(a) = 1 via Conclusion encoding (paper-faithful). Formalized auto L589
  • Lemma 16 N(a) = 2 via Conclusion encoding (paper-faithful). Formalized auto L595
  • Lemma 16 N(a) = 3 via Conclusion encoding (paper-faithful). Formalized auto L601
  • Lemma 16 N(a) = 7 via Conclusion encoding (paper-faithful). Formalized auto L607
  • Lemma 16 N(a) = 0 Conclusion instance (unconditional from N count). Formalized auto L613
  • Lemma 16 N(a) = 1 Conclusion instance (unconditional from N count). Formalized auto L624
  • Lemma 16 N(a) = 2 Conclusion instance (unconditional from N count). Formalized auto L635
  • Lemma 16 N(a) = 3 Conclusion instance (unconditional from N count). Formalized auto L646
  • Lemma 16 N(a) = 7 Conclusion instance (unconditional from N count). Formalized auto L657
  • Lemma 16 (paper-faithful Conclusion-Prop dispatch). — Conclusion-Prop counterpart of `lem16_pgroup_fix_shape_paper`: for σ a `p^k`-element with odd prime `p > 2` fixing a vertex `a`, the σ-fixed-neighbour count `c = |N(a) ∩ Fix(σ)|` dispatches into the per-count Conclusi… Formalized done L680
  • Lemma 16 case (3) [p = 7] prime-case Conclusion with explicit `fixedVertexCount σ = 2`. — [done — partial unconditional, prime case] Given the paper case-(3) fix-edge fact `fixedVertexCount σ = 2` (asserted by Lem 16 case (3) for `p = 7` — derivable once the future 7-group SRG ladder is built), discharge `… Formalized auto L761
  • Lemma 16 case (3) [p = 7] prime-case Conclusion via small-Fix bound. — [done — partial unconditional, prime case] Prime specialisation of `lem16_case3_7group_conclusion_if_small`: given `σ^7 = 1` (the prime case) and `fixedVertexCount σ ≤ 8`, the mod-7 constraint `fixedVertexCount σ ≡ 2… Formalized auto L781
  • Lemma 16 case (3) [p = 7] prime-case Conclusion via existing `_if_small` wiring. — [done — partial unconditional, prime case] Combinator form: explicitly threads through the existing `lem16_case3_7group_fix_edge_if_small` theorem (rather than the Conclusion-instance version). Useful for callers that… Formalized auto L797
  • Lemma 16 case (3) [p = 7] prime-case Conclusion-only paper-faithful dispatch. — [done — partial unconditional, prime case] Conjunction of the two prime-case Conclusion entry points (`_with_fix_count_two` and `_via_small_fix`), exposing the paper's case (3) `p = 7` edge-fix Conclusion as a Prop-le… Formalized auto L817
  • Lemma 16 case (3) [p = 7] Conclusion totalised over `σ = 1`. — For `σ^7 = 1` with `fixedVertexCount σ ≤ 8`, the Conclusion holds *unconditionally on `σ ≠ 1`*: if `σ = 1`, then `fixedVertexCount σ = 3250 > 8`, contradicting `h_small`; so we are forced into the non-trivial branch w… Formalized done L852
  • Lemma 16 case (3) [p = 7] Conclusion totalised over `σ = 1` (fix-count form). — Variant of `_via_small_fix_total` that takes the explicit `fixedVertexCount σ = 2` instead of a small bound. In the `σ = 1` branch, `fixedVertexCount σ = 3250 ≠ 2`, so the hypothesis cannot hold; otherwise the non-tri… Formalized done L866
  • Lemma 16 case (3) [p = 7] paper Conclusion via `EdgeFixedData`. — [done — partial unconditional, prime case, EdgeFixedData-routed] Wire of `aut_order_seven_EdgeFixedData_of_small_fix` to the paper Conclusion. Given `σ^7 = 1`, `smul_adj`, and `|Fix(σ)| ≤ 8`, build the `EdgeFixedData… Formalized auto L908
  • Lemma 16 case (3) [p = 7] paper Conclusion via `EdgeFixedData` — total form. — [done — partial unconditional, prime case, EdgeFixedData-routed] Total wrapper of `lem16_case3_7group_edgeFixedData_paper_prime`: same hypotheses + Conclusion, packaged under the same shape as the `_via_small_fix_tota… Formalized auto L948
  • Lemma 16 fix-shape dispatch Prop encoding (full case (3) star K_{1, 1+7l}). — [done — Prop encoding, full `l ≥ 0`] For σ a 7-group element acting as a graph automorphism of a Moore57 Γ with σ^7 = 1, the §6 Lem 16 case (3) classification asserts that `Fix(σ)` is a star `K_{1, 1+7l}` with `|Fix(σ… Formalized auto L1002
  • Lemma 16 full dispatch paper bound `orderOf σ ∣ 343` (combined upper, p=7). — [done — full wire, conditional on `Lemma16P7FixShapeDispatch`] The paper's §6 Lem 16 case (3) for `p = 7` states `|X| ∣ 7^k` for a 7-group `X` with a star fix shape. Specialised to the prime case `σ^7 = 1`, `orderOf σ… Formalized auto L1023
  • Lemma 16 full dispatch Conclusion Prop encoding (p=7). — Encapsulates the combined paper-bound `orderOf σ ∣ 343` from the full p=7 dispatch as a `Prop`, paralleling `Lemma18FullDispatchConclusion` and the per-case `Lemma16Case3_7Group_EdgeFix_Conclusion`. Used by downstream… Formalized auto L1039
  • Lemma 16 full dispatch via Conclusion encoding (p=7). — Given the `Lemma16P7FullDispatchConclusion σ` Prop, conclude `orderOf σ ∣ 343`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern Formalized done L1047
  • Lemma 16 full dispatch Conclusion instance, given fix-shape dispatch (p=7). — [done — full wire, conditional on `Lemma16P7FixShapeDispatch`] Conclusion-Prop wrapper around `lem16_7group_paper_bound_given_dispatch`. Discharges `Lemma16P7FullDispatchConclusion σ` (= `orderOf σ ∣ 343`) from the pr… Formalized auto L1059
Mačaj–Širáň 2010, §6, Lemma 17 — 51/51 formalized .lean
  • Lemma 17 case (1) arithmetic core: 3-group with `|X| ∣ 54` gives `|X| ∣ 27`. — For a 3-group `X` (`|X| = 3^k`), `|X| ∣ 54 = 2·27` forces `k ≤ 3` (since `3^4 = 81 > 54`), so `|X| ∈ {1, 3, 9, 27}`, all dividing `27` Formalized done L41
  • Lemma 17 case (1) modular bridge (geometric). — For a cyclic 3-group `⟨σ⟩` acting on Γ via a single permutation σ with `σ ^ 3^k = 1`, the σ-fixed-neighbour count at a fixed vertex `a` is divisible by 3 (since `Γ.degree a = 57 ≡ 0 (mod 3)`). This is the §6 Lem 17 N(… Formalized done L60
  • Lemma 17 case (1) conditional + arithmetic (combined). — If a single graph-automorphism σ has order a power of 3 (`σ^(3^k) = 1`), fixes a vertex `a`, and the count `|N(a) \ Fix(σ)| = 54` (the geometric "Petersen complement" assumption), then `orderOf σ ∣ 27`. This is the §6… Formalized done L78
  • Lemma 17 case (2) arithmetic core: 3-group with `|X| ≤ 81` gives `|X| ∣ 81`. — For a 3-group `X` (`|X| = 3^k`), `|X| ≤ 81 = 3^4` forces `k ≤ 4`, so `|X| ∈ {1, 3, 9, 27, 81}`, all dividing `81`. This is the §6 Lem 17 (case (2)) arithmetic step: combined with the paper's deeper analysis (Lem 21 +… Formalized done L96
  • Lemma 17 case (2) arithmetic enumeration: 3-group with `|X| ≤ 81`. — Enumeration form of `lem17_case2_arithmetic_3group_le_81_dvd_81`: the possible orders are exactly `{1, 3, 9, 27, 81}` Formalized done L111
  • Lemma 17 case (2) conditional + arithmetic (3-group, singleton fix). — If a single graph-automorphism σ has order a power of 3 (`σ^(3^k) = 1`) and `orderOf σ ≤ 81` (the paper's deeper bound for the singleton-fix case), then `orderOf σ ∣ 81` Formalized done L132
  • Lemma 17 case (2) semi-regular arithmetic core: 3-group with `|X| ∣ 57` gives `|X| ∣ 3`. — [done — C3.4] For a 3-group `X` (`|X| = 3^k`), `|X| ∣ 57 = 3 · 19` and `19` prime forces `3^k ∣ 3`, so `|X| ∈ {1, 3}`. This is the genuine semi-regular conclusion for the singleton-fix case: σ acts semi-regularly on t… Formalized auto L154
  • Lemma 17 case (2) unconditional bridge via `SingletonFixedData` and the C3.4 semi-regular orbit argument — [done — C3.4] For a 3-group element σ with singleton fix `{v}` acting semi-regularly on `N(v) \ Fix(σ) = N(v)` (the entire 57-element neighbourhood), the arithmetic core gives `orderOf σ ∣ 3` — sharper than the paper-… Formalized auto L174
  • Lemma 17 case (1) geometric: `|N(a) \ Fix(σ)| = 54` from `PetersenFixedData`. — For σ with `PetersenFixedData` on a Moore57 graph, the σ-moved neighbour count at any fixed vertex equals `54 = 57 − 3` (where `57` is the Moore57 degree and `3` is the Petersen induced degree). This is the §6 Lem 17… Formalized done L199
  • Lemma 17 case (1) full bridge via `PetersenFixedData` — combines the geometric data with a semi-regular orbit hypothesis to conclude `orderOf σ ∣ 27`. The hypothesis `h_semi_regular : orderOf σ ∣ 54` is the deferred geometric step (semi-regular action of `⟨σ⟩` on the 54-el… Formalized done L213
  • Lemma 17 case (1) unconditional bridge via `PetersenFixedData` and the C3.4 semi-regular orbit argument — [done — C3.4] Replaces the `h_semi_regular : orderOf σ ∣ 54` hypothesis of the conditional bridge `lem17_case1_orderOf_dvd_27_with_petersenFixedData` with the more paper-faithful semi-regular hypothesis `σ^k w = w → o… Formalized auto L232
  • Lemma 17 dispatch arithmetic: `orderOf σ ∣ 27 ∨ orderOf σ ∣ 81` ⟹ `orderOf σ ∣ 81`. — Paper-faithful packaging of the Lem 17 conclusion: both Petersen-fix (`|X| ∣ 27`) and singleton-fix (`|X| ∣ 81`) branches imply `|X| ∣ 81` Formalized done L248
  • Lemma 17 dispatch numeric bound: `|X| ≤ 81` from dispatch. Formalized done L255
  • Lemma 17 case (1) prime-case unconditional wrapper. — For σ a graph automorphism of Γ with σ³ = 1 (i.e. σ has order dividing the prime 3) and `PetersenFixedData Γ σ`, the bound `orderOf σ ∣ 27` holds trivially since `orderOf σ ∣ 3 ∣ 27`. This is the `k = 1` base case of… Formalized done L281
  • Lemma 17 case (2) prime-case unconditional wrapper. — For σ a graph automorphism of Γ with σ³ = 1 and `SingletonFixedData σ`, the bound `orderOf σ ∣ 3` holds trivially. Stronger than the paper's case (2) `∣ 81`: combined with C3.4 semi-regular conclusion `∣ 57` (which gi… Formalized done L297
  • Lemma 17 case (1) `k ≤ 3` unconditional wrapper. — For σ a graph automorphism of Γ with σ^(3^k) = 1 (where k ≤ 3) and `PetersenFixedData Γ σ`, the bound `orderOf σ ∣ 27` holds since `orderOf σ ∣ 3^k ∣ 27` for k ≤ 3. This extends the prime-case wrapper to cover k ∈ {0,… Formalized done L314
  • Lemma 17 case (2) paper-stated bound, `k ≤ 4` unconditional wrapper. — For σ a graph automorphism of Γ with σ^(3^k) = 1 (k ≤ 4) and `SingletonFixedData σ`, the paper-stated bound `orderOf σ ∣ 81` holds since `orderOf σ ∣ 3^k ∣ 81` for k ≤ 4. Covers σ of order ∈ {1, 3, 9, 27, 81} — i.e.,… Formalized done L337
  • Lemma 17 case (1) prime-case via semi-regular (fully unconditional). — [done — Path B] For σ a graph automorphism of Γ with σ^3 = 1 and `PetersenFixedData Γ σ`, the bound `orderOf σ ∣ 27` follows via: 1. prime-order semi-regular generator (`aut_semiRegular_at_movedNeighbor_of_prime`) 2.… Formalized auto L378
  • Lemma 17 case (2) prime-case via semi-regular (fully unconditional). — [done — Path B] For σ a graph automorphism of Γ with σ^3 = 1 and `SingletonFixedData σ`, the bound `orderOf σ ∣ 3` (sharper than paper's `∣ 81`) follows via: 1. prime-order semi-regular generator on the full neighbour… Formalized auto L399
  • Lemma 17 abstract conclusion (3-group fix classification). — For an automorphism group `X` of Γ that is a 3-group (so any element σ satisfies `σ ^ 3 ^ k = 1` for some `k`), the paper claims that either: * Case (1): `Fix(X)` is the Petersen graph and `|X| ∣ 27`; or * Case (2): `… Formalized auto L420
  • Lemma 17 (paper-faithful conditional 3-group fix shape). — [done — conditional] Proper-signature paper-faithful conditional: given a 3-group element `σ` (i.e., `σ^(3^k) = 1` for some k) and the deferred-heavy Fix-shape classification packaged as a disjunction (`PetersenFixedD… Formalized auto L433
  • Lemma 17 (3-group fix is Petersen or singleton, proper-signature paper-faithful form). — [done — paper-signature upgrade] Proper-signature replacement for the prior backward-compat True-stub. Given a 3-group element `σ` and the deferred-heavy Fix-shape classification packaged as a disjunction (PetersenFix… Formalized auto L463
  • Lemma 17 case (2) prime-case with explicit `fixedVertexCount σ = 1`. — [done — Path B, prime case] Given the §6 case-(2) fix-singleton fact `fixedVertexCount σ = 1`, construct `SingletonFixedData σ` via `singletonFixedData_of_fixedVertexCount_eq_one` and dispatch through `lem17_case2_ord… Formalized auto L509
  • Lemma 17 case (2) prime-case via small-fix narrowing. — [done — Path B, prime case] Given `fixedVertexCount σ ≤ 3` (the §6 Lem 16 case (2) shape-narrowing input via `lem16_case2_3group_fix_singleton_if_small`), the mod-3 constraint `fixedVertexCount σ ≡ 1 [MOD 3]` forces `… Formalized auto L531
  • Lemma 17 case (1) abstract conclusion — (Conclusion Prop encoding). For σ of order dividing `3^k` (k ≤ 3) acting as a graph automorphism of a Moore57 Γ with Petersen-fix shape (`PetersenFixedData Γ σ`), the paper's case (1) conclusion is: `orderOf σ ∣ 27`.… Formalized auto L564
  • Lemma 17 case (1) via Conclusion encoding (paper-faithful). — Given the `Lemma17Case1Conclusion σ` (the paper's case (1) divisibility bound), conclude `orderOf σ ∣ 27`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern used by `MainTheorem` Formalized done L572
  • Lemma 17 case (1) Conclusion instance, prime-case with PetersenFixedData. — [done — Path B, prime case] The Conclusion Prop `Lemma17Case1Conclusion σ` is discharged for `σ^3 = 1` graph automorphisms of a Moore57 Γ that satisfy the paper case-(1) Petersen-fix shape (`PetersenFixedData Γ σ`). N… Formalized auto L591
  • Lemma 17 case (2) abstract conclusion — (Conclusion Prop encoding). For σ of order dividing `3^k` acting as a graph automorphism of a Moore57 Γ with singleton-fix shape (`SingletonFixedData σ`), the paper-stated bound is `orderOf σ ∣ 81`; the C3.4 semi-regu… Formalized auto L608
  • Lemma 17 case (2) via Conclusion encoding (paper-faithful). — Given the `Lemma17Case2Conclusion σ` (the sharpened case (2) divisibility bound), conclude `orderOf σ ∣ 3`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern used by `MainTheorem` Formalized done L616
  • Lemma 17 case (2) via Conclusion encoding, paper-stated `∣ 81` form. — Weaker form of `lem17_case2_via_conclusion` that exposes the paper-stated bound `orderOf σ ∣ 81` (rather than the sharper `∣ 3`). Useful when interoperating with the original `Lemma17ThreeGroupFixConclusion` disjuncti… Formalized done L628
  • Lemma 17 case (2) Conclusion instance, prime-case with `SingletonFixedData`. — [done — Path B, prime case] The Conclusion Prop `Lemma17Case2Conclusion σ` is discharged for `σ^3 = 1` graph automorphisms of a Moore57 Γ that satisfy the paper case-(2) singleton-fix shape (`SingletonFixedData σ`). T… Formalized auto L644
  • Lemma 17 case (2) Conclusion instance, prime-case with explicit fix-singleton. — [done — Path B, prime case] Variant that exposes `fixedVertexCount σ = 1` as an explicit hypothesis, constructing `SingletonFixedData σ` internally via `singletonFixedData_of_fixedVertexCount_eq_one`. Mirrors `lem19_c… Formalized auto L659
  • Lemma 17 case (2) Conclusion instance, prime-case via small-fix. — [done — Path B, prime case] Variant that exposes `fixedVertexCount σ ≤ 3` as the small-fix narrowing input (which mod-3 narrows to `= 1`, then dispatches as above). Mirrors `lem19_case2_orderOf_dvd_19_prime_via_small_… Formalized auto L674
  • Lemma 17 per-case Conclusion ⟹ original disjunction Conclusion. — Combines `Lemma17Case1Conclusion` (`orderOf σ ∣ 27`, Petersen branch) and `Lemma17Case2Conclusion` (`orderOf σ ∣ 3`, singleton branch, sharpened) into the original `Lemma17ThreeGroupFixConclusion` disjunction (`orderO… Formalized done L689
  • Lemma 17 case (2) prime-case `orderOf σ ∣ 3` truly unconditional (singleton branch, via |Fix| < 10). — [done — Path B, Foundations commit `be72ed5`] The case-2 conclusion `orderOf σ ∣ 3` is derived **without** a `SingletonFixedData` hypothesis, by combining 1. `aut_order_three_SingletonFixedData_of_lt_10` (Foundations)… Formalized auto L745
  • Lemma 17 case (2) Conclusion prime-case truly unconditional (singleton branch, via |Fix| < 10). — [done — Path B, Foundations commit `be72ed5`] Conclusion-Prop wrapper around `lem17_case2_orderOf_dvd_3_prime_unconditional`. Discharges `Lemma17Case2Conclusion σ` (= `orderOf σ ∣ 3`) from the truly unconditional inpu… Formalized auto L764
  • Lemma 17 case (2) Conclusion prime-case via `|Fix(σ)| ≤ 9` (paper-signature variant). — [done — Path B, Foundations commit `be72ed5`] Paper-signature form using `≤ 9` (equivalent to `< 10`). Some upstream callers state the small-fix narrowing as `≤ 9` (the maximum `|Fix(σ)|` strictly less than the Peters… Formalized auto L779
  • Lemma 17 case (2) Conclusion prime-case via `|Fix(σ)| ≠ 10` (complement form). — [done — Path B, Foundations commit `be72ed5`] Alternate dispatch shape: the singleton branch is selected by excluding the Petersen branch `|Fix(σ)| = 10`. Combined with the unconditional dichotomy `|Fix(σ)| ∈ {1, 10}`… Formalized auto L797
  • Arithmetic core (local re-statement): `3^k ∣ 3249 ⟹ 3^k ∣ 9`. — For a 3-power `3^k`, divisibility by `3249 = 3² · 19²` forces `k ≤ 2` (since `3^3 = 27` and `27 ∤ 3249`), hence `3^k ∈ {1, 3, 9}`, all dividing `9`. Local copy of `Section07.lem21_arithmetic_3group_dvd_3249_implies_9`… Formalized done L865
  • Lemma 17 full dispatch (prime case, given Petersen uniqueness): per-case Conclusion disjunction. — [done — full wire, conditional on `PetersenUniqueness`] Given: * `hΓ : IsMoore57 Γ`, * `σ : Equiv.Perm V` with `σ^3 = 1` and `σ ≠ 1`, * `smul_adj` (σ is a graph automorphism), * `h_uniq : PetersenUniqueness` (the Bose… Formalized auto L1060
  • Lemma 17 full dispatch (prime case, given Petersen uniqueness): original disjunction form. — [done — full wire, conditional on `PetersenUniqueness`] Returns the paper-faithful `Lemma17ThreeGroupFixConclusion σ` (= the disjunction `orderOf σ ∣ 27 ∨ orderOf σ ∣ 81`), automatically dispatched between the Peterse… Formalized auto L1102
  • Lemma 17 full dispatch paper bound `orderOf σ ∣ 27` (combined upper). — [done — full wire, conditional on `PetersenUniqueness`] The paper's Lem 17 statement combines both branches under a single upper-bound divisor: `orderOf σ ∣ 27`. In the prime case (`σ^3 = 1`), both branches deliver th… Formalized auto L1123
  • Lemma 17 full dispatch Conclusion Prop encoding. — Encapsulates the combined paper-bound `orderOf σ ∣ 27` from the full dispatch as a `Prop`, paralleling `Lemma17Case1Conclusion` and `Lemma17Case2Conclusion`. Used by downstream Cor3 / MainTheorem dispatch chain when t… Formalized auto L1141
  • Lemma 17 full dispatch via Conclusion encoding. — Given the `Lemma17FullDispatchConclusion σ` Prop, conclude `orderOf σ ∣ 27`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern Formalized done L1149
  • Lemma 17 full dispatch Conclusion instance, given Petersen uniqueness. — [done — full wire, conditional on `PetersenUniqueness`] Conclusion-Prop wrapper around `lem17_3group_paper_bound_given_uniqueness`. Discharges `Lemma17FullDispatchConclusion σ` (= `orderOf σ ∣ 27`) from the prime-case… Formalized auto L1160
  • Lemma 17 full dispatch per-case — unconditional. — Discharges the `PetersenUniqueness` hypothesis of `lem17_3group_full_dispatch_per_case_given_uniqueness` via `Moore57.petersenUniqueness` Formalized done L1248
  • Lemma 17 full dispatch (paper-faithful disjunction) — unconditional. Formalized done L1256
  • Lemma 17 paper bound `orderOf σ ∣ 27` — unconditional. — The headline §6 Lem 17 prime-case bound, now landed as a sorry-free, hypothesis-free theorem (modulo the Moore57 graph assumption). Combines the §6 case analysis with the Bose 1963 / Hoffman–Singleton 1960 Petersen un… Formalized done L1269
  • Lemma 17 full dispatch Conclusion — unconditional. Formalized done L1277
  • Lem 17 sharp-singleton per-case dispatch — unconditional. Formalized done L1285
  • Lem 17 paper bound via sharp singleton — unconditional. Formalized done L1293
Mačaj–Širáň 2010, §6, Lemma 18 — 45/45 formalized .lean
  • Lemma 18 case (1) arithmetic core: 5-group with `|X| ∣ 50` gives `|X| ∣ 25`. — For a 5-group `X` (i.e., `|X| = 5^k` for some `k`), the constraint `|X| ∣ 50` forces `|X| ≤ 50` hence `k ≤ 2`, hence `|X| = 5^k ∈ {1, 5, 25}`, all of which divide `25`. This is the §6 Lem 18 (1) arithmetic step: semi-… Formalized done L51
  • Lemma 18 case (2) arithmetic core: 5-group with `|X| ∣ 55` gives `|X| ∣ 5`. — For a 5-group `X` (`|X| = 5^k`), `|X| ∣ 55 = 5·11` forces `k ≤ 1` since `5^2 = 25` does not divide `55`. Hence `|X| ∈ {1, 5}` and `|X| ∣ 5`. Combined with the orbit-stabilizer argument `|X| = 5·|Y|` and `|Y| ≤ 25` fro… Formalized done L69
  • Lemma 18 case (1) modular bridge (geometric). — For a single graph-automorphism σ with `σ^(5^k) = 1` fixing `a`, the σ-fixed-neighbour count satisfies `|N(a) ∩ Fix(σ)| ≡ 2 (mod 5)` (since `57 = 5·11 + 2`). This is the §6 Lem 18 N(a) modular ingredient: for `Fix(X)… Formalized done L94
  • Lemma 18 case (1) conditional + arithmetic. — If a single graph-automorphism σ has order a power of 5 (`σ^(5^k) = 1`) and `orderOf σ ∣ 50` (the geometric Hoffman–Singleton complement assumption `|N(a) \ Fix(σ)| = 50`), then `orderOf σ ∣ 25` Formalized done L108
  • Lemma 18 case (2) conditional + arithmetic. — If a single graph-automorphism σ has order a power of 5 (`σ^(5^k) = 1`) and `orderOf σ ∣ 55` (the geometric pentagon complement assumption `|N(a) \ Fix(σ)| = 55`), then `orderOf σ ∣ 5` Formalized done L122
  • Lemma 18 case (3) arithmetic core: 5-group with `|X| ∣ 3250` gives `|X| ∣ 125`. — For a 5-group `X` (`|X| = 5^k`) with `Fix(X) = ∅` and X acting semi-regularly on `V`, the orbit equation forces `|X| ∣ |V| = 3250`. Since `3250 = 2 · 5³ · 13`, the 5-part of `3250` is exactly `5³ = 125`, so `5^k ∣ 325… Formalized done L139
  • Lemma 18 case (3) conditional + arithmetic (5-group, empty fix). — If a single graph-automorphism σ has order a power of 5 (`σ^(5^k) = 1`) and `orderOf σ ∣ 3250` (semi-regular action on the whole vertex set, the geometric "Fix is empty" assumption), then `orderOf σ ∣ 125` Formalized done L157
  • Lemma 18 case (1) geometric: `|N(a) \ Fix(σ)| = 50` from `HSFixedData`. — For σ with `HSFixedData` on a Moore57 graph, the σ-moved neighbour count at any fixed vertex equals `50 = 57 − 7` (where `57` is the Moore57 degree and `7` is the Hoffman–Singleton induced degree). This is the §6 Lem… Formalized done L176
  • Lemma 18 case (1) full bridge via `HSFixedData` — combines the geometric data with a semi-regular orbit hypothesis to conclude `orderOf σ ∣ 25`. The hypothesis `h_semi_regular : orderOf σ ∣ 50` is the deferred geometric step (semi-regular action of `⟨σ⟩` on the 50-el… Formalized done L190
  • Lemma 18 case (1) unconditional bridge via `HSFixedData` and the C3.4 semi-regular orbit argument — [done — C3.4] Replaces `h_semi_regular : orderOf σ ∣ 50` with the paper-faithful semi-regular hypothesis on `N(a) \ Fix(σ)`. The complement-count is internalised via `hs_orderOf_dvd_50_of_semiRegular` Formalized auto L203
  • Lemma 18 case (2) geometric: `|N(a) \ Fix(σ)| = 55` from `C5FixedData`. — For σ with Pentagon (`C5FixedData`) on a Moore57 graph, the σ-moved neighbour count at any of the 5 fixed pentagon vertices equals `55 = 57 − 2` Formalized done L219
  • Lemma 18 case (2) full bridge via `C5FixedData` — conditional `PentagonFixedData + orderOf σ ∣ 55 ⟹ orderOf σ ∣ 5` Formalized auto L226
  • Lemma 18 case (2) unconditional bridge via `C5FixedData` and the C3.4 semi-regular orbit argument — [done — C3.4] Formalized auto L235
  • Lemma 18 case (3) geometric: `|V \ Fix(σ)| = 3250` from `EmptyFixedData`. — For σ with empty fix on a Moore57 graph, the σ-moved vertex count equals `3250 = |V|` Formalized done L251
  • Lemma 18 case (3) full bridge via `EmptyFixedData` — conditional `EmptyFixedData + orderOf σ ∣ 3250 ⟹ orderOf σ ∣ 125` Formalized auto L258
  • Lemma 18 case (3) unconditional bridge via `EmptyFixedData` and the C3.4 semi-regular orbit argument — [done — C3.4] The empty-fix case treats σ as acting semi-regularly on the entire vertex set, giving `orderOf σ ∣ 3250` Formalized auto L270
  • Lemma 18 dispatch arithmetic: `n ∣ 25 ∨ n ∣ 5 ∨ n ∣ 125` ⟹ `n ∣ 125`. — Paper-faithful packaging of the Lem 18 conclusion: each of the three fix-shape branches (HS, pentagon, empty) gives a divisibility bound, combined to `|X| ∣ 125` Formalized done L285
  • Lemma 18 dispatch numeric bound: `|X| ≤ 125` from dispatch. Formalized done L293
  • Lemma 18 case (1) prime-case unconditional wrapper. — For σ a graph automorphism of Γ with σ⁵ = 1 and `HSFixedData Γ σ`, the bound `orderOf σ ∣ 25` holds trivially since `orderOf σ ∣ 5 ∣ 25` Formalized done L313
  • Lemma 18 case (2) prime-case unconditional wrapper. — For σ a graph automorphism of Γ with σ⁵ = 1 and `C5FixedData Γ σ`, the bound `orderOf σ ∣ 5` holds trivially Formalized done L325
  • Lemma 18 case (3) prime-case unconditional wrapper. — For σ a graph automorphism of Γ with σ⁵ = 1 and `EmptyFixedData σ`, the bound `orderOf σ ∣ 125` holds trivially since `orderOf σ ∣ 5 ∣ 125` Formalized done L336
  • Lemma 18 case (1) `k ≤ 2` unconditional wrapper. — For σ a graph automorphism of Γ with σ^(5^k) = 1 (k ≤ 2) and `HSFixedData Γ σ`, the bound `orderOf σ ∣ 25` holds since `orderOf σ ∣ 5^k ∣ 25` for k ≤ 2. Extends the prime-case wrapper to cover k ∈ {0, 1, 2} (σ of orde… Formalized done L352
  • Lemma 18 case (3) `k ≤ 3` unconditional wrapper. — For σ a graph automorphism of Γ with σ^(5^k) = 1 (k ≤ 3) and `EmptyFixedData σ`, the bound `orderOf σ ∣ 125` holds since `orderOf σ ∣ 5^k ∣ 125` for k ≤ 3. Extends the prime-case wrapper to cover k ∈ {0, 1, 2, 3} (σ o… Formalized done L376
  • Lemma 18 case (1) prime-case via semi-regular (fully unconditional). — [done — Path B] For σ a graph automorphism of Γ with σ^5 = 1 and `HSFixedData Γ σ`, `orderOf σ ∣ 25` follows via: 1. prime-order semi-regular generator (`aut_semiRegular_at_movedNeighbor_of_prime`) 2. C3.4 semi-regula… Formalized auto L411
  • Lemma 18 case (2) prime-case via semi-regular (fully unconditional). — [done — Path B] For σ a graph automorphism of Γ with σ^5 = 1 and `C5FixedData Γ σ`, `orderOf σ ∣ 5` follows trivially (orderOf σ ∣ 5). The semi-regular path gives an alternative derivation through the C3.4 bridge (`c5… Formalized auto L428
  • Lemma 18 case (3) prime-case via semi-regular (fully unconditional). — [done — Path B] For σ a graph automorphism of Γ with σ^5 = 1 and `EmptyFixedData σ`, `orderOf σ ∣ 125` follows via: 1. prime-order semi-regular generator on the full vertex set (using `EmptyFixedData.no_fixed` and `se… Formalized auto L450
  • Lemma 18 case (1) abstract conclusion — (Conclusion Prop encoding). For σ a 5-group element acting as a graph automorphism of a Moore57 Γ with `Fix(⟨σ⟩) = Hoffman-Singleton`, the paper's case (1) conclusion is: `orderOf σ ∣ 25` (i.e., `|⟨σ⟩| ∈ {1, 5, 25}`).… Formalized auto L488
  • Lemma 18 case (2) abstract conclusion — (Conclusion Prop encoding). For σ a 5-group element acting as a graph automorphism of a Moore57 Γ with `Fix(⟨σ⟩) = Pentagon` (`C5FixedData`), the paper's case (2) conclusion at the cyclic level is: `orderOf σ ∣ 5` (th… Formalized auto L499
  • Lemma 18 case (3) abstract conclusion — (Conclusion Prop encoding). For σ a 5-group element acting as a graph automorphism of a Moore57 Γ with `Fix(⟨σ⟩) = ∅` (`EmptyFixedData`), the paper's case (3) conclusion is: `orderOf σ ∣ 125` (since the 5-part of `|V|… Formalized auto L510
  • Lemma 18 case (1) via Conclusion encoding (paper-faithful). — Given the `Lemma18Case1Conclusion σ` (the paper's case (1) HS-fix divisibility bound), conclude `orderOf σ ∣ 25`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern used by `MainTheorem` Formalized done L518
  • Lemma 18 case (2) via Conclusion encoding (paper-faithful). — Given the `Lemma18Case2Conclusion σ` (the paper's case (2) Pentagon-fix divisibility bound), conclude `orderOf σ ∣ 5`. Trivial bridge Formalized done L527
  • Lemma 18 case (3) via Conclusion encoding (paper-faithful). — Given the `Lemma18Case3Conclusion σ` (the paper's case (3) empty-fix divisibility bound), conclude `orderOf σ ∣ 125`. Trivial bridge Formalized done L536
  • Lemma 18 case (1) Conclusion instance, prime-case + HSFixedData. — The Conclusion Prop `Lemma18Case1Conclusion σ` is discharged for σ a graph automorphism of a Moore57 Γ with `σ^5 = 1` and `HSFixedData Γ σ`, via `lem18_case1_orderOf_dvd_25_with_HSFixedData_prime_via_semiRegular`. **P… Formalized done L553
  • Lemma 18 case (2) Conclusion instance, prime-case + C5FixedData. — The Conclusion Prop `Lemma18Case2Conclusion σ` is discharged for σ a graph automorphism of a Moore57 Γ with `σ^5 = 1` and `C5FixedData Γ σ`, via `lem18_case2_orderOf_dvd_5_with_c5FixedData_prime_via_semiRegular`. **Pl… Formalized done L571
  • Lemma 18 case (3) Conclusion instance, prime-case + EmptyFixedData. — The Conclusion Prop `Lemma18Case3Conclusion σ` is discharged for σ a graph automorphism of a Moore57 Γ with `σ^5 = 1` and `EmptyFixedData σ`, via `lem18_case3_orderOf_dvd_125_with_emptyFixedData_prime_via_semiRegular`… Formalized done L589
  • Lemma 18 prime-case Conclusion dispatch. — Given σ a graph automorphism of a Moore57 Γ with `σ^5 = 1`, the three-case fix-shape disjunction (HS / Pentagon / Empty) dispatches into the per-case Conclusion Props. This packages the paper's full §6 Lem 18 trichoto… Formalized done L603
  • Lemma 18 fix-shape dispatch Prop encoding (HS ⊕ Pentagon ⊕ Empty). — [done — Prop encoding] For σ a 5-group element acting as a graph automorphism of a Moore57 Γ with σ^5 = 1, the §6 Lem 18 trichotomy asserts that `Fix(σ)` is one of: * the Hoffman–Singleton subgraph (HS, witnessed by `… Formalized auto L672
  • Lemma 18 full dispatch paper bound `orderOf σ ∣ 125` (combined upper). — [done — full wire, conditional on `Lemma18FixShapeDispatch`] The paper's §6 Lem 18 statement combines the three fix-shape branches under a single upper-bound divisor: `orderOf σ ∣ 125`. In the prime case (σ^5 = 1), ea… Formalized auto L696
  • Lemma 18 full dispatch Conclusion Prop encoding. — Encapsulates the combined paper-bound `orderOf σ ∣ 125` from the full dispatch as a `Prop`, paralleling `Lemma17FullDispatchConclusion` and the per-case `Lemma18Case1/2/3Conclusion` props. Used by downstream Cor3 / Ma… Formalized auto L716
  • Lemma 18 full dispatch via Conclusion encoding. — Given the `Lemma18FullDispatchConclusion σ` Prop, conclude `orderOf σ ∣ 125`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern Formalized done L724
  • Lemma 18 full dispatch Conclusion instance, given fix-shape dispatch. — [done — full wire, conditional on `Lemma18FixShapeDispatch`] Conclusion-Prop wrapper around `lem18_5group_paper_bound_given_dispatch`. Discharges `Lemma18FullDispatchConclusion σ` (= `orderOf σ ∣ 125`) from the prime-… Formalized auto L735
  • Lemma 18 fix-shape dispatch from prime-case σ-data modulo HS uniqueness. — [done — Pentagon and Empty branches unconditional] Given the standard prime-case inputs (`σ^5 = 1`, `σ ≠ 1`, `smul_adj`) plus an *HS uniqueness* hypothesis `IsSRGWith 50 7 0 1 → HSFixedData Γ σ`, derive the full `Lemm… Formalized auto L778
  • Lemma 18 paper bound from prime-case σ-data modulo HS uniqueness. — [done — conditional only on HS uniqueness] Combines `lem18_5group_fixShapeDispatch_modulo_HSUniqueness` with `lem18_5group_paper_bound_given_dispatch` to give the §6 Lem 18 paper bound `orderOf σ ∣ 125` from σ-data pl… Formalized auto L805
  • Lemma 18 fix-shape dispatch from prime-case σ-data — unconditional. — [done — fully unconditional] The unconditional version of `lem18_5group_fixShapeDispatch_modulo_HSUniqueness`: discharges the `h_HS_unique` hypothesis by plugging in `Moore57.hsFixedData_of_isSRGWith` (the structural… Formalized auto L839
  • Lemma 18 paper bound from prime-case σ-data — unconditional. — [done — fully unconditional] The unconditional version of `lem18_5group_paper_bound_modulo_HSUniqueness`: routes through `lem18_5group_fixShapeDispatch_unconditional` to give `orderOf σ ∣ 125` from σ-data alone (`σ^5… Formalized auto L855
Mačaj–Širáň 2010, §6, Lemma 19 [deferred-heavy] — 44/44 formalized .lean
  • Lemma 19 case (1) arithmetic core: 13-group with `|X| ∣ 3250` is `Z₁₃`. — For `p = 13` and `X` a 13-group with `Fix(X) = ∅` (semi-regular on 3250 vertices ⟹ `|X| ∣ 3250`), the only nontrivial possibility is `|X| = 13` (since `13² = 169` does not divide `3250 = 2·5²·13`) Formalized done L42
  • Lemma 19 case (2) arithmetic core: 19-group with `|X| ∣ 57` is `Z₁₉`. — For `p = 19` and `X` a 19-group with `|Fix(X)| = 1` (semi-regular on `N(a) \ {a}` of size 57 ⟹ `|X| ∣ 57 = 3·19`), the only nontrivial possibility is `|X| = 19` (since `19² = 361` does not divide `57`) Formalized done L61
  • Lemma 19 case (3) arithmetic core: 11-group with `|X| ∣ 55` is `Z₁₁`. — For `p = 11` and `X` an 11-group with `Fix(X)` a pentagon (semi-regular on `N(a) \ Fix(X)` of size 55 ⟹ `|X| ∣ 55 = 5·11`), the only nontrivial possibility is `|X| = 11` Formalized done L79
  • Lemma 19 case (1) conditional + arithmetic (13-group, empty fix). — If σ has order a power of 13 (`σ^(13^k) = 1`) and `orderOf σ ∣ 3250` (semi-regular action on V), then `orderOf σ ∣ 13` Formalized done L97
  • Lemma 19 case (2) conditional + arithmetic (19-group, singleton fix). — If σ has order a power of 19 (`σ^(19^k) = 1`) and `orderOf σ ∣ 57` (semi-regular action on `N(a) \ {a}`), then `orderOf σ ∣ 19` Formalized done L113
  • Lemma 19 case (3) conditional + arithmetic (11-group, pentagon fix). — If σ has order a power of 11 (`σ^(11^k) = 1`) and `orderOf σ ∣ 55` (semi-regular action on `N(a) \ Fix(σ)` for pentagon Fix), then `orderOf σ ∣ 11` Formalized done L130
  • Lemma 19 cases (4)/(5) arithmetic core: 7-group with `|X| ∣ 56` is `Z₇` or trivial. — For `p = 7` and a 7-group `X` with `|X| ∣ 56 = 7·8`, the only possibilities are `|X| = 1` or `|X| = 7` (since `7² = 49` does not divide `56`). Geometric source (case (4) at a star leaf or case (5) at an edge endpoint)… Formalized done L152
  • Lemma 19 cases (4)/(5) conditional + arithmetic (7-group, star leaf or edge endpoint). — If σ has order a power of 7 (`σ^(7^k) = 1`) and `orderOf σ ∣ 56` (semi-regular action on `N(a) \ Fix(σ)` for a star-leaf or edge-endpoint `a`), then `orderOf σ ∣ 7`. The geometric source is the §6 case (4) star or cas… Formalized done L174
  • Lemma 19 case (1) geometric: `|V \ Fix(σ)| = 3250` from `EmptyFixedData`. Formalized done L187
  • Lemma 19 case (1) full bridge via `EmptyFixedData` — conditional `EmptyFixedData + orderOf σ ∣ 3250 ⟹ orderOf σ ∣ 13` (for 13-group) Formalized auto L194
  • Lemma 19 case (2) geometric: `|N(a) \ Fix(σ)| = 57` from `SingletonFixedData`. Formalized done L203
  • Lemma 19 case (2) full bridge via `SingletonFixedData` — conditional `SingletonFixedData + orderOf σ ∣ 57 ⟹ orderOf σ ∣ 19` (for 19-group) Formalized auto L210
  • Lemma 19 case (3) geometric: `|N(a) \ Fix(σ)| = 55` from `C5FixedData`. Formalized done L219
  • Lemma 19 case (3) full bridge via `C5FixedData` — conditional `C5FixedData + orderOf σ ∣ 55 ⟹ orderOf σ ∣ 11` (for 11-group) Formalized auto L226
  • Lemma 19 case (3) unconditional bridge via `C5FixedData` and the C3.4 semi-regular orbit argument — [done — C3.4] Mirrors `Lemma18.lem18_case2_orderOf_dvd_5_with_c5FixedData_semiRegular`: given an arbitrary `C5FixedData`, the C3.4 semi-regular bridge derives `orderOf σ ∣ 55`, which combined with `σ^{11^k}=1` gives `… Formalized auto L240
  • Lemma 19 case (3) prime-case via semi-regular (no `hsemi`). — [done — Path B prime case] For σ of prime order 11 (`σ^11 = 1`), the cyclic action is automatically semi-regular on every moved neighbour (`aut_semiRegular_at_movedNeighbor_of_prime`). Given `C5FixedData`, the C3.4 br… Formalized auto L259
  • Lemma 19 case (3) prime-case fully unconditional (no `C5FixedData`!). — [done — unconditional Path B] For σ a graph automorphism of a Moore57 graph with `σ^11 = 1` and `σ ≠ 1`, the pentagon-fix shape (`C5FixedData Γ σ`) is *constructed* unconditionally from `aut_order_eleven_C5FixedData`,… Formalized auto L285
  • Lemma 19 case (3) prime-case unconditional with trivial case. — Combines the `σ ≠ 1` non-trivial branch (derived via `aut_order_eleven_C5FixedData` + semi-regular C3.4 bridge) with the trivial `σ = 1` branch (where `orderOf σ = 1 ∣ 11`). This is the **strictly weakest** hypothesis… Formalized done L302
  • Lemma 19 case (3) abstract conclusion — (Conclusion Prop encoding). For σ of order 11 (or 1) acting as a graph automorphism of a Moore57 Γ, the paper's case (3) conclusion is: `orderOf σ ∣ 11`. Bundled as a Prop for downstream Cor3 dispatch chain, paralleli… Formalized auto L318
  • Lemma 19 case (3) via Conclusion encoding (paper-faithful). — Given the `Lemma19Case3Conclusion σ` (the paper's case (3) divisibility bound), conclude `orderOf σ ∣ 11`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern used by `MainTheorem` Formalized done L326
  • Lemma 19 case (3) Conclusion instance, prime-case unconditional. — The Conclusion Prop `Lemma19Case3Conclusion σ` is *unconditionally* discharged for `σ^11 = 1` graph automorphisms of a Moore57 Γ, via `lem19_case3_orderOf_dvd_11_prime_unconditional_total`. No `C5FixedData` hypothesis… Formalized done L337
  • Lemma 19 dispatch numeric bound: `n ≤ 19` from per-prime dispatch. — Paper-faithful packaging: any of the four large-prime branches (`n ∣ 13`, `n ∣ 19`, `n ∣ 11`, `n ∣ 7`) gives `n ≤ 19`, the largest prime in the Lemma 4 list Formalized done L349
  • Lemma 19 (paper-faithful conditional dispatch). — Proper-signature paper-faithful packaging: given the per-prime case dispatch (`n ∣ 13 ∨ n ∣ 19 ∨ n ∣ 11 ∨ n ∣ 7`) for the large-prime classification, conclude `n ≤ 19`. Re-export of `lem19_le_19_from_dispatch` with pa… Formalized done L364
  • Lemma 19 abstract conclusion (`n ≤ 19` envelope). — Paper's structural conclusion packaged: for the cardinality `n` of a large-prime `p`-group acting on Γ, `n ≤ 19` Formalized auto L373
  • Lemma 19 (large-prime `p`-group classification, proper-signature paper-faithful form). — [done — paper-signature upgrade] Proper-signature replacement for the prior backward-compat True-stub. Given the per-prime case dispatch (`n ∣ 13 ∨ n ∣ 19 ∨ n ∣ 11 ∨ n ∣ 7`) for the large-prime classification, conclud… Formalized auto L387
  • Lemma 19 (paper-faithful conclusion instance). — [done — conditional] Re-states `lem19_large_prime_pgroup_paper` using the abstract conclusion Prop `Lemma19LargePrimeConclusion` Formalized auto L396
  • Lemma 19 case (1) prime-case via `EmptyFixedData` and semi-regular. — [done — Path B, prime case] For σ a graph automorphism of a Moore57 graph with `σ^13 = 1` and an `EmptyFixedData σ` structure (the paper case-(1) shape input), the C3.4 semi-regular orbit bridge gives `orderOf σ ∣ 325… Formalized auto L438
  • Lemma 19 case (1) prime-case with explicit `fixedVertexCount σ = 0`. — [done — Path B, prime case, partial unconditional] Given the paper case-(1) fix-emptiness fact `fixedVertexCount σ = 0` (asserted by Lem 4 case (1) / Lem 16 case (1) for `p = 13`), construct `EmptyFixedData σ` via `au… Formalized auto L468
  • Lemma 19 case (1) prime-case via small-fix narrowing. — [done — Path B, prime case] Given `fixedVertexCount σ ≤ 12` (a paper-asserted bound for the 13-prime case, expected from the shape-classification chain), the mod-13 constraint `fixedVertexCount σ ≡ 0 [MOD 13]` forces… Formalized auto L491
  • Lemma 19 case (1) prime-case fully unconditional (no `EmptyFixedData`!). — [done — unconditional Path B] For σ a graph automorphism of a Moore57 graph with `σ^13 = 1` and `σ ≠ 1`, the empty-fix shape (`EmptyFixedData σ`) is *constructed* unconditionally from `aut_order_thirteen_EmptyFixedDat… Formalized auto L526
  • Lemma 19 case (1) prime-case unconditional with trivial case. — Combines the `σ ≠ 1` non-trivial branch (derived via `aut_order_thirteen_EmptyFixedData_unconditional` + semi-regular C3.4 bridge) with the trivial `σ = 1` branch (where `orderOf σ = 1 ∣ 13`). This is the **strictly w… Formalized done L546
  • Lemma 19 case (1) abstract conclusion — (Conclusion Prop encoding). For σ of order 13 (or 1) acting as a graph automorphism of a Moore57 Γ, the paper's case (1) conclusion is: `orderOf σ ∣ 13`. Bundled as a Prop for downstream Cor3 dispatch chain, paralleli… Formalized auto L564
  • Lemma 19 case (1) via Conclusion encoding (paper-faithful). — Given the `Lemma19Case1Conclusion σ` (the paper's case (1) divisibility bound), conclude `orderOf σ ∣ 13`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern Formalized done L572
  • Lemma 19 case (1) Conclusion instance, prime-case with fix-emptiness. — [done — partial unconditional] The Conclusion Prop `Lemma19Case1Conclusion σ` is discharged for `σ^13 = 1` graph automorphisms of a Moore57 Γ that satisfy the paper case-(1) fix-emptiness `fixedVertexCount σ = 0`. No… Formalized auto L585
  • Lemma 19 case (1) Conclusion instance, prime-case unconditional. — The Conclusion Prop `Lemma19Case1Conclusion σ` is *unconditionally* discharged for `σ^13 = 1` graph automorphisms of a Moore57 Γ, via `lem19_case1_orderOf_dvd_13_prime_unconditional_total`. No `EmptyFixedData`, `fixed… Formalized done L606
  • Lemma 19 case (2) prime-case via `SingletonFixedData` and semi-regular. — [done — Path B, prime case] For σ a graph automorphism of a Moore57 graph with `σ^19 = 1` and a `SingletonFixedData σ` structure (the paper case-(2) shape input), the C3.4 semi-regular orbit bridge gives `orderOf σ ∣… Formalized auto L645
  • Lemma 19 case (2) prime-case with explicit `fixedVertexCount σ = 1`. — [done — Path B, prime case] Given the paper case-(2) fix-singleton fact `fixedVertexCount σ = 1` (supplied either as a hypothesis or — for the 19-prime — derivable unconditionally from `order19_aut_fixedVertexCount_eq… Formalized auto L675
  • Lemma 19 case (2) prime-case via small-fix narrowing. — [done — Path B, prime case] Given `fixedVertexCount σ ≤ 19` (which is implied by virtually any shape-narrowing input for the 19-prime case), the mod-19 constraint `fixedVertexCount σ ≡ 1 [MOD 19]` forces `fixedVertexC… Formalized auto L694
  • Lemma 19 case (2) prime-case fully unconditional. — [done — unconditional Path B] For σ a graph automorphism of a Moore57 graph with `σ^19 = 1` and `σ ≠ 1`, the singleton-fix shape (`SingletonFixedData σ`) is *constructed* unconditionally from `aut_order_nineteen_Singl… Formalized auto L725
  • Lemma 19 case (2) prime-case unconditional with trivial case. — Combines the `σ ≠ 1` non-trivial branch (derived via `aut_order_nineteen_SingletonFixedData` + semi-regular C3.4 bridge) with the trivial `σ = 1` branch (where `orderOf σ = 1 ∣ 19`). This is the **strictly weakest** h… Formalized done L743
  • Lemma 19 case (2) abstract conclusion — (Conclusion Prop encoding). For σ of order 19 (or 1) acting as a graph automorphism of a Moore57 Γ, the paper's case (2) conclusion is: `orderOf σ ∣ 19`. Bundled as a Prop for downstream Cor3 dispatch chain, paralleli… Formalized auto L761
  • Lemma 19 case (2) via Conclusion encoding (paper-faithful). — Given the `Lemma19Case2Conclusion σ` (the paper's case (2) divisibility bound), conclude `orderOf σ ∣ 19`. Trivial bridge — exposed for the Conclusion-Prop dispatch pattern used by `MainTheorem` Formalized done L769
  • Lemma 19 case (2) Conclusion instance, prime-case unconditional. — The Conclusion Prop `Lemma19Case2Conclusion σ` is *unconditionally* discharged for `σ^19 = 1` graph automorphisms of a Moore57 Γ, via `lem19_case2_orderOf_dvd_19_prime_unconditional_total`. No `SingletonFixedData` or… Formalized done L780
  • Lemma 19 case (2) Conclusion instance, with explicit fix-singleton. — Variant of `lem19_case2_conclusion_prime_unconditional` that exposes `fixedVertexCount σ = 1` as an explicit hypothesis, for parallelism with `lem19_case1_conclusion_prime_with_fix_count_zero`. Useful for callers that… Formalized done L793
Mačaj–Širáň 2010, §6, Lemma 20 — 2/2 formalized .lean
  • Lemma 20 — in its abstract index form: for any subgroup `H` of `G`, `[N_G(H) : H] · [G : N_G(H)] = [G : H]`. This is the algebraic core behind the orbit-conjugate counting identity Formalized auto L51
  • Lemma 20 — in its index form for actions: for any `MulAction G α` and `o : α`, `[N_G(stab o) : stab o] · [G : N_G(stab o)] = |orbit G o|` Formalized auto L57
Mačaj–Širáň 2010, §6, Theorem 4 — 5/5 formalized .lean
  • Theorem 4 arithmetic core: `n ∣ 27` from dispatch + Cor 2 exclusion — Given the two-case Lem 17 dispatch (`Fix(X) = Petersen ⟹ n ∣ 27` / `Fix(X) = singleton ⟹ n ∣ 81`), plus the Section 7 Cor 2 exclusion of `n = 81` (the unique SG(81, 9) is excluded), conclude `n ∣ 27`. The case-(1) bra… Formalized done L39
  • Theorem 4 exponent bound: 3-group with dispatch + ≠ 81 has k ≤ 3 — For a 3-group `|X| = 3^k`, the Lem 17 dispatch plus Cor 2 exclusion forces `k ≤ 3` Formalized done L92
  • Theorem 4 numeric bound: |X| ≤ 27 from dispatch + Cor 2 exclusion Formalized done L110
  • Theorem 4 (paper-faithful conditional bound). — Proper-signature paper-faithful packaging: given Lem 17 dispatch (`n ∣ 27 ∨ n ∣ 81`) and Cor 2 SG(81,9) exclusion (`n ≠ 81`), conclude `n ∣ 27 ∧ n ≤ 27`. Re-export of `thm4_card_dvd_27_from_dispatch_and_cor2` + `thm4_… Formalized done L125
  • Theorem 4 (3-group order ≤ 27, proper-signature paper-faithful form). — [done — paper-signature upgrade] Proper-signature replacement for the prior backward-compat True-stub. Given the Lem 17 dispatch (`n ∣ 27 ∨ n ∣ 81`) and the Section 7 Cor 2 exclusion (`n ≠ 81`), the Thm 4 paper bound… Formalized auto L142
Mačaj–Širáň 2010, §6, Theorem 5 — 6/6 formalized .lean
  • Theorem 5 arithmetic core: |X| dvd 125 from three-case dispatch — Given the dispatch over the three Lem 18 fix-shape cases (HS / pentagon / empty), each producing the Thm 5 divisibility bound, the combined `|X| ∣ 125` follows by case analysis Formalized done L44
  • Theorem 5 bound: |X| ≤ 125 from three-case dispatch — The numeric form: under the same three-case dispatch, `|X| ≤ 125` Formalized done L55
  • Theorem 5 5-group exponent bound: 5^k ∣ 125 ⟹ k ≤ 3 — The exponent form: for any 5-group `5^k`, `|X| ∣ 125` forces `k ≤ 3`, hence `|X| ∈ {1, 5, 25, 125}` Formalized done L65
  • Theorem 5 excludes 5-group of order 625 — For a 5-group `X` (`|X| = 5^k`), the Thm 5 dispatch forces `|X| ≠ 625` (since `625 = 5^4` would require `k = 4`, but `|X| ∣ 125` gives `k ≤ 3`) Formalized done L78
  • Theorem 5 (paper-faithful conditional bound). — Proper-signature paper-faithful packaging: given the three-case Section 8 dispatch (`n ∣ 5 ∨ n ∣ 25 ∨ n ∣ 125`), conclude `n ∣ 125 ∧ n ≤ 125` Formalized done L97
  • Theorem 5 (5-group order bound, proper-signature paper-faithful form). — [done — paper-signature upgrade] Proper-signature replacement for the prior backward-compat True-stub. Given the three-case Section 8 dispatch (`n ∣ 5 ∨ n ∣ 25 ∨ n ∣ 125`) for the Lem 18 fix-shape trichotomy (HS / pen… Formalized auto L115

§7 Theorem 4 proof

27 formalized · 4 pending · 0 out of scope · total 31

Mačaj–Širáň 2010, §7, Corollary 2 [GAP] — 3/4 formalized, 1 pending .lean
  • Corollary 2 Conclusion (paper-faithful Prop encoding). — Encodes the Corollary 2 classification result: any 3-group `X` of order 81 acting on a Moore57 graph `Γ` as graph automorphisms is isomorphic to the GAP small group `SG819 = (Z₉ × Z₃) ⋊ Z₃`. The unconditional form req… Formalized done L55
  • Corollary 2 Exclusion Conclusion — (Cor 2 chain-role encoding). Companion to `Cor2SG819Conclusion` capturing the *role of Cor 2 in the §7 Theorem 4 chain*: any 3-group acting on Moore57 cannot have order 81 (combining Cor 2 classification `X ≅ SG819` w… Formalized done L71
  • Corollary 2 exclusion (`|X| ≠ 81` for 3-groups on Γ, paper-faithful conditional). — Proper-signature paper-faithful packaging of the Cor 2 chain role: given the `Cor2SG819ExclusionConclusion` hypothesis, conclude that any subgroup `X` of `Equiv.Perm V` acting on `Γ` as graph automorphisms has `Fintyp… Formalized done L107
  • Corollary 2 (`|X| = 81` ⇒ `X = SmallGroup(81, 9)`). — Backwards-compat True-stub. The paper-faithful content is captured by `Cor2SG819Conclusion` / `cor2_smallGroup_81_9_paper` (classification form) and `Cor2SG819ExclusionConclusion` / `cor2_smallGroup_81_9_exclusion_pap… Pending GAP-computation L126
Mačaj–Širáň 2010, §7, Lemma 21 [proper-signature subgroup form + deferred-heavy] — 16/18 formalized, 2 pending .lean
  • Lemma 21 (1) arithmetic core: index-9 trivial intersection forces `|X| = 9`. — If `X1, X2 ◁ X` are normal subgroups of index 3, then their intersection `X1 ∩ X2` has index dividing 9. The geometric content of Lemma 21 (1) (every element of `X1 ∩ X2` fixes ≥ 6 elements of `N(a)`) forces this inte… Formalized done L63
  • Lemma 21 (2) arithmetic core: orbit-stabilizer chain gives `|X| = 27`. — For `X` acting on Γ with `|Fix(X)| = {a}` and an orbit `O ⊆ N(a)` of size 9, the paper's argument produces a chain `X ⊇ X_o ⊇ X_{oo'}` with: - `[X : X_o] = |O| = 9` (orbit-stabilizer at o ∈ O). - `[X_o : X_{oo'}] = |o… Formalized done L84
  • Lemma 21 (2) arithmetic bound: `|X| ≤ 27` from index chain. — A weaker conditional matching the paper's stated bound `|X| ≤ 27`: if `|X| = 9 · |X_o|` and `|X_o| ≤ 3`, then `|X| ≤ 27`. (The `|X_o| ≤ 3` factor comes from `[X_o : X_{oo'}] = 3` plus the non-trivial-stabilizer altern… Formalized done L102
  • Lemma 21 (1) (subgroup form, proper-signature). — [done — arithmetic] Mathlib `Subgroup`-API form of part (1). Given a subgroup `X` of any group `G` and a subgroup `X₁₂ ≤ X` of `X` with `[X : X₁₂] = 9` (the paper's "intersection of two index-3 normal subgroups") and… Formalized auto L124
  • Lemma 21 (2) (subgroup form, proper-signature). — [done — arithmetic] Mathlib `Subgroup`-API form of part (2): orbit-stabilizer chain gives `|X| = 27`. Given `X_o ≤ X` (stabilizer of orbit point `o`) with `[X : X_o] = 9` (orbit size 9) and `X_oo ≤ X_o` (deeper stabil… Formalized auto L139
  • Lemma 21 (1) (paper-signature, proper-signature, proven). — [done — paper-signature bridge] Given the geometric condition `Lemma21TwoSize3OrbitsCondition X` (i.e., the existence of an index-9 trivial subgroup of `X`, the group- theoretic encoding of "two orbits of size 3 on `N… Formalized auto L219
  • Lemma 21 (2) (paper-signature, proper-signature, proven). — [done — paper-signature bridge] Given the geometric condition `Lemma21Size9OrbitCondition X` (the orbit-stabilizer chain `X_oo ≤ X_o ≤ X` with `[X : X_o] = 9`, `[X_o : X_oo] = 3`, `|X_oo| = 1`), conclude `|X| = 27` by… Formalized auto L239
  • Lemma 21 (1) (two size-3 orbits on `N(a)` ⇒ `|X| = 9`). — Arithmetic backbone via `lem21_part1_index_arithmetic` and the proper- signature `lem21_part1_subgroup_paper`. Backward-compat True-stub — see `lem21_two_size3_orbits_paper_signature` for the paper-signature proven form Pending deferred L254
  • Lemma 21 (2) (size-9 orbit on `N(a)` ⇒ `|X| ≤ 27`). — Arithmetic backbone via `lem21_part2_orbit_stabilizer_arithmetic`, `lem21_part2_card_le_27`, and `lem21_part2_subgroup_paper`. Backward-compat True-stub — see `lem21_size9_orbit_paper_signature` for the paper-signatur… Pending deferred L262
  • Arithmetic core: `3^k ∣ 3249 ⟹ 3^k ∣ 9`. — For a 3-power `3^k`, divisibility by `3249 = 3² · 19²` forces `k ≤ 2` (since `3^3 = 27` and `gcd(27, 3249) = 9 < 27`, so `27 ∤ 3249`), hence `3^k ∈ {1, 3, 9}`, all dividing `9`. This is the arithmetic step used by `le… Formalized done L299
  • Backup: `|X| ≤ 27` group-form arithmetic (no graph hypothesis). — Combinatorial group-arithmetic version of `lem21_part2_card_le_27`: given subgroups `X_o ≤ X` with `[X : X_o] = 9` and `|X_o| ≤ 3`, conclude `|X| ≤ 27`. This is the cleanest Lagrange-style packaging of part (2)'s uppe… Formalized done L406
  • Constructor for `Lemma21TwoSize3OrbitsCondition`. — Given explicit witness data — a subgroup `X₁₂ : Subgroup G` with `[X : X₁₂] = 9` and `|X₁₂| = 1` (the group-theoretic encoding of "two distinct stabilizers of orbits of size 3 ⇒ trivial intersection") — this packages… Formalized done L445
  • Constructor for `Lemma21Size9OrbitCondition`. — Given the orbit-stabilizer chain `X_oo ≤ X_o ≤ X` with `[X : X_o] = 9`, `[X_o : X_oo] = 3`, and `|X_oo| = 1`, package it as the existential `Lemma21Size9OrbitCondition X`. Trivial constructor exposed as a named lemma… Formalized done L461
  • Combined: witness subgroups ⇒ `|X| = 9`. — Composition of `lem21_two_size3_orbits_condition_from_subgroups` with `lem21_two_size3_orbits_paper_signature`. Lets a geometric site producing `(X₁₂, [X:X₁₂]=9, |X₁₂|=1)` jump straight to `|X| = 9` in one named step Formalized done L476
  • Combined: orbit-stabilizer chain ⇒ `|X| = 27`. — Composition of `lem21_size9_orbit_condition_from_chain` with `lem21_size9_orbit_paper_signature`. Lets a geometric site producing the `X_oo ≤ X_o ≤ X` chain jump straight to `|X| = 27` Formalized done L489
  • Graph-automorphism specialization: two-size-3-orbits condition for `X : Subgroup (Equiv.Perm V)`. — The Moore57 use case: `G = Equiv.Perm V` (graph automorphism group). Identical statement to `lem21_two_size3_orbits_condition_from_subgroups`, but pinned to the permutation-group specialization for downstream use at t… Formalized done L509
  • Graph-automorphism specialization: size-9 orbit chain condition for `X : Subgroup (Equiv.Perm V)`. — The Moore57 use case for part (2): pinned to the permutation-group specialization. Lets the orbit-stabilizer chain produced at the graph site discharge `Lemma21Size9OrbitCondition X` in one applied lemma Formalized done L522
  • Cor 2 orbit structure on N(a) for `|X| = 81` (pure arithmetic core). — Given non-negative integer counts `a, b, c` of orbits of sizes `3, 9, 27` respectively, summing to `|N(a)| = 57` (no size-1 or size-81 orbits by `Fix(X) = {a}` and `|X| = 81 > 57`), plus the Lem 21 contrapositive inpu… Formalized done L561
Mačaj–Širáň 2010, §7, Theorem 4 (full proof) [deferred-heavy] — 8/9 formalized, 1 pending .lean
  • Step 4-5 arithmetic contradiction. — In the §7 proof, Lemma 8 plus Lemma 9 give `81 * (26 + 30 l) = 18 * a₁(x)`, while the common `Z₉ × Z₃` orbit splitting gives `a₁(x) = 27 k`. These two numerical constraints are incompatible Formalized done L39
  • Step 4-5 sharper arithmetic contradiction (ℤ form, parity-free). — Drops the parity input: Lemma 8's mod-15 congruence alone, combined with Lemma 9's trace-a₁ link and the orbit-splitting, suffices to derive a contradiction. This isolates the *minimal* set of arithmetic constraints t… Formalized done L60
  • Lemma 8 + parity ⇒ `Tr = 26 + 30·l` pin-down. — Combining Lemma 8 (mod-15 congruence with `k = 48`) and Lemma 6 (2) parity (`|X| = 81` odd ⇒ `Tr(X)` even) via CRT pins `Tr(X)` to the form `26 + 30·l` that appears in the §7 Theorem 4 proof Formalized done L72
  • Theorem 4 conditional form: contradiction from the three §7 geometric inputs. — [done given hypotheses] Encodes the conditional content of §7 Steps 4-5 with the paper's intermediate quantities exposed: * `X` is an order-81 subgroup of `Sym(V)` acting by graph automorphisms on a Moore57 graph `Γ`.… Formalized auto L98
  • Theorem 4 (Section 7 full proof) arithmetic dispatch — Given the Section 7 dispatch (Lem 17 case 1: `|X| ∣ 27` from Petersen-fix; Lem 17 case 2 + Cor 2 sharpening: `|X| ∣ 81` with `|X| ≠ 81` from SG(81, 9) classification), conclude `|X| ∣ 27`. Directly delegates to the Se… Formalized done L118
  • Theorem 4 (Section 7) exponent bound — For a 3-group `|X| = 3^k`, the dispatch + Cor 2 exclusion forces `k ≤ 3`. Delegates to Section 6's `thm4_3pow_le_3_from_dispatch` Formalized done L129
  • Theorem 4 (Section 7) numeric bound — The dispatch + Cor 2 exclusion gives `|X| ≤ 27` Formalized done L139
  • Theorem 4 (paper-faithful Section-7 conditional bound). — Proper-signature paper-faithful packaging at the Section-7 level: given Section 7 Lem 17 dispatch (`n ∣ 27 ∨ n ∣ 81`) and Cor 2 SG(81,9) exclusion (`n ≠ 81`), conclude `n ∣ 27 ∧ n ≤ 27` Formalized done L151
  • Theorem 4 (no 3-group of order > 27). — Arithmetic backbone via `thm4_final_dvd_27_from_dispatch_and_cor2`, `thm4_final_3pow_le_3_from_dispatch`, and `thm4_final_card_le_27_from_dispatch_and_cor2` / `thm4_final_paper` (above). What remains is the Cor 2 geom… Pending deferred L165

§8 Theorem 5 proof

65 formalized · 0 pending · 0 out of scope · total 65

Mačaj–Širáň 2010, §8, Lemma 22 [GAP] — 6/6 formalized .lean
  • Lemma 22 arithmetic: orbit-stabilizer at size-25 orbits — For `|X| = 625` and a vertex `v` in a size-25 orbit `O`, the vertex stabilizer `Stab_X(v)` has order `|X|/|O| = 625/25 = 25` by the orbit-stabilizer theorem Formalized done L42
  • Lemma 22 arithmetic: orbit decomposition with smallest orbit = 25 — For `|X| = 625` acting with smallest orbit size 25 (so all orbits have size in `{25, 125, 625}`), the orbit count equation `25·i + 125·j + 625·k = 3250` reduces to `i + 5·j + 25·k = 130` (with `i ≥ 1`). The pure arith… Formalized done L62
  • Lemma 22 arithmetic: `5^k = 625 ↔ k = 4`. — The order-625 hypothesis pins the 5-group exponent uniquely as `5^4` Formalized done L71
  • Lemma 22 arithmetic: 5-group with `|X| ∣ 625` enumeration. — For a 5-group `X` (`|X| = 5^k`), `|X| ∣ 625 = 5^4` forces `|X| ∈ {1, 5, 25, 125, 625}` Formalized done L88
  • Lemma 22 conditional + arithmetic (5-group, order 625). — If a single graph-automorphism σ has order a power of 5 (`σ^(5^k) = 1`) and `orderOf σ ∣ 625`, then `orderOf σ ∈ {1, 5, 25, 125, 625}` Formalized done L108
  • Lemma 22 (paper-faithful arithmetic core, orbit-stabilizer + 5-group divisors) — — discharged. Replaces the prior backward-compat True-stub with the proven arithmetic backbone composing `lem22_arithmetic_stabilizer_25`, `lem22_arithmetic_orbit_25_dvd_625`, and `lem22_arithmetic_5group_dvd_625_enum… Formalized done L134
Mačaj–Širáň 2010, §8, Lemma 23 — 3/3 formalized .lean
  • Lemma 23 arithmetic: orbit-stabilizer at size-125 orbits — For `|X| = 625` and a vertex `v` in a size-125 orbit `O`, the vertex stabilizer `Stab_X(v)` has order `|X|/|O| = 625/125 = 5` by the orbit-stabilizer theorem. The lemma takes the algebraic statement `|X| = stab · orbi… Formalized done L37
  • Lemma 23 (paper-faithful arithmetic form). — Proper-signature paper-faithful packaging: for |X| = 625 acting with smallest orbit of size 125, the vertex stabilizer has order 5 (by orbit-stabilizer). This is the arithmetic substance of Lem 23 (the "|Y| = 5" claim) Formalized done L70
  • Lemma 23 (paper-faithful arithmetic core, conditional) — — discharged. Replaces the prior backward-compat True-stub with the proven `lem23_stabilizer_orbits_paper` (which packages `lem23_arithmetic_stabilizer_order` and `lem23_arithmetic_5_dvd_625` into the |Y| = 5 ∧ 5 ∣ 62… Formalized done L94
Mačaj–Širáň 2010, §8, Lemma 24 — 5/5 formalized .lean
  • Lemma 24 arithmetic core: orbit decomposition for `|X| = 625` with smallest orbit `≥ 125`. — Given non-negative integers `i, j` (numbers of size-625 and size-125 orbits respectively) with `625·i + 125·j = 3250`, the solutions are precisely the six pairs: `(0, 26), (1, 21), (2, 16), (3, 11), (4, 6), (5, 1)`. P… Formalized done L45
  • Lemma 24 conditional bridge: `j ≥ 2` from excluding `(5, 1)`. — The orbit-decomposition arithmetic gives six configurations. Five of them (the `j ∈ {26, 21, 16, 11, 6}` cases) directly satisfy `j ≥ 2`. The remaining case `(i, j) = (5, 1)` is excluded by the paper's central-order-5… Formalized done L62
  • Lemma 24 arithmetic core: `j ≥ 1` always — Even without the central-element argument, the orbit-decomposition arithmetic itself forces `j ≥ 1`: there is no solution to `625·i + 125·j = 3250` with `j = 0` (since `3250 / 625 = 5.2`, not an integer). This is a st… Formalized done L84
  • Lemma 24 (paper-faithful conditional `j ≥ 2`). — Proper-signature paper-faithful form: given the orbit-decomposition `625·i + 125·j = 3250` and the (deferred) paper exclusion of `(i, j) = (5, 1)`, conclude `j ≥ 2`. Re-export combination of `lem24_arithmetic_j_ge_one… Formalized done L95
  • Lemma 24 (paper-faithful conditional `j ≥ 2`) — — discharged. Replaces the prior backward-compat True-stub with the proven `lem24_two_orbits_paper`: given the orbit-decomposition equation `625·i + 125·j = 3250` and the paper-deferred exclusion of `(i, j) = (5, 1)`,… Formalized done L123
Mačaj–Širáň 2010, §8, Proposition 3 [deferred-heavy] — 22/22 formalized .lean
  • Proposition 3 arithmetic core: no partition of 7 has square-sum 31. — For non-negative integers `x_0, ..., x_7` where `x_k` is the count of parts equal to `k`, the simultaneous constraints `1·x_1 + 2·x_2 + 3·x_3 + 4·x_4 + 5·x_5 + 6·x_6 + 7·x_7 = 7` `1·x_1 + 4·x_2 + 9·x_3 + 16·x_4 + 25·x… Formalized done L53
  • Proposition 3 prime-case unconditional wrapper. — For σ a graph automorphism of Γ with σ⁵ = 1 (prime base case k = 1) and `HSFixedData Γ σ`, the bound `orderOf σ ≤ 5` holds trivially since `orderOf σ ∣ 5`. This is the `k = 1` base case of Proposition 3. The composite… Formalized done L81
  • Proposition 3 arithmetic step: `n ∣ 25 ∧ n ≠ 25 ⟹ n ≤ 5`. — [done — C3.6] Since `25 = 5²`, the divisors of 25 are `{1, 5, 25}`. Excluding 25 leaves `{1, 5}`, both of which are at most 5 Formalized auto L98
  • Proposition 3 conditional bridge via `HSFixedData` (Lem 18 (1) input form) — [done — C3.6] Given: * `σ ^ 5^k = 1` (σ is a 5-group element), * `HSFixedData Γ σ` (Fix(σ) = Hoffman–Singleton), * `h_semi_regular : orderOf σ ∣ 50` (Lem 18 (1) input — semi-regular action of σ on `N(a) \ Fix(σ)`), *… Formalized auto L124
  • Proposition 3 unconditional bridge via `HSFixedData` and the C3.4 semi-regular orbit argument — [done — C3.6] Replaces the `h_semi_regular : orderOf σ ∣ 50` numeric hypothesis with the paper-faithful semi-regular hypothesis on `N(a) \ Fix(σ)`. The remaining deferred input is `h_no_25` (paper §8 step 1-5 conclusion) Formalized auto L141
  • Proposition 3 (Hoffman–Singleton-fix 5-group `|X| ≤ 5`, paper-faithful arithmetic + structural conditional) — — discharged. Replaces the prior backward-compat True-stub with the proven `prop3_hs_fix_bound_with_hsFixedData` (which composes `prop3_arithmetic_dvd_25_ne_25_le_5` with Section 6's `lem18_case1_orderOf_dvd_25_with_H… Formalized done L176
  • Proposition 3 abstract conclusion (paper claim) — for any 5-group element σ with HS-shape fix, `|X| ≤ 5`. This is the Tier B finalize-style abstract `Conclusion : Prop` def for Proposition 3. Once the `|X| = 25` exclusion (paper §8 step 1-5) is Lean-internalised, thi… Formalized auto L191
  • Proposition 3 arithmetic core packaged as the §8 step 5 abstract conclusion — [done — C3.6] `prop3_arithmetic_core_no_partition_of_7_with_sq_31` repackaged as a Prop-level non-existence statement, exposing the §8 step 5 conclusion in the form usable by downstream `Proposition3` bridges Formalized auto L201
  • Proposition 3 direct-form Diophantine bridge (paper-faithful). — [done — research] Paper §8 equations (7) and (8) state: * `∑_{i=151}^{177} b_{178,i} = 7` (eq 7, degree sum) * `∑_{i=151}^{177} b_{178,i}² = 31` (eq 8, derived from B² + B − 56I) These 27 non-negative integer variable… Formalized auto L226
  • Proposition 3 direct-form step 5 conclusion (paper-faithful) — [done — research] The paper-faithful statement of paper §8 step 5: there is no non-negative integer assignment to 27 variables `b_i` with sum 7 and sum-of-squares 31. This is the abstract version of `prop3_no_solution… Formalized auto L302
  • Item 4: Lem 5(5) at diagonal entry `(i, i)`. — Direct consequence of `lem5_matrix_identity` at `i = j`: `(B²)_{i, i} = 56 + sᵢ - bᵢᵢ`. For `i = 178` (chosen free orbit), `sᵢ = 25` (orbit size), `bᵢᵢ = 0` (trace), giving `(B²)_{178, 178} = 56 + 25 - 0 = 81` Formalized done L438
  • Step 1 arithmetic core: orbit decomposition `50 + 100 + 28 = 178`. — For `|X| = 25 + HSFixedData (|Fix| = 50)`, the semi-regular action of `X` on `V \ Fix(X)` (3200 vertices) yields `3200 / 25 = 128` size-25 orbits. Of these, `100` are "fix-neighbourhood" orbits (each of the 50 fixed v… Formalized done L747
  • Eq (7) arithmetic core: degree split for `v ∈ O_{178}` gives `Σb = 7`. — Each vertex `v ∈ O_{178}` (a "free" orbit) has degree `57` in Γ. The 57 neighbours decompose as: * `0` in `Fix(X)` (paper assumption: `O_{178}` not connected to Fix) * `50` in fix-N orbits (Moore graph μ=1: for each f… Formalized done L771
  • Eq (8) arithmetic core: square-sum decomposition gives `Σb² = 31`. — By Lem 5(5), `(B² + B - 56I)_{178, 178} = s_{178} = 25` (orbit size). Decomposing `(B²)_{178, 178} = Σ_l b_{178, l} · b_{l, 178}`: * `l ∈ Fix`: `b_{178, l} = 0`, contributes 0 * `l ∈ fix-N` (100 orbits, indices 51..15… Formalized done L793
  • Step 2 structural core: σ-orbit in `N(a)` is an independent set. — [done — Path B Step 2] For `σ : Equiv.Perm V` automorphism of Moore57 `Γ`, fixed vertex `a`, and `v ∈ N(a)`: any two distinct σ-iterates of `v` are non-adjacent. Equivalently, the σ-orbit `{v, σ v, σ² v, ...}` ⊆ N(a)… Formalized auto L815
  • Step 3 arithmetic core: `Tr(O) ≤ 2 ∧ even ⟹ Tr(O) ∈ {0, 2}`. — For an orbit `O` of size 25, Lem 6 (3) gives `Tr(O) ≤ 2` (X abelian, central element argument). Lem 6 (2) gives `Tr(O)` even (X has odd order). Together, `Tr(O) ∈ {0, 2}`. This is a tiny arithmetic step packaging the… Formalized done L855
  • Step 4 arithmetic core: 28 trace-2 orbits forces `2 · n_two ≢ 6 [MOD 15]`. — If we have `n_zero` trace-0 orbits and `n_two` trace-2 orbits among the 28 "free" orbits (with `n_zero + n_two = 28`), and if `2 · n_two ≡ 6 [MOD 15]` (from Lem 8 + the 100 fix-N orbits contributing 0 to trace), then… Formalized done L869
  • Step 4 arithmetic: existence of zero-trace orbit (weak form). — The weaker version of `prop3_step4_arithmetic_zero_orbit_exists`: just `n_zero ≥ 1` (matching paper's stated claim) Formalized done L886
  • Step 4 arithmetic: `n_two ∈ {3, 18}` exactly. — Strongest form: the modular + bound constraints force `n_two` to be exactly 3 or 18 (so `Tr(X) ∈ {6, 36}`) Formalized done L897
  • Proposition 3 Step 1-4 conclusion (abstract paper-faithful) — Steps 1-4 combined: from `|X| = 25 + HSFixedData`, produce the eq (7)+(8) witness `b : Fin 27 → ℕ` for application to `prop3_no_solution_direct`. This is a paper-faithful encoding of the deferred structural chain (Moo… Formalized auto L922
  • Proposition 3 `|X| ≠ 25` via structural Step 1-4 conclusion — [done — bridge] Combines the deferred `Proposition3Step1To4Conclusion` (witness construction) with the proven `prop3_no_solution_direct` (no-solution) to derive `orderOf σ ≠ 25` for any `σ` with `HSFixedData`. This pr… Formalized auto L988
  • Proposition 3 full bound via Steps 1-4 + 5 — [done — bridge] The final chain: given the (deferred) structural Step 1-4 conclusion, plus the proven C3.4 semi-regular orbit bridge, derive the paper's `|X| ≤ 5` bound (Proposition 3 statement) unconditionally on the… Formalized auto L1005
Mačaj–Širáň 2010, §8, Proposition 4 [GAP] — 1/1 formalized .lean
  • Proposition 4 (`SmallGroup(625, 12)` cannot act with smallest orbit 25, paper-faithful conditional) — — discharged. Replaces the prior backward-compat True-stub with a paper-faithful conditional: given the orbit-stabilizer hypothesis (which Lem 22's `lem22_arithmetic_stabilizer_25` formalises) and the GAP-deferred exc… Formalized done L41
Mačaj–Širáň 2010, §8, Proposition 5 — 23/23 formalized .lean
  • Prop 5 conditional bridge: case-by-case exclusion — Given the orbit decomposition `625·i + 125·j = 3250` (Lem 24's six configurations), the paper's exclusions: * `h_i_le_3`: row constraints exclude `i ≤ 3` (cases (0,26), (1,21), (2,16), (3,11)). * `h_i_4`: row-type + t… Formalized done L61
  • Prop 5 conditional bridge: i ≤ 4 dispatch — Variant separating the Lem 24 input (which already gives j ≥ 2, ruling out (5, 1)) and the i = 4 specific case Formalized done L80
  • Proposition 5 (paper-faithful conditional, three-case dispatch). — Proper-signature paper-faithful packaging: given the three case- exclusion hypotheses (i ≤ 3, (i = 4, j = 6), (i = 5, j = 1)) and the orbit-size equation 625·i + 125·j = 3250, conclude False. Re-export of `prop5_arith… Formalized done L103
  • Proposition 5 (paper-faithful three-case dispatch) — — discharged. Replaces the prior backward-compat True-stub with the proven `prop5_orbit_size_125_paper`: given the orbit-decomposition `625·i + 125·j = 3250` and the three case-exclusion hypotheses (i ≤ 3 contradictio… Formalized done L130
  • Prop 5 via Lem 24 (h_i_5 auto-discharged) — `prop5_orbit_size_125_paper` の `h_i_5` hypothesis を Lem 24 (`lem24_two_orbits_paper`) 経由で auto-discharge する wrapper。 paper の `(i, j) = (5, 1)` exclusion は Lem 24 の central-order-5 argument (`h_not_5_1`) として上位に押し上げる。 Formalized done L156
  • Prop 5 (j ≥ 2 form via Lem 24) — contradiction packaging matching `lem24_two_orbits_paper`'s conclusion. Same `h_not_5_1` hypothesis as `lem24_two_orbits_paper`, plus the two remaining Prop 5 case-exclusion hypotheses. Convenient for downstream wires… Formalized done L172
  • Prop 5 row arithmetic kernel, case i = 0 — For `(i, j) = (0, 26)`: no size-625 orbits, the entire row of the chosen size-125 orbit splits into 25 other-size-125 entries (all multiples of 5) plus the diagonal `b_{k,k} = 2`. Constraints (after normalization): *… Formalized done L233
  • Prop 5 row arithmetic kernel, case i = 1 — For `(i, j) = (1, 21)`: one size-625 orbit contributes `b_{k,1} = 5·q1`, and 20 other-size-125 entries (all multiples of 5) plus the diagonal. Constraints: `q1 + S = 11`, `q1² + 5·S2 = 35`, `S2 ≥ S`. `q1² ≤ 35` forces… Formalized done L252
  • Prop 5 row arithmetic kernel, case i = 2 — For `(i, j) = (2, 16)`: two size-625 orbits (`b_{k,j} = 5·q_j`, `j ∈ {1, 2}`), 15 other-size-125 entries, plus diagonal. Constraints: `q1 + q2 + S = 11`, `q1² + q2² + 5·S2 = 35`, `S2 ≥ S`. Case-split `q1, q2 ∈ {0, …,… Formalized done L271
  • Prop 5 row arithmetic kernel, case i = 3 — For `(i, j) = (3, 11)`: three size-625 orbits, 10 other-size-125 entries. Constraints: `q1 + q2 + q3 + S = 11`, `q1² + q2² + q3² + 5·S2 = 35`, `S2 ≥ S`. Case-split `q1, q2, q3 ∈ {0, …, 5}` (216 cases): every case fail… Formalized done L290
  • Prop 5 row arithmetic: combined no-solution for i ≤ 3 — For each `i ∈ {0, 1, 2, 3}`, the paper's row-config constraints (degree `Σq + S = 11`, eq (9) `Σq² + 5·S2 = 35`, basic nat inequality `S2 ≥ S`) admit no solution. This packaged form takes a single `i ≤ 3` and dispatch… Formalized done L313
  • Prop 5 i = 4 a-side enumeration for q = (2, 2, 1, 1) — For q-tuple (2, 2, 1, 1) (Σq = 6, Σq² = 10): * Σa = 5 (degree). * 5·Σa² = 25, i.e., Σa² = 5. * Bound a1 ≤ 2. Sorted a-tuples: only (1, 1, 1, 1, 1) satisfies. Yields TYPE 1 Formalized done L386
  • Prop 5 i = 4 a-side enumeration for q = (3, 2, 1, 1) — q-tuple (3, 2, 1, 1) (Σq = 7, Σq² = 15) gives Σa = 4, Σa² = 4. Sorted a-tuples: only (1, 1, 1, 1, 0) satisfies. Yields TYPE 2 Formalized done L402
  • Prop 5 i = 4 a-side enumeration for q = (3, 3, 1, 1) — q-tuple (3, 3, 1, 1) (Σq = 8, Σq² = 20) gives Σa = 3, Σa² = 3. Sorted a-tuples: only (1, 1, 1, 0, 0) satisfies. Yields TYPE 3 Formalized done L418
  • Prop 5 i = 4 a-side enumeration for q = (4, 2, 2, 1) — q-tuple (4, 2, 2, 1) (Σq = 9, Σq² = 25) gives Σa = 2, Σa² = 2. Sorted a-tuples: only (1, 1, 0, 0, 0) satisfies. Yields TYPE 4 Formalized done L434
  • Prop 5 i = 4 a-side enumeration for q = (4, 3, 2, 1) — q-tuple (4, 3, 2, 1) (Σq = 10, Σq² = 30) gives Σa = 1, Σa² = 1. Sorted a-tuples: only (1, 0, 0, 0, 0) satisfies. Yields TYPE 5 Formalized done L450
  • Prop 5 i = 4 a-side enumeration for q = (4, 3, 3, 1) — q-tuple (4, 3, 3, 1) (Σq = 11, Σq² = 35) gives Σa = 0, Σa² = 0. Forces all a_j = 0. Yields TYPE 6 Formalized done L464
  • Prop 5 i = 4 a-side rejection for the 8 non-paper q-tuples — For each q-tuple that doesn't lead to a paper type, the residual a-side constraints (Σa = X, Σa² = Y) fail with Y < X — which contradicts the basic nat inequality `Σa² ≥ Σa` (since each a_j² ≥ a_j). Aggregated: any (S… Formalized done L477
  • Prop 5 i = 4 q-tuple enumeration (sub-case q1 ≤ 3) — Sorted 4-tuples with q1 ≤ 3 and Σq² ≤ 35 and (Σq²) mod 5 = 0: fewer cases, tractable for interval_cases + omega Formalized done L509
  • Prop 5 i = 4 q-tuple enumeration (sub-case q1 = 4) Formalized done L526
  • Prop 5 i = 4 q-tuple enumeration (sub-case q1 = 5) Formalized done L541
  • Prop 5 i = 4 arithmetic enumeration: 6 row types are exhaustive — Given sorted `(q1, q2, q3, q4)` and sorted `(a1, a2, a3, a4, a5)` of non-negative integers satisfying: * `q1 + q2 + q3 + q4 + a1 + a2 + a3 + a4 + a5 = 11` (degree) * `q1² + q2² + q3² + q4² + 5·(a1² + a2² + a3² + a4² +… Formalized done L573
  • Prop 5 i = 4 dispatch via 6 row types — Given: * A row config `(q1, …, q4, a1, …, a5)` (sorted, satisfying degree + eq (9)) from the geometric extractor. * For each of the 6 paper row types, a structural contradiction (paper §8 lines 818-821). The combined… Formalized done L725
Mačaj–Širáň 2010, §8, Theorem 5 (full proof) — 5/5 formalized .lean
  • Theorem 5 (Section 8 full proof) arithmetic dispatch — Given the three-case Section 8 dispatch (Prop 3 for HS, Lem 18 (2) for pentagon, Prop 4 + Prop 5 + Lem 22 combined for empty-fix at most 125), conclude `n ∣ 125`. Directly delegates to the Section 6 `thm5_card_dvd_125… Formalized done L51
  • Theorem 5 (Section 8) 625-exclusion arithmetic — Given the empty-fix dispatch (orbit-size 25 case excluded by Lem 22 + Prop 4; orbit-size 125 case excluded by Prop 5), conclude `5^k ≠ 625`. Delegates to Section 6's `thm5_5group_not_625_from_dispatch` Formalized done L61
  • Theorem 5 (Section 8) numeric bound — The three-case Section 8 dispatch gives `|X| ≤ 125` Formalized done L69
  • Theorem 5 (paper-faithful Section-8 conditional, full bound) — — discharged. Replaces the prior backward-compat True-stub with the proven `thm5_final_paper`: given the three-case Section 8 dispatch (`n ∣ 5 ∨ n ∣ 25 ∨ n ∣ 125`), conclude `n ∣ 125 ∧ n ≤ 125`. What this discharge ca… Formalized done L93
  • Theorem 5 (paper-faithful Section-8 conditional bound). — Proper-signature paper-faithful packaging at the Section-8 level: given the three-case Section 8 dispatch (`n ∣ 5 ∨ n ∣ 25 ∨ n ∣ 125`), conclude `n ∣ 125 ∧ n ≤ 125` Formalized done L104

§9 Mixing primes

166 formalized · 5 pending · 0 out of scope · total 171

Mačaj–Širáň 2010, §9, Corollary 3 — 8/8 formalized .lean
  • Corollary 3 arithmetic core (odd order). — Given the Theorem 6 conclusion `|G| ∣ X` for some `X` in the listed odd-order maxima `{171, 39, 275, 147, 35, 375, 135}` (= `{19·9, 13·3, 5²·11, 7²·3, 7·5, 5³·3, 3³·5}`), conclude `|G| ≤ 375` (the maximum in the list) Formalized done L37
  • Corollary 3 arithmetic core (even order). — Given the Theorem 7 conclusion `|G| ∣ X` for some `X` in the listed even-order maxima `{110, 50, 54, 14, 22, 38}` (= `{11·5·2, 5²·2, 3³·2, 2·7, 2·11, 2·19}`), conclude `|G| ≤ 110` (the maximum) Formalized done L55
  • Corollary 3 unified arithmetic core (flat disjunction). — Given that `n` divides ONE of the 13 values in the union of Theorem 6 (odd-order) and Theorem 7 (even-order) lists, conclude `n ≤ 375`. This is the combined arithmetic content of `cor3_odd_arithmetic_bound` and `cor3_… Formalized done L78
  • Corollary 3 conditional bridge (parity-dispatched). — The paper-faithful conditional form: given the Theorem 6/7 divisibility conclusions dispatched by parity of `n`, conclude `n ≤ 375`, and the sharper `n ≤ 110` when `n` is even. Both branches are direct wraps of the od… Formalized done L105
  • Corollary 3 conditional from Prop-level dispatch. — A stronger conditional form taking the inputs at the Propositions 6/7/8 and Thm-7-odd-part level (one step earlier than `cor3_bound_of_thm6_thm7`). For each parity: * `h_odd_props`: if `n` is odd, then the Props 6/7/8… Formalized done L132
  • Corollary 3 via `autSubgroup` (`|Aut(Γ)| ≤ 375`). — Subgroup-level form of `aut_card_le_375_conditional`: given the Props 6/7/8 dispatch for the odd branch and the Thm 7 odd-part dispatch for the even branch — *applied to the cardinality of `Moore57.autSubgroup Γ`* — c… Formalized done L163
  • Corollary 3 (paper-faithful conditional bound). — Proper-signature paper-faithful packaging of the headline `|G| ≤ 375` / `Even → ≤ 110` bound, taking the Theorem 6/7 Prop-level dispatch as explicit input. Re-export of `cor3_bound_from_props_and_oddpart` with paper-f… Formalized done L186
  • Corollary 3 (`|Aut(Γ)| ≤ 375`, and `≤ 110` if even). — [done — Conclusion-Prop dispatched] Full paper-faithful statement of Cor 3 at the `Nat.card (autSubgroup Γ)` level, taking the §9 Theorem 6 (odd-order) and Theorem 7 (even-order) abstract Conclusion-Prop encodings as… Formalized auto L214
Mačaj–Širáň 2010, §9, Lemma 25 — 7/7 formalized .lean
  • Lemma 25 (X-action on `Fix(P)` for `P ◁ X`). — For any subgroup `X ≤ Equiv.Perm V` contained in the normaliser of `P` (equivalently, `P ◁ X`), every `g ∈ X` restricts to a permutation of `MulAction.fixedPoints P V` Formalized done L39
  • Lemma 25 (P acts trivially on `Fix(P)`). — Composed with `lem25_x_acts_on_fixedPoints`, this shows the X-action factors through `X ⧸ P` Formalized done L50
  • Lemma 25 (X-action is by graph automorphisms). — If every element of `X` is a graph automorphism of `Γ`, then the restricted X-action on `Fix(P)` is also by graph automorphisms (of the induced subgraph) Formalized done L68
  • Lemma 25 (Q acts on `Fix(P)` for `P ◁ X`, `Q ≤ X`). — The paper-faithful "Q acts on Fix(P)" form: given any subgroup `Q ≤ X` with `P ◁ X` (encoded as `X ≤ N(P)`), each `q ∈ Q` restricts to a permutation of `MulAction.fixedPoints P V`. Direct specialization of `lem25_x_ac… Formalized done L90
  • Lemma 25 (Q acts by graph automorphisms on `Fix(P)`). — If every `g ∈ X` is a graph automorphism, and `Q ≤ X`, then each `q ∈ Q` restricts to a graph automorphism of the induced subgraph on `Fix(P)` Formalized done L103
  • Lemma 25 (paper-faithful, conditional Q-action on `Fix(P)`). — Proper-signature paper-faithful packaging: given a P-normalizing X ⊆ G and a subgroup Q ≤ X, the Q-action on `Fix(P)` (via `lem25_q_acts_on_fixedPoints`) is by graph automorphisms. Re-export of `lem25_q_action_isGraph… Formalized done L124
  • Lemma 25 (normal Sylow ⇒ action on `Fix(P)`). — [done — delegates to `_paper`] The paper-faithful "Q acts on Fix(P) by graph automorphisms" content, upgraded from the prior `True := by trivial` stub. Direct re-export of `lem25_normal_sylow_action_paper` with the sa… Formalized auto L143
Mačaj–Širáň 2010, §9, Lemma 26 — 11/11 formalized .lean
  • Lemma 26 arithmetic enumeration (ordered pairs) — If `p, q` are both in the Moore57 large-prime set `{7, 11, 13, 19}` and `p < q`, then `(p, q)` is one of the six lexicographic pairs. Pure omega-decidable enumeration Formalized auto L55
  • Lemma 26 contrapositive: large-prime membership from `¬(p ≤ 5 ∨ q ≤ 5)` — If both `p, q` are odd primes in the Moore57 prime set `{3, 5, 7, 11, 13, 19}`, distinct, and neither is `≤ 5`, then both are in `{7, 11, 13, 19}`. Pure arithmetic Formalized auto L69
  • Lemma 26 conditional: paper's geometric reduction to `{p, q} = {7, 19}` — This is the abstract content of the paper's Lemma 26 argument: given that both `p` and `q` are in the large-prime set `{7, 11, 13, 19}` (so neither is `≤ 5`), and given the paper's "Sylow + Lemma 19 normality + Fix-sh… Formalized auto L92
  • Lemma 26 conditional: `(p, q) = (7, 19)` excluded via Lem 12 starred row — The geometric content of the (p, q) = (7, 19) configuration after the paper's normal-Sylow reduction is: an order-7 graph automorphism `σ` fixing some vertex `c` and all of its 57 neighbours (the `a₀ = 58 = 1 + 57` st… Formalized auto L123
  • Lemma 26 conditional combined (paper-faithful) — The full conditional structure of Lemma 26's proof: * Take as hypothesis the paper's geometric reduction (Sylow + Lemma 19 normality + Fix-shape compatibility) which, for `p, q ∈ {7, 11, 13, 19}` distinct with `p < q`… Formalized auto L147
  • Lemma 26 (paper-faithful conditional, p ≤ 5 ∨ q ≤ 5). — Re-export of `lem26_conditional_combined` with paper-faithful naming. Given: * Moore57 prime pair `p, q ∈ {3,5,7,11,13,19}` with `p < q`, * Paper geometric reduction `h_paper_geom` excluding all (p,q) pairs except (3,… Formalized done L181
  • Lemma 26 fully unconditional — for any σ ∈ Aut(Γ) of order `pq` with `p, q ∈ {3, 5, 7, 11, 13, 19}` distinct odd primes (`p < q`), `p ≤ 5 ∨ q ≤ 5`. The proof case-splits on the 6 possible pairs with `p, q > 5` and discharges each via the correspond… Formalized auto L240
  • Lemma 26 group form (thin wrapper). — Given a subgroup `X ≤ autSubgroup Γ` and an element `σ ∈ X` (viewed in `Equiv.Perm V`) with `orderOf σ = p · q` for distinct primes `p, q ∈ {3, 5, 7, 11, 13, 19}` (`p < q`), conclude `p ≤ 5 ∨ q ≤ 5`. Re-export of `lem… Formalized done L335
  • Lemma 26 group form (paper-faithful, direct product extraction). — Given a subgroup `X ≤ autSubgroup Γ` of order `p^a · q^b` for distinct primes `p < q` in `{3, 5, 7, 11, 13, 19}`, plus the paper's structural hypothesis "both Sylow subgroups `P` (of order `p^a`) and `Q` (of order `q^… Formalized done L398
  • Lemma 26 group form — abstract Conclusion Prop. — Packages the paper's full group-form claim "|X| = p^a · q^b ⟹ p ≤ 5 ∨ q ≤ 5" as a deferred-hypothesis Prop. The deferred content is the Sylow + Lemma 19 argument that forces both Sylow subgroups to be normal and disjo… Formalized auto L453
  • Lemma 26 (`p ≤ 5` or `q ≤ 5`). — [done — fully unconditional via Lem 15 closures] Proper-signature upgrade of the prior `True := by trivial` stub, delegated to the fully unconditional element-level form `lem26_small_prime_unconditional` (which case-s… Formalized auto L473
Mačaj–Širáň 2010, §9, MainTheorem (Plan B extended dispatch) — 9/9 formalized .lean
  • Cor 3 2-prime branch divisibility via per-Prop Conclusions. — Given the combined `TwoPrimeMixingCaseDispatch Γ` (which packages Props 6/7/8 case structures and the underlying card hypothesis), plus the per-Prop abstract Conclusions `Proposition{6,7,8}Conclusion Γ`, conclude that… Formalized done L528
  • Cor 3 odd-branch dispatch via per-Prop Conclusions (odd-`|Aut(Γ)|` form). — Specialisation of `cor3_odd_dispatch_dvd_via_per_prop_conclusions` to the odd-card case, packaged in the same shape as `Cor3OddDispatchConclusion Γ` under the additional hypothesis `Odd (Nat.card (autSubgroup Γ)) → Tw… Formalized done L566
  • Prop 6 case dispatch arithmetic bound (direct form) — Given `Prop6CaseDispatch a b` (the paper's case (1) ∨ case (2) arithmetic content for `(p, q) = (3, 5)`) and positivity `a, b ≥ 1`, conclude `3^a · 5^b ≤ 375`. This is the **pure-arithmetic** discharge of the Prop 6 b… Formalized done L757
  • Prop 7 case dispatch arithmetic bound (direct form) — Given `Prop7CaseDispatch a b q` (the paper's per-`q` arithmetic content for `(p, q) = (3, q)` with `q ∈ {7, 13, 19}`) and positivity `a, b ≥ 1`, conclude `3^a · q^b ≤ 171` Formalized done L768
  • Prop 8 case dispatch arithmetic bound (direct form) — Given `Prop8CaseDispatch a b q` (the paper's per-`q` arithmetic content for `(p, q) = (5, q)` with `q ∈ {7, 11}`) and positivity `a, b ≥ 1`, conclude `5^a · q^b ≤ 275` Formalized done L779
  • Combined 2-prime mixing arithmetic bound from `TwoPrimeMixingCaseDispatch` — without `IsMoore57`. A `IsMoore57`-free variant of `aut_card_le_375_via_2_prime_mixing_holds_partial`: given only the `TwoPrimeMixingCaseDispatch V Γ` input, conclude `Nat.card (autSubgroup Γ) ≤ 375`. The arithmetic d… Formalized done L796
  • Constructor: Prop 7 case dispatch via Sylow q normality + paper bounds Formalized done L838
  • Constructor: Prop 8 case dispatch via Sylow q normality + paper bounds Formalized done L848
  • Theorem 7 even-order case dispatch (Conclusion Prop encoding) — For `Γ` with `|Aut(Γ)|` even, encodes the paper's Thm 7 conclusion that the odd part `m = |Aut(Γ)| / 2` divides one of `{55, 25, 27, 7, 11, 19}`, i.e., `|Aut(Γ)| = 2 · m` for some such `m`. Conclusion-Prop encoding pa… Formalized auto L910
Mačaj–Širáň 2010, §9, Proposition 6 — 19/20 formalized, 1 pending .lean
  • Proposition 6 case (1) arithmetic: `P ◁ X` ⇒ `|X| ∣ 135`. — For the `P ◁ X` case, the paper gives `|Q| = 5` and `|P| = 3^a` with `a ∈ {1, 2, 3}` (Lemma 17 cases: Petersen-fix `a ≤ 3` or singleton-fix `a ≤ 4`; the latter is excluded for this case by the Petersen fix shape force… Formalized done L47
  • Proposition 6 case (2) arithmetic: `P ⋪ X` ⇒ `|X| ∣ 375`. — For the `P ⋪ X` case, the paper gives `|P| = 3` and `|Q| = 5^b` with `b ∈ {2, 3}` (the cases `Q ∈ {Z₂₅, Z₁₂₅, Z₂₅ · Z₅}` of paper Lem 18, all of order `25` or `125`). So `|X| = 3 · 5^b ∈ {75, 375}`, all dividing `375… Formalized done L62
  • Proposition 6 combined arithmetic: `|X| ∣ 135 ∨ |X| ∣ 375`. — The two cases of Prop 6 combine to give the Cor 3 odd-list pair `{135, 375}`: * Case (1) `P ◁ X`: `|X| ∈ {15, 45, 135}`, all `∣ 135 = 3³ · 5`. * Case (2) `P ⋪ X`: `|X| ∈ {75, 375}`, all `∣ 375 = 3 · 5³` Formalized done L75
  • Proposition 6 Sylow arithmetic core: `n₅ = 1` from Sylow's third for `|X| = 3^a · 5^b` with `a ≤ 3` — This is the **Feit–Thompson-free** dispatch step for Prop 6. Given a 3-power `3^a ∣ 27` (i.e., `a ≤ 3`) and a count `n₅ ∣ 3^a` with `n₅ ≡ 1 (mod 5)` (the Sylow's-third-theorem conclusion for any group of order `3^a ·… Formalized done L107
  • Proposition 6 Sylow arithmetic core (parametric `a ≤ 3`) — Same as `prop6_sylow5_count_one_of_3pow_dvd_27` but with the 3-power exponent `a ≤ 3` as a parameter. Covers the entire Prop 6 case table where `a ∈ {1, 2, 3}` and `b ≥ 1` Formalized done L123
  • Proposition 6 Sylow-level conclusion: Sylow 5 is unique in `X` — For any finite group `X` with `Nat.card X = 3^a · 5^b` (`a ≤ 3`, `b ≥ 1`), Sylow's third theorem combined with the arithmetic gives that there is exactly one Sylow 5-subgroup, hence (by Mathlib `Sylow.normal_of_subsin… Formalized done L148
  • Proposition 6 Sylow-level: `Nat.card (Sylow 5 X) = 1` from arithmetic hypothesis — The Mathlib-level lift of `prop6_sylow5_count_one_of_3pow_a_le_three`: given a finite group `X` whose Sylow 5-subgroup count divides `3^a` for some `a ≤ 3` (which holds whenever `|X| = 3^a · 5^b` with `a ≤ 3`), the nu… Formalized done L170
  • Proposition 6 Sylow-level: `Subsingleton (Sylow 5 X)` — from arithmetic. The Subsingleton version of `prop6_sylow5_card_eq_one`, which serves as the immediate input to `Sylow.normal_of_subsingleton`. Together they give the paper's "`Q ◁ X`" conclusion of Prop 6 from Sylow'… Formalized done L188
  • Proposition 6 Sylow-level: `Sylow 5 X` is normal — (the paper's `Q ◁ X`). The full chain: arithmetic hypothesis `n₅ ∣ 3^a, a ≤ 3` ⟹ `Subsingleton (Sylow 5 X)` ⟹ Sylow 5-subgroup is normal in `X`. This is the **Feit–Thompson-free** proof of the paper's "`Q ◁ X`" claim… Formalized done L206
  • Proposition 6 (paper-faithful conditional dispatch). — Proper-signature wrapper for the paper's two-case `|X| ∣ {135, 375}` classification: given the case dispatch (case (1) `P ◁ X` with `a ≤ 3, b = 1` or case (2) `P ⋪ X` with `a = 1, 2 ≤ b ≤ 3`) as input, conclude `|X| ∈… Formalized done L225
  • Proposition 6 (`(p, q) = (3, 5)` classification). — The arithmetic backbone for both cases is captured by `prop6_case1_card_dvd_135` / `prop6_case2_card_dvd_375` / `prop6_card_dvd_135_or_375` / `prop6_3_and_5_paper` (above). The Feit–Thompson-free Sylow dispatch step i… Pending deferred L242
  • Prop 6 case dispatch constructor (case 1: P normal, b = 1) — The paper's case (1) input `(a ≤ 3 ∧ b = 1)` constructs the `Prop6CaseDispatch a b` Prop via the left disjunct. Mirror of `prop6_case1_card_dvd_135` at the Prop level Formalized done L276
  • Prop 6 case dispatch constructor (case 2: P not normal, a = 1) — The paper's case (2) input `(a = 1 ∧ 2 ≤ b ∧ b ≤ 3)` constructs the `Prop6CaseDispatch a b` Prop via the right disjunct Formalized done L285
  • Prop 6 case dispatch arithmetic bound: `3^a · 5^b ≤ 375` — Given the `Prop6CaseDispatch a b` arithmetic content (the paper's case (1) ∨ case (2) bounds on `(a, b)`) and positivity, conclude the bound `3^a · 5^b ≤ 375`. This is the **direct-arithmetic discharge** of the `Prop6… Formalized done L304
  • Prop 6 case dispatch arithmetic bound (case 1 refinement: `≤ 135`) — Tighter bound for the `Prop6CaseDispatch` case (1) branch: `3^a · 5 ≤ 135` when `a ≤ 3`, by `Nat.le_of_dvd` on `prop6_case1_card_dvd_135` Formalized done L317
  • Prop 6 case dispatch arithmetic bound (case 2 refinement: `≤ 375`) — Tighter bound for the `Prop6CaseDispatch` case (2) branch: `3 · 5^b ≤ 375` when `2 ≤ b ≤ 3`, by `Nat.le_of_dvd` on `prop6_case2_card_dvd_375` Formalized done L327
  • Proposition 6 abstract Conclusion Prop. — For any subgroup `X ≤ autSubgroup Γ` whose card is `3^a · 5^b` (with `a, b ≥ 1`), `|X| ∣ 135 ∨ |X| ∣ 375`. Encodes the paper's full Prop 6 claim as a `Prop` def; downstream takes this as deferred input, discharged via… Formalized done L359
  • Bridge: `Prop6CaseDispatch a b` ⇒ `Proposition6Conclusion` — (per-card). Given the per-card `Prop6CaseDispatch` arithmetic dispatch (which is the output of the paper's geometric case analysis), conclude the divisibility disjunction at any subgroup-level card matching `3^a · 5^b… Formalized done L374
  • Lift universal `Prop6CaseDispatch` ⇒ `Proposition6Conclusion`. — Given a function producing `(a ≤ 3 ∧ b = 1) ∨ (a = 1 ∧ 2 ≤ b ∧ b ≤ 3)` for every (a, b) with `1 ≤ a, 1 ≤ b` and `Nat.card X = 3^a · 5^b`, derive the per-subgroup `Proposition6Conclusion Γ`. This is the "lifted" versio… Formalized done L402
  • Proposition 6 — `via_conclusion` form (paper-faithful unconditional). — Given `Proposition6Conclusion Γ` (the paper's abstract Prop 6 claim) and a subgroup `X ≤ autSubgroup Γ` with `|X| = 3^a · 5^b`, conclude `|X| ∣ 135 ∨ |X| ∣ 375`. This is the **unconditional via-Conclusion form** of Pr… Formalized done L424
Mačaj–Širáň 2010, §9, Proposition 7 — 16/17 formalized, 1 pending .lean
  • Proposition 7 arithmetic enumeration (combined card list) — Given the paper's per-case structural input for `p = 3, q > 5`: * `q = 7`: `|P| = 3` and `|Q| ∈ {7, 49}` (Lem 19 cases 4/5). * `q = 13`: `|P| = 3` and `|Q| = 13` (Lem 19 case 1). * `q = 19`: `|P| ∈ {3, 9}` and `|Q| =… Formalized done L41
  • Proposition 7 arithmetic divisibility (Cor 3 odd-list form) — The Prop 7 cases all give `|X|` that divides one of the Thm 6 odd-list maxima `{147, 39, 171}`: * `q = 7` cases (`|X| ∈ {21, 147}`): both divide `147`. * `q = 13` case (`|X| = 39`): divides `39`. * `q = 19` cases (`|X… Formalized done L72
  • Proposition 7 Sylow arithmetic for `q = 7`: `n₇ = 1` from `n₇ ∣ 3 ∧ n₇ ≡ 1 (mod 7)` — For `|X| = 3 · 7^b` (Prop 7 case `q = 7, a = 1`), Sylow's third gives `n₇ ∣ 3` and `n₇ ≡ 1 (mod 7)`. Divisors of 3: `{1, 3}`; only `1 ≡ 1 (mod 7)` (3 mod 7 = 3 ≠ 1). Hence `n₇ = 1` and Sylow 7 is normal Formalized done L100
  • Proposition 7 Sylow arithmetic for `q = 13`: `n₁₃ = 1` from `n₁₃ ∣ 3 ∧ n₁₃ ≡ 1 (mod 13)` — For `|X| = 3 · 13` (Prop 7 case `q = 13`, `a = b = 1`). Divisors of 3: `{1, 3}`; only `1 ≡ 1 (mod 13)` (3 mod 13 = 3 ≠ 1) Formalized done L111
  • Proposition 7 Sylow arithmetic for `q = 19`: `n₁₉ = 1` from `n₁₉ ∣ 9 ∧ n₁₉ ≡ 1 (mod 19)` — For `|X| = 3^a · 19` (Prop 7 case `q = 19, a ≤ 2`). Divisors of 9: `{1, 3, 9}`; only `1 ≡ 1 (mod 19)` (3 mod 19 = 3, 9 mod 19 = 9, both ≠ 1) Formalized done L123
  • Proposition 7 unified Sylow arithmetic: `n_q = 1` for `q ∈ {7, 13, 19}` — Combines the three q-case arithmetic lemmas into a single dispatch. Hypothesis form: `n_q ∣ 3^a` (with `a ≤ 1` for q ∈ {7, 13}, `a ≤ 2` for q = 19) and `n_q ≡ 1 (mod q)` Formalized done L135
  • Proposition 7 Sylow-level: `Sylow q X` is normal for q ∈ {7, 13, 19} — The Mathlib-level lift of `prop7_q*_sylow*_count_one`: given a finite group `X` whose Sylow q-subgroup count divides the appropriate 3-power (3 for q ∈ {7, 13}, 9 for q = 19), Sylow's third forces uniqueness, hence no… Formalized done L170
  • Proposition 7 (paper-faithful conditional dispatch). — Proper-signature wrapper for the paper's per-`q` `|X| ∣ {147, 39, 171}` classification. Given the case dispatch (q ∈ {7, 13, 19} with appropriate (a, b) constraints) as input, conclude `|X| ∈ {divisors of 147 ∨ 39 ∨ 1… Formalized done L221
  • Proposition 7 (`(p, q) = (3, large)` classification). — The arithmetic content of the case-by-case `|X|` enumeration is captured by `prop7_card_enumeration` and the Cor 3 bridge by `prop7_card_dvd_147_39_or_171` / `prop7_3_and_large_paper` (above). The Feit–Thompson-free S… Pending deferred L242
  • Prop 7 case dispatch constructor (q = 7 branch) Formalized done L269
  • Prop 7 case dispatch constructor (q = 13 branch) Formalized done L276
  • Prop 7 case dispatch constructor (q = 19 branch) Formalized done L283
  • Prop 7 case dispatch arithmetic bound: `3^a · q^b ≤ 171` — Given the `Prop7CaseDispatch a b q` arithmetic content (per-`q` bounds for `q ∈ {7, 13, 19}`) and positivity, conclude `3^a · q^b ≤ 171`. Direct-arithmetic discharge (no `Nat.card` hypothesis). Pairs with `prop7_card_… Formalized done L298
  • Proposition 7 abstract Conclusion Prop. — For any subgroup `X ≤ autSubgroup Γ` whose card is `3^a · q^b` (with `a, b ≥ 1` and `q ∈ {7, 13, 19}`), `|X| ∣ 147 ∨ |X| ∣ 39 ∨ |X| ∣ 171`. Encodes the paper's full Prop 7 claim as a `Prop` def; downstream discharges… Formalized done L325
  • Bridge: `Prop7CaseDispatch a b q` ⇒ Proposition 7 divisibility — (per-card). Given the per-card `Prop7CaseDispatch` arithmetic dispatch (per-`q` `(a,b)` bounds for `q ∈ {7, 13, 19}`), conclude the divisibility triple-disjunction at any subgroup-level card matching `3^a · q^b` Formalized done L338
  • Lift universal `Prop7CaseDispatch` ⇒ `Proposition7Conclusion`. Formalized done L354
  • Proposition 7 — `via_conclusion` form (paper-faithful unconditional). — Given `Proposition7Conclusion Γ` and a subgroup `X ≤ autSubgroup Γ` with `|X| = 3^a · q^b` (`q ∈ {7, 13, 19}`), conclude `|X| ∣ 147 ∨ |X| ∣ 39 ∨ |X| ∣ 171`. Replaces the True-stub `prop7_3_and_large` when `Proposition… Formalized done L375
Mačaj–Širáň 2010, §9, Proposition 8 — 16/17 formalized, 1 pending .lean
  • Proposition 8 case `q = 7` arithmetic: `|X| = 35`. — For the `q = 7` case, the paper gives `P ◁ X` and `|X| = 35 = 5 · 7`. This corresponds to `a = b = 1` in the standing `|X| = 5^a · 7^b` notation Formalized done L36
  • Proposition 8 case `q = 11` arithmetic: `|X| ∣ 275`. — For the `q = 11` case, the paper gives `|P| = 5^a` with `a ∈ {1, 2}` (Lemma 18 cases 1/2: HS-fix `a ≤ 2` or pentagon-fix `a ≤ 1`) and `|Q| = 11` (Lemma 19 case 3). So `|X| = 5^a · 11 ∈ {55, 275}`, both dividing `275 =… Formalized done L45
  • Proposition 8 combined arithmetic: `|X| ∣ 35 ∨ |X| ∣ 275`. — The two cases of Prop 8 combine to give the Cor 3 odd-list pair `{35, 275}`: * `q = 7` case: `|X| = 35 ∣ 35`. * `q = 11` cases: `|X| ∈ {55, 275}`, all `∣ 275 = 5² · 11`. This is the bridge from Prop 8 to the Cor 3 ari… Formalized done L61
  • Proposition 8 Sylow arithmetic for `q = 7`: both `n₅ = 1` and `n₇ = 1` — For `|X| = 5 · 7` (Prop 8 case `q = 7`, `a = b = 1`): * `n₇ ∣ 5` and `n₇ ≡ 1 (mod 7)`: divisors of 5 are `{1, 5}`; only `1` is `≡ 1 (mod 7)` (5 mod 7 = 5). Hence `n₇ = 1` and Q is normal. * `n₅ ∣ 7` and `n₅ ≡ 1 (mod 5… Formalized done L86
  • Proposition 8 Sylow arithmetic for `q = 7` (P-side): `n₅ = 1` from `n₅ ∣ 7 ∧ n₅ ≡ 1 (mod 5)` Formalized done L94
  • Proposition 8 Sylow arithmetic for `q = 11`: `n₁₁ = 1` from `n₁₁ ∣ 5^a ∧ n₁₁ ≡ 1 (mod 11)` with `a ≤ 2` — For `|X| = 5^a · 11` (Prop 8 case `q = 11`, `a ∈ {1, 2}`). Divisors of 25 (`a = 2` worst case): `{1, 5, 25}`; only `1 ≡ 1 (mod 11)` (5 mod 11 = 5, 25 mod 11 = 3, both ≠ 1) Formalized done L106
  • Proposition 8 unified Sylow arithmetic: `n_q = 1` for `q ∈ {7, 11}` — Combines the q-case arithmetic lemmas into a single dispatch. Hypothesis form: `n_q ∣ 5^a` (with `a ≤ 1` for q = 7, `a ≤ 2` for q = 11) and `n_q ≡ 1 (mod q)` Formalized done L118
  • Proposition 8 Sylow-level: `Sylow q X` normal for q ∈ {7, 11} — Lifts of `prop8_q*_sylow*_count_one` to Mathlib `Sylow.Normal`. - q = 7: `n₇ ∣ 5 ⟹ n₇ = 1 ⟹ Subsingleton ⟹ Normal`. - q = 11: `n₁₁ ∣ 25 ⟹ n₁₁ = 1 ⟹ Subsingleton ⟹ Normal`. - q = 7 (P-side): `n₅ ∣ 7 ⟹ n₅ = 1 ⟹ Subsingl… Formalized done L145
  • Proposition 8 (paper-faithful conditional dispatch). — Proper-signature wrapper for the paper's two-`q` `|X| ∣ {35, 275}` classification. Given the case dispatch (q ∈ {7, 11} with appropriate (a, b)) as input, conclude `|X| ∈ {divisors of 35 ∨ 275}`. The geometric content… Formalized done L195
  • Proposition 8 (`(p, q) = (5, large)` classification). — The arithmetic backbone for both cases is captured by `prop8_q7_card_eq_35` / `prop8_q11_card_dvd_275` / `prop8_card_dvd_35_or_275` / `prop8_5_and_large_paper` (above). The Feit–Thompson-free Sylow dispatch giving `Q… Pending deferred L215
  • Prop 8 case dispatch constructor (q = 7 branch) Formalized done L242
  • Prop 8 case dispatch constructor (q = 11 branch) Formalized done L248
  • Prop 8 case dispatch arithmetic bound: `5^a · q^b ≤ 275` — Given the `Prop8CaseDispatch a b q` arithmetic content (per-`q` bounds for `q ∈ {7, 11}`) and positivity, conclude `5^a · q^b ≤ 275`. Direct-arithmetic discharge (no `Nat.card` hypothesis). Pairs with `prop8_card_dvd_… Formalized done L262
  • Proposition 8 abstract Conclusion Prop. — For any subgroup `X ≤ autSubgroup Γ` whose card is `5^a · q^b` (with `a, b ≥ 1` and `q ∈ {7, 11}`), `|X| ∣ 35 ∨ |X| ∣ 275`. Encodes the paper's full Prop 8 claim as a `Prop` def; downstream discharges via `prop8_case_… Formalized done L286
  • Bridge: `Prop8CaseDispatch a b q` ⇒ Proposition 8 divisibility — (per-card). Given the per-card `Prop8CaseDispatch` arithmetic dispatch (per-`q` `(a,b)` bounds for `q ∈ {7, 11}`), conclude the divisibility disjunction at any subgroup-level card matching `5^a · q^b` Formalized done L299
  • Lift universal `Prop8CaseDispatch` ⇒ `Proposition8Conclusion`. Formalized done L315
  • Proposition 8 — `via_conclusion` form (paper-faithful unconditional). — Replaces the True-stub `prop8_5_and_large` when `Proposition8Conclusion` is in scope Formalized done L332
Mačaj–Širáň 2010, §9, Theorem 6 — 36/37 formalized, 1 pending .lean
  • Theorem 6 disjunction from Props 6/7/8 dispatch — Given the per-case Proposition 6 / 7 / 8 arithmetic outputs as a combined hypothesis, the seven-way Theorem 6 disjunction follows by pure boolean disjunction rearrangement. The hypothesis structure mirrors the paper's… Formalized done L61
  • Theorem 6 bound `|G| ≤ 375` from Props 6/7/8 dispatch — Combines `thm6_dvd_one_of_seven_from_props` with `Nat.le_of_dvd` per branch to derive `|G| ≤ 375` directly. (`Corollary3_375Bound` imports this file, so the cleaner re-use of `cor3_unified_arithmetic_bound` is not ava… Formalized done L78
  • Theorem 6 conditional from per-case Props 6/7/8 + 1-prime input — Stronger conditional including the single-prime case dispatch. The input is the disjunction `1-prime ∨ 2-prime`, matching the paper's case split. Given either branch, conclude `|G|` divides one of the seven Theorem 6… Formalized done L106
  • Theorem 6 (paper-faithful conditional dispatch). — Proper-signature paper-faithful packaging: given the Props 6/7/8 dispatch (`n` divides one of three case-products) as input, conclude `n ∈ divisors of {171, 39, 275, 147, 35, 375, 135}` and `n ≤ 375`. The geometric co… Formalized done L135
  • Theorem 6 abstract conclusion — (Conclusion Prop encoding). For an odd integer `n` (`|Aut(Γ)|` odd), the paper dispatches `n` into one of three case-product divisibility classes: * Prop 6 case (3, 5): `n ∣ 135` or `n ∣ 375`, * Prop 7 case (3, q≥7):… Formalized auto L155
  • Theorem 6 via Conclusion encoding (paper-faithful). — Given the `Thm6OddOrderConclusion` (paper's Props 6/7/8 disjunction for odd `n`), conclude `n ≤ 375`. Delegates to `thm6_odd_order_paper` after applying the Conclusion Formalized done L166
  • Theorem 6 (odd `|Aut(Γ)|` divides one of seven values). — Arithmetic conclusion is captured by `thm6_dvd_one_of_seven_from_props` and `thm6_dvd_one_of_seven_from_props_and_one_prime` and combined in `thm6_odd_order_paper` (above). The Conclusion Prop encoding is `Thm6OddOrde… Pending deferred L184
  • Theorem 6 1-prime branch Conclusion — (Conclusion Prop encoding). For an odd integer `n` (`|Aut(Γ)|` odd), the paper's 1-prime case (Lems 16/17/18/19) gives `n ∣ p^k` for `p ∈ {3, 5, 7, 11, 13, 19}` with `p^k ∈ {27, 125, 49, 11, 13, 19}` (Lem 4 / Lem 16 p… Formalized auto L219
  • Theorem 6 combined Conclusion (1-prime ∨ 2-prime) — Packages both Conclusion encodings into the disjunction structure expected by `thm6_dvd_one_of_seven_from_props_and_one_prime`. For each odd `n`, either the 1-prime branch fires (`n ∣ p^k` for one of the six prime-pow… Formalized done L229
  • Combined Conclusion from 1-prime Conclusion alone. — Given the 1-prime Conclusion, the combined Conclusion holds via the left disjunct (2-prime branch unused). Companion of `thm6_odd_order_conclusion_with_one_prime_of_two_prime` Formalized done L241
  • Combined Conclusion from 2-prime alone (1-prime trivially false). — Specialization: if the 2-prime Conclusion holds, the combined Conclusion holds (1-prime branch unused). Useful as a bridge from the existing `Thm6OddOrderConclusion` chain Formalized done L251
  • Theorem 6 via combined Conclusion (1-prime + 2-prime). — Given the combined `Thm6OddOrderConclusionWithOnePrime` (the paper's 1-prime ∨ 2-prime case split for odd `n`), conclude `n ≤ 375` and that `n` divides one of the seven Theorem 6 entries. Delegates to `thm6_dvd_one_of… Formalized done L264
  • Theorem 6 1-prime branch wire (Lem 19 case 3, p=11) — via σ-witness. [done — unconditional Lem 19 case 3] Given: * `IsMoore57 Γ`, * a witness σ ∈ `autSubgroup Γ` with `σ^11 = 1`, `σ ≠ 1` (the paper's "Aut(Γ) is an 11-group" input, specialised to a generator), * the cycli… Formalized auto L309
  • Theorem 6 1-prime branch wire (Lem 19 case 2, p=19) — via σ-witness. [done — unconditional Lem 19 case 2] Parallel to `thm6_one_prime_branch_card_dvd_11_via_lem19_unconditional`, for the `p = 19` case (Lem 19 case 2, singleton fix). Discharges `orderOf σ ∣ 19` via `lem19… Formalized auto L326
  • Theorem 6 1-prime branch wire (Lem 19 case 1, p=13) — via σ-witness. [done — unconditional Lem 19 case 1 via `aut_order_thirteen_EmptyFixedData_unconditional`] Parallel to the `p = 11` and `p = 19` wires, for the `p = 13` case (Lem 19 case 1, empty fix). Uses the foundat… Formalized auto L346
  • Aut order-`p` ⟹ cyclic with generator σ of `orderOf σ = p` — (helper). For prime `p`, `Nat.card (autSubgroup Γ) = p` implies the subgroup is cyclic of prime order, hence a generator σ exists with: * `σ ∈ autSubgroup Γ` (giving `smul_adj`), * `orderOf σ = p` (giving `σ ^ p = 1`… Formalized done L388
  • Theorem 6 1-prime branch wire (Lem 19 case 3, p=11) via prime card. — [done — fully unconditional cyclic-exhaust discharge] Discharges both the σ-witness hypothesis and the cyclic-exhaust hypothesis of `thm6_one_prime_branch_card_dvd_11_via_lem19_unconditional`. Hypotheses: * `IsMoore57… Formalized auto L437
  • Theorem 6 1-prime branch wire (Lem 19 case 2, p=19) via prime card. — [done — fully unconditional cyclic-exhaust discharge] Parallel to `thm6_one_prime_branch_card_dvd_11_holds_of_prime_card` for the `p = 19` case (Lem 19 case 2, singleton fix) Formalized auto L450
  • Theorem 6 1-prime branch wire (Lem 19 case 1, p=13) via prime card. — [done — fully unconditional cyclic-exhaust discharge] Parallel to `thm6_one_prime_branch_card_dvd_11_holds_of_prime_card` for the `p = 13` case (Lem 19 case 1, empty fix). No fix-emptiness hypothesis required (uses th… Formalized auto L465
  • Theorem 6 1-prime branch wire (Lem 17, p=3) via prime card and Petersen uniqueness. — [done — full Lem 17 dispatch, conditional on `PetersenUniqueness`] For `Nat.card (autSubgroup Γ) = 3`, extracts a σ-generator via `exists_aut_generator_of_prime_card` (giving `σ ≠ 1`, `σ^3 = 1`, `orderOf σ = 3`, `smul… Formalized auto L519
  • Theorem 6 1-prime branch wire (Lem 17, p=3) via prime card — unconditional. — [done — fully unconditional, no PetersenUniqueness hypothesis] Discharges the `PetersenUniqueness` hypothesis of `thm6_one_prime_branch_card_dvd_27_holds_of_prime_card_given_uniqueness` via `Moore57.petersenUniqueness… Formalized auto L562
  • Theorem 6 1-prime branch wire (Lem 18, p=5) via prime card and fix-shape dispatch. — [done — full Lem 18 dispatch, conditional on `Lemma18FixShapeDispatch`] For `Nat.card (autSubgroup Γ) = 5`, extracts a σ-generator via `exists_aut_generator_of_prime_card` (giving `σ ≠ 1`, `σ^5 = 1`, `orderOf σ = 5`,… Formalized auto L633
  • Theorem 6 1-prime branch wire (Lem 18, p=5) via prime card — unconditional. — [done — Phase 0 carryover, fully unconditional] Discharges the `h_dispatch` hypothesis of `thm6_one_prime_branch_card_dvd_125_holds_of_prime_card_given_dispatch` via the Phase 0 unconditional discharge `Moore57.Papers… Formalized auto L671
  • Theorem 6 1-prime branch wire (Lem 16, p=7) via prime card and fix-shape dispatch. — [done — full Lem 16 p=7 dispatch, conditional on `Lemma16P7FixShapeDispatch`] For `Nat.card (autSubgroup Γ) = 7`, extracts a σ-generator via `exists_aut_generator_of_prime_card` (giving `σ ≠ 1`, `σ^7 = 1`, `orderOf σ… Formalized auto L735
  • Theorem 6 1-prime branch wire (Lem 16, p=7) via prime card — unconditional. — [done — Phase 1, fully unconditional] Discharges the `h_dispatch` hypothesis of `thm6_one_prime_branch_card_dvd_343_holds_of_prime_card_given_dispatch` via the Phase 1 unconditional discharge `Moore57.Papers.MacajSira… Formalized auto L772
  • Aut card ≥ 2 ⟹ ∃ non-identity σ in autSubgroup with σ ^ n = 1 — (helper for prime-power-card wires). For `Nat.card (autSubgroup Γ) = n` with `n ≥ 2`, extract a σ ∈ autSubgroup with: * `σ ≠ 1` (from `Nontrivial` of the subgroup, since `Nat.card ≥ 2`), * `σ ^ n = 1` (from `pow_card_… Formalized done L823
  • Theorem 6 `_holds`: paper-faithful odd-order bound, 2-prime Conclusion form. — [done — `_holds` upgrade of `thm6_odd_order` True-stub, 2-prime side] Proper-signature replacement of the bare `True`-stub `thm6_odd_order` (2-prime branch only). Given: * `IsMoore57 Γ`, * `Odd n` (with `n = Nat.card… Formalized auto L896
  • Theorem 6 `_holds` aut-card form: paper-faithful odd-order bound, `IsMoore57 Γ` + autSubgroup card. — Specialisation of `thm6_odd_order_holds` to `n = Nat.card (autSubgroup Γ)`. Given: * `IsMoore57 Γ`, * `Odd (Nat.card (autSubgroup Γ))`, * `Thm6OddOrderConclusion`, conclude the autSubgroup card divides one of `{171, 3… Formalized done L919
  • Theorem 6 `_holds`: paper-faithful odd-order bound, combined 1-prime + 2-prime Conclusion form. — Stronger version of `thm6_odd_order_holds` consuming the full `Thm6OddOrderConclusionWithOnePrime` Prop encoding (combining the 1-prime Lems 16/17/18/19 branch with the 2-prime Props 6/7/8 branch). Delegates to `thm6_… Formalized done L945
  • Theorem 6 `_holds` aut-card form (combined 1-prime + 2-prime): paper-faithful odd-order bound, `IsMoore57 Γ` + autSubgroup card. — Specialisation of `thm6_odd_order_with_one_prime_holds` to `n = Nat.card (autSubgroup Γ)`. Maximal-coverage Plan B packaging of Thm 6 — consumes the combined Conclusion (1-prime ∪ 2-prime) and discharges to the seven-… Formalized done L964
  • Theorem 6 `|G| = 27` ⟹ `|G| ≤ 375` — (Lem 17 ceiling) Formalized done L1019
  • Theorem 6 `|G| = 125` ⟹ `|G| ≤ 375` — (Lem 18 ceiling) Formalized done L1025
  • Theorem 6 `|G| = 49` ⟹ `|G| ≤ 375` — (Lem 4 / Lem 16 ceiling) Formalized done L1031
  • Theorem 6 `|G| = 11` ⟹ `|G| ≤ 375` — (Lem 19 case 3 ceiling) Formalized done L1037
  • Theorem 6 `|G| = 13` ⟹ `|G| ≤ 375` — (Lem 19 case 2 ceiling) Formalized done L1043
  • Theorem 6 `|G| = 19` ⟹ `|G| ≤ 375` — (Lem 19 case 1 ceiling) Formalized done L1049
  • Theorem 6 unified 1-prime-power card dispatch (`|G| ≤ 375`). — Given `Nat.card (autSubgroup Γ) ∈ {27, 125, 49, 11, 13, 19}` (paper-deferred Lems 16/17/18/19 dispatch via Feit–Thompson + Sylow), conclude `|G| ≤ 375`. Parallels `thm7_aut_card_le_110_holds_partial` for the even-orde… Formalized done L1066
Mačaj–Širáň 2010, §9, Theorem 7 — 44/45 formalized, 1 pending .lean
  • Theorem 7 disjunction from odd-part dispatch — The paper's Thm 2 (Makhnev–Paduchikh) decomposition `G = ⟨Y, t⟩ × X` isolates the involution `t`, leaving the odd part `m = |G| / 2` constrained by the Thm 5 (5-group bound) + Lemma 15 + Lemma 12 considerations to div… Formalized done L49
  • Theorem 7 bound `|G| ≤ 110` from odd-part dispatch — Combines `thm7_dvd_one_of_six_from_odd_part` with per-branch `Nat.le_of_dvd` to derive `|G| ≤ 110` directly. The max of `{110, 50, 54, 14, 22, 38}` is `110` Formalized done L67
  • Theorem 7 odd-part bound (paper-faithful) — Combined arithmetic conclusion: if `m` is the odd part (i.e. odd divisor of `|G|`) satisfying the Thm 5 + Lem 15 + Lem 12 constraints `m ∣ 55 ∨ m ∣ 25 ∨ m ∣ 27 ∨ m ∣ 7 ∨ m ∣ 11 ∨ m ∣ 19`, then `m ≤ 55` Formalized done L85
  • Theorem 7 Sylow arithmetic for `|G| = 110 = 2·5·11`: `n₁₁ = 1` — For `|G| = 2·5·11 = 110`, Sylow's third gives `n₁₁ ∣ 10` (since `|G|/|Sylow 11| = 10`) and `n₁₁ ≡ 1 (mod 11)`. Divisors of 10: `{1, 2, 5, 10}`; only `1 ≡ 1 (mod 11)` (the others are `2, 5, 10` mod 11, all ≠ 1). Hence… Formalized done L121
  • Theorem 7 Sylow arithmetic for `|G| = 50 = 2·5²`: `n₅ = 1` Formalized done L128
  • Theorem 7 Sylow arithmetic for `|G| = 54 = 2·3³`: `n₃ = 1` Formalized done L135
  • Theorem 7 Sylow arithmetic for `|G| = 14 = 2·7`: `n₇ = 1` Formalized done L142
  • Theorem 7 Sylow arithmetic for `|G| = 22 = 2·11`: `n₁₁ = 1` Formalized done L149
  • Theorem 7 Sylow arithmetic for `|G| = 38 = 2·19`: `n₁₉ = 1` Formalized done L156
  • Theorem 7 unified Sylow dispatch (`q` Sylow normal for each even candidate order) — For each `(|G|, q)` pair in the even-order Thm 7 list with `q` the "largest" prime, `n_q = 1` forced by Sylow + mod arithmetic. This provides the Feit–Thompson-free dispatch: each even-order candidate has a unique (he… Formalized done L178
  • Theorem 7 Sylow-level: Sylow q is normal for each even-order candidate — Mathlib lifts of `thm7_card_*_sylow*_count_one`. For each candidate even order, the Sylow subgroup of the "large prime" q is normal Formalized done L200
  • Theorem 7 Sylow-level: `Sylow 5 G` normal for `|G| = 50 = 2·5²` Formalized done L216
  • Theorem 7 Sylow-level: `Sylow 3 G` normal for `|G| = 54 = 2·3³` Formalized done L232
  • Theorem 7 Sylow-level: `Sylow 7 G` normal for `|G| = 14 = 2·7` Formalized done L247
  • Theorem 7 Sylow-level: `Sylow 11 G` normal for `|G| = 22 = 2·11` Formalized done L263
  • Theorem 7 Sylow-level: `Sylow 19 G` normal for `|G| = 38 = 2·19` Formalized done L279
  • Theorem 7 (paper-faithful conditional dispatch). — Proper-signature paper-faithful packaging: given the odd-part dispatch (`m ∈ divisors of {55, 25, 27, 7, 11, 19}`) as input, conclude `|G| ∈ divisors of {110, 50, 54, 14, 22, 38}` and `|G| ≤ 110`. The geometric conten… Formalized done L301
  • Theorem 7 abstract conclusion — (Conclusion Prop encoding). For an even integer `n` (`|Aut(Γ)|` even), the paper's Thm 2 (Makhnev–Paduchikh) decomposition `G = ⟨Y, t⟩ × X` extracts the odd part `m = n / 2`, which by Thm 5 + Lems 12/15 is constrained… Formalized auto L317
  • Theorem 7 via Conclusion encoding (paper-faithful). — Given the `Thm7EvenOrderConclusion` (paper's Thm 2 + Thm 5 + Lems 12/15 odd-part dispatch for even `n`), conclude `n ≤ 110`. Delegates to `thm7_even_order_paper` after applying the Conclusion Formalized done L327
  • Theorem 7 (even `|Aut(Γ)|` divides one of six values). — Arithmetic conclusion is captured by `thm7_dvd_one_of_six_from_odd_part` and `thm7_bound_110_from_odd_part` and combined in `thm7_even_order_paper` (above). The Feit–Thompson-free Sylow dispatch is captured by the `th… Pending deferred L348
  • Theorem 7 `|G| = 110` ⟹ `|G| ≤ 110`. — [done — direct arithmetic] For `Nat.card (autSubgroup Γ) = 110`, conclude `Nat.card ≤ 110` by rewriting and `norm_num`. This is the simplest of the six Thm 7 even-order cards — provided for packaging-uniformity with t… Formalized auto L375
  • Theorem 7 `|G| = 50` ⟹ `|G| ≤ 110`. — [done — direct arithmetic] Formalized auto L381
  • Theorem 7 `|G| = 54` ⟹ `|G| ≤ 110`. — [done — direct arithmetic] Formalized auto L387
  • Theorem 7 `|G| = 14` ⟹ `|G| ≤ 110`. — [done — direct arithmetic] Formalized auto L393
  • Theorem 7 `|G| = 22` ⟹ `|G| ≤ 110`. — [done — direct arithmetic] Formalized auto L399
  • Theorem 7 `|G| = 38` ⟹ `|G| ≤ 110`. — [done — direct arithmetic] Formalized auto L405
  • Theorem 7 unified even-order card dispatch (`|G| ≤ 110`). — For `Nat.card (autSubgroup Γ)` in the Thm 7 even-order list `{110, 50, 54, 14, 22, 38}` (paper-deferred dispatch via Thm 2 Makhnev–Paduchikh + Thm 5 + Lems 12/15), conclude `|G| ≤ 110`. Parallels `aut_card_le_343_via_… Formalized done L422
  • Theorem 7 `_holds`: full paper-faithful even-order bound, Conclusion form. — [done — `_holds` upgrade of `thm7_even_order` True-stub] Replaces the bare `True`-stub `thm7_even_order` with a real arithmetic conclusion under the paper-deferred `Thm7EvenOrderConclusion` Prop encoding. Given: * `Is… Formalized auto L454
  • Theorem 7 `_holds` aut-card form: paper-faithful even-order bound, `IsMoore57 Γ` + autSubgroup card. — Specialisation of `thm7_even_order_holds` to `n = Nat.card (autSubgroup Γ)`. Given: * `IsMoore57 Γ`, * `Even (Nat.card (autSubgroup Γ))`, * `Thm7EvenOrderConclusion`, conclude the autSubgroup card divides one of `{110… Formalized done L477
  • Per-card constructor (card 14) — Nat.card = 14` produces the existential odd-part dispatch with `m = 7`. `14 = 2·7`, so `m = 7` and `m ∣ 7` (4th disjunct in the six-way odd-part dispatch) Formalized done L541
  • Per-card constructor (card 22) — Nat.card = 22` produces the existential odd-part dispatch with `m = 11`. `22 = 2·11`, so `m = 11` and `m ∣ 11` (5th disjunct) Formalized done L552
  • Per-card constructor (card 38) — Nat.card = 38` produces the existential odd-part dispatch with `m = 19`. `38 = 2·19`, so `m = 19` and `m ∣ 19` (6th disjunct) Formalized done L563
  • Per-card constructor (card 50) — Nat.card = 50` produces the existential odd-part dispatch with `m = 25`. `50 = 2·5²`, so `m = 25` and `m ∣ 25` (2nd disjunct) Formalized done L574
  • Per-card constructor (card 54) — Nat.card = 54` produces the existential odd-part dispatch with `m = 27`. `54 = 2·3³`, so `m = 27` and `m ∣ 27` (3rd disjunct) Formalized done L585
  • Per-card constructor (card 110) — Nat.card = 110` produces the existential odd-part dispatch with `m = 55`. `110 = 2·5·11`, so `m = 55` and `m ∣ 55` (1st disjunct) Formalized done L596
  • Unified 6-card disjunction constructor — from `Nat.card ∈ {14, 22, 38, 50, 54, 110}` (or-form), produce the existential odd-part dispatch suitable for `Theorem7EvenCaseDispatch V Γ`. Case-splits on the six branches and dispatches to the corresponding per-car… Formalized done L612
  • Finset-form constructor — from `Nat.card ∈ ({14,22,38,50,54,110} : Finset ℕ)`, produce the existential odd-part dispatch suitable for `Theorem7EvenCaseDispatch V Γ`. This is the Finset-form variant of `thm7_even_case_dispatch_existential_from_… Formalized done L642
  • Sigma-form variant — same as the Finset-form constructor but returns the odd-part `m` explicitly along with the witnesses, allowing direct consumption by downstream wires that want the `m` value visible (e.g., for further arithmetic). Thi… Formalized done L668
  • Per-card combined dispatcher (card 14) — produce both the six-disjunction divisibility AND the `≤ 110` bound Formalized done L718
  • Per-card combined dispatcher (card 22) Formalized done L732
  • Per-card combined dispatcher (card 38) Formalized done L746
  • Per-card combined dispatcher (card 50) Formalized done L760
  • Per-card combined dispatcher (card 54) Formalized done L774
  • Per-card combined dispatcher (card 110) Formalized done L788
  • Unified 6-card combined dispatcher — produce both the six-disjunction divisibility AND the `≤ 110` bound from any of the six even cards `{14, 22, 38, 50, 54, 110}`. Combines `thm7_even_case_dispatch_existential_from_card_or` with `thm7_even_order_paper`… Formalized done L813

Main theorem

20 formalized · 1 pending · 0 out of scope · total 21

Mačaj–Širáň 2010 — main theorem — 20/21 formalized, 1 pending .lean
  • Theorem 4 (top-level): 3-group order bounded by 27 — Given the Section 6 / Section 7 Theorem 4 dispatch (Lem 17 dispatch + Cor 2 SG(81, 9) exclusion: `n ∣ 27 ∨ n ∣ 81` with `n ≠ 81`), conclude `n ∣ 27`. Re-exports `S6.thm4_card_dvd_27_from_dispatch_and_cor2` Formalized done L45
  • Theorem 5 (top-level): 5-group order divides 125 — Given the Section 6 / Section 8 Theorem 5 dispatch (`n ∣ 5 ∨ n ∣ 25 ∨ n ∣ 125`), conclude `n ∣ 125`. Re-exports `S6.thm5_card_dvd_125_from_dispatch` Formalized done L55
  • Theorem 6 (top-level): odd `|G|` divides one of seven values — Given the Section 9 Theorem 6 Prop-level dispatch (Props 6/7/8 combined disjunction), conclude `|G|` divides one of `{171, 39, 275, 147, 35, 375, 135}`. Re-exports `S9.thm6_dvd_one_of_seven_from_props` Formalized done L65
  • Theorem 7 (top-level): even `|G|` divides one of six values — Given the Section 9 Theorem 7 odd-part dispatch (`n = 2·m` with `m` dividing one of `{55, 25, 27, 7, 11, 19}`), conclude `|G|` divides one of `{110, 50, 54, 14, 22, 38}`. Re-exports `S9.thm7_dvd_one_of_six_from_odd_part` Formalized done L81
  • Main theorem conditional — (Mačaj–Širáň 2010, Corollary 3). Given the Section 9 Cor 3 Prop-level dispatch as a conditional input (Props 6/7/8 for the odd branch; Thm 7 odd-part `{55, 25, 27, 7, 11, 19}` for the even branch), conclude: * `|n| ≤… Formalized done L97
  • Main theorem (paper-faithful conditional form, top-level). — Proper-signature paper-faithful packaging of the headline Mačaj-Širáň 2010 Corollary 3: `|G| ≤ 375` and `Even |G| → |G| ≤ 110`, given the Props 6/7/8 (odd case) + Thm 7 odd-part (even case) Prop-level dispatch. Re-exp… Formalized done L115
  • Main theorem (Mačaj–Širáň 2010, Corollary 3). — |Aut(Γ)| ≤ 375`. The unconditional form awaits the `Aut(Γ)` ↔ subgroup-of-Sym(V) bridge and the per-section geometric content (Thms 4/5, Props 6/7/8). Proper-signature conditional form is `aut_card_le_375_paper` (above) Pending deferred L132
  • Main theorem (Tier 2 via Conclusion defs) — [done — L4 plan §4.4 Tier 2] Given `IsMoore57 Γ` plus the two Conclusion-encoded dispatches (odd / even parity), conclude `|Aut(Γ)| ≤ 375` and `Even → ≤ 110`. This is the **Tier 2 partial-unconditional** form: the 2 C… Formalized auto L170
  • Main theorem via combined all-order case dispatch. — Top-level wrapper around the §9 Plan B all-order dispatch: `AllOrdersCaseDispatch V Γ` bundles either the odd-order Props 6/7/8 case dispatch or the even-order Theorem 7 case dispatch, and the §9 wire proves the Corol… Formalized done L188
  • Bridge: `Thm6OddOrderConclusion ⟹ Cor3OddDispatchConclusion` — The §9 per-theorem `Thm6OddOrderConclusion` is strictly stronger than `Cor3OddDispatchConclusion Γ` (it is `∀ n, Odd n → ...`, while the latter specializes at `n = Nat.card (autSubgroup Γ)`). Specialization gives the… Formalized done L202
  • Bridge: `Thm7EvenOrderConclusion ⟹ Cor3EvenOddPartConclusion` — Parallel to `cor3_odd_dispatch_of_thm6_conclusion`: the §9 per-theorem `Thm7EvenOrderConclusion` specializes to the `Cor3EvenOddPartConclusion Γ` at `n = Nat.card (autSubgroup Γ)` Formalized done L211
  • Main theorem (top-level via per-theorem Conclusion defs) — Same bound as `aut_card_le_375_via_conclusions`, but parameterised on the stronger §9 per-theorem `Thm6OddOrderConclusion` / `Thm7EvenOrderConclusion` encodings (which are `∀ n, ...` forms, independent of `Γ`) Formalized done L221
  • Bridge: `Thm6OnePrimeConclusion ⟹ Cor3OnePrimeConclusion` — Specialisation of the `∀ n, Odd n → ...` per-theorem encoding to `n = Nat.card (autSubgroup Γ)`. Parallel to `cor3_odd_dispatch_of_thm6_conclusion` Formalized done L269
  • Combined 1-prime + 2-prime dispatch from per-theorem encoding. — Given the combined `S9.Thm6OddOrderConclusionWithOnePrime`, specialise to `n = Nat.card (autSubgroup Γ)` and split into per-Γ `Cor3OddDispatchConclusion ∨ Cor3OnePrimeConclusion`-style content. The output flattens the… Formalized done L284
  • Main theorem via combined 1-prime + 2-prime Conclusion — Same bound as `aut_card_le_375_via_thm_conclusions`, parameterised on the combined `S9.Thm6OddOrderConclusionWithOnePrime` (which also admits the 1-prime branch) instead of the 2-prime-only `Thm6OddOrderConclusion` Formalized done L307
  • Cor 3 Lem 17 1-prime entry (`|Aut(Γ)| ≤ 27`) — unconditional. Formalized done L573
  • Cor 3 combined Lem 17 + Lem 19 1-prime entry (`|Aut(Γ)| ≤ 27`) — unconditional. — Discharges the `PetersenUniqueness` hypothesis of `aut_card_le_27_via_lems_17_19_given_uniqueness_holds_partial` via `Moore57.petersenUniqueness`. For `|Aut(Γ)| ∈ {3, 11, 13, 19}`, unconditionally yields `|Aut(Γ)| ≤ 2… Formalized done L592
  • Cor 3 Lem 18 1-prime entry (`|Aut(Γ)| ≤ 125`) — unconditional. — Single-prime `≤ 125` bound for `|Aut(Γ)| = 5`, with no dispatcher hypothesis required. Parallels `aut_card_le_27_via_lem17_holds_partial_unconditional` (p=3) for the p=5 case Formalized done L687
  • Cor 3 Lem 16 1-prime entry (`|Aut(Γ)| ≤ 343`) — unconditional. — Single-prime `≤ 343` bound for `|Aut(Γ)| = 7`, with no dispatcher hypothesis required. Parallels `aut_card_le_27_via_lem17_holds_partial_unconditional` (p=3) for the p=7 case Formalized done L833
  • Cor 3 combined Lem 17 + Lem 18 + Lem 19 → `|Aut(Γ)| ≤ 125` — unconditional modulo Lem 18 dispatch (p=5). — Discharges the `PetersenUniqueness` hypothesis of `aut_card_le_125_via_lems_17_18_19_given_uniqueness_and_dispatch_holds_partial` via `Moore57.petersenUniqueness`. Retains only the Lem 18 p=5 fix-shape dispatcher (pap… Formalized done L935
  • Cor 3 combined Lem 16 + Lem 17 + Lem 18 + Lem 19 → `|Aut(Γ)| ≤ 343` — unconditional modulo Lem 16 p=7 + Lem 18 p=5 dispatches. — Discharges the `PetersenUniqueness` hypothesis of `aut_card_le_343_via_lems_16_17_18_19_given_uniqueness_and_dispatch_holds_partial` via `Moore57.petersenUniqueness`. Retains the two remaining fix-shape dispatchers (L… Formalized done L987