Cameron, Permutation Groups, Ch. 3
Permutation Groups, Chapter 3 (Coherent configurations)
Cambridge University Press, 1999. DOI: 10.1017/CBO9780511623677.004.
21 formalized · 0 pending · 26 out of scope · total 47 · all papers · browse source on GitHub
§3.1 Introduction
Cameron Ch.3 §3.1 — Coherent configurations (definitions) — 0/2 formalized, 2 out of scope .lean
- Definition: coherent configuration. — A coherent configuration is the data of a finite set `Ω` together with a partition `𝓡` of `Ω²` satisfying conditions (CC1)–(CC4) Out of scope out of scope L40
- Theorem 3.1 (matrix form). — `{A_1, …, A_r}` is the basis matrix set of a coherent configuration iff: * (CC1*) `Σ_i A_i = J` (all-ones). * (CC2*) A subset of `{A_i}` sums to `I`. * (CC3*) `{A_i^T}` is a permutation of `{A_i}`. * (CC4*) For each `… Out of scope out of scope L50
§3.2 Algebraic theory
Cameron Ch.3 §3.2 — Algebraic theory — 0/3 formalized, 3 out of scope .lean
§3.3 Association schemes
Cameron Ch.3 §3.3 — Association schemes — 0/5 formalized, 5 out of scope .lean
- Definition: association scheme — (commutative / symmetric variants) Out of scope out of scope L52
- Theorem 3.5(a) (commutative ⇔ multiplicity-free). Out of scope out of scope L55
- Theorem 3.5(b) (symmetric ⇔ all FS index +1). Out of scope out of scope L58
- Theorem 3.6 (distance-regular ⇒ scheme). Out of scope out of scope L61
- Theorem 3.7 (parameter monotonicity, `c_i / b_i` chains). Out of scope out of scope L64
§3.4 Algebra of schemes
Cameron Ch.3 §3.4 — Algebra of association schemes — 2/5 formalized, 3 out of scope .lean
- Theorem 3.8 (multiplicity formula). Out of scope out of scope L48
- Theorem 3.9 (`P Q = Q P = n I`). Out of scope out of scope L51
- Theorem 3.10 (Frame's condition). — The general Frame quantity `F = n · ∏ n_i / ∏ f_j` is integer; for rational eigenvalues it is a square Out of scope out of scope L57
- Theorem 3.10 (Moore57 instance). — For Moore57 the Frame quantity is `F = 3250 · 1 · 57 · 3192 / (1 · 1729 · 1520) = 225 = 15²`. This is verified by a pure-arithmetic identity `3250 · 57 · 3192 = 225 · 1729 · 1520`. The square form `225 = 15²` is expec… Formalized auto L75
- Theorem 3.10 (Moore57 Frame is a perfect square). — 225 = 15²` Formalized auto L79
§3.5 Strongly regular graphs
Cameron Ch.3 §3.5 — Strongly regular graphs (substantive) — 5/5 formalized .lean
- Theorem 3.11 (SRG diameter-two witness form). — For an SRG with `0 < μ`, any two vertices are equal, adjacent, or joined by a path of length two. This is the diameter-`≤ 2` witness form of Cameron's connected-SRG statement; the intersection-number data are exactly… Formalized done L76
- Theorem 3.12 (Moore `(k, 2)` classification, arithmetic form). — A Moore graph of diameter 2 has order `n ∈ {5, 10, 50, 3250}` and valency `k ∈ {2, 3, 7, 57}`. This is the paper's Case I/II arithmetic conclusion, packaged in Cameron's notation: assuming `n = k² + 1`, the non-degene… Formalized done L120
- Theorem 3.12 (Moore57 valence fork instance). — Moore57 sits in the `k = 57` fork of the classification — proven via `Higman1964.theorem1_moore57_valence` Formalized auto L156
- Theorem 3.12 (Moore57 order instance). — Moore57 has `n = 3250 = 57² + 1` — proven via `Higman1964.theorem1_moore57_degree` Formalized auto L164
- Theorem 3.12 (Moore57 SRG-parameter instance). — Moore57 is `IsSRGWith 3250 57 0 1`, by definition Formalized auto L171
§3.6 Hoffman–Singleton graph
Cameron Ch.3 §3.6 — The Hoffman–Singleton graph — 0/1 formalized, 1 out of scope .lean
- Hoffman–Singleton graph (existence + uniqueness). — Constructive existence (Robertson's 1969 explicit construction) is intentionally NOT formalised here: it does not feed into any Moore57 non-existence chain Out of scope out of scope L37
§3.7 Automorphisms
Cameron Ch.3 §3.7 — Automorphisms (substantive) — 13/13 formalized .lean
- Step 1 (fix set is star or Moore subgraph). — [done — Moore57 structural collapse] For an involution `g ∈ Aut(Γ)`, the paper's "fixed subgraph is a star or a Moore subgraph" dichotomy structurally collapses to the star branch in the Moore57 setting, because every… Formalized auto L98
- Step 1 (paper-faithful, Moore57 structural collapse). — Proper-signature paper-faithful packaging: in the Moore57 setting, Cameron's Step 1 alternative "fixed subgraph is a star *or* a Moore subgraph" structurally collapses to the star branch. The proof goes via `aut_invol… Formalized done L118
- Step 2 (adjacent moved ⇒ 56 fixed) — — wraps existing infrastructure. If a non-trivial involution `σ ∈ Aut(Γ)` interchanges an adjacent pair, then `|Fix(σ)| = 56`. This is exactly `aut_involution_fixedVertexCount_eq_56_of_adjacent_moved` in the Moore57Gr… Formalized auto L132
- Step 3 (fix is 56-star or 58-star, no other Moore subgraph). — [done — Moore57 structural elimination] Cameron's "58-star vs 50-Moore-subgraph" alternative (with the 50-Moore case ruled out numerically by `50 · 50 ≠ 3250 − 50`) collapses to "always 56-star" in the Moore57 setting… Formalized auto L151
- Step 3 (paper-faithful, Moore57 structural elimination). — Proper-signature paper-faithful packaging: in the Moore57 setting, the "58-star vs 50-Moore-subgraph" alternative collapses to "always 56-star", because every non-trivial involution interchanges an adjacent pair (by `… Formalized done L167
- Step 4 (character argument eliminates 58-star case). — [done — Moore57 bypass] Cameron's character integrality argument (the `−8`-eigenspace character value `−1/3` is not an algebraic integer in the `α_0 = 58, α_1 = 0, α_2 = 3192` regime) is unnecessary in the Moore57 set… Formalized auto L185
- Step 4 (Moore57 conclusion: every involution fixes exactly 56) — — wraps `aut_involution_fixedVertexCount_eq_56` unconditionally Formalized auto L193
- Step 4 (paper-faithful, Moore57 bypass of the character argument). — Proper-signature paper-faithful packaging of Cameron's Step 4: in the Moore57 setting the character integrality argument is unnecessary because Step 3's structural collapse already pins `|Fix(σ)| = 56` (the 58-star ca… Formalized done L210
- Step 5 (parity contradiction). — [done — sign-of-involution core] The Step 5 contradiction chain: if `Aut(Γ)` is vertex-transitive then `3250 ∣ |Aut(Γ)|`, so `|Aut(Γ)|` is even and contains an involution `g` with `|Fix(g)| = 56`. The non-fixed `3250… Formalized auto L230
- Theorem 3.13 (no vertex-transitive Moore57). — [proven downstream] There is no vertex-transitive automorphism group of a Moore graph of diameter 2 and valency 57. The full statement and proof live downstream as `Moore57.Papers.MacajSiran2010.S2.cor_lem2_no_vertex_… Formalized auto L279
- Theorem 3.13 (Moore57 involution-fix instance) — — wraps the unconditional `|Fix(σ)| = 56` result Formalized auto L287
- Step 5 sign lemma (Moore57 involution is an odd permutation). — Every non-trivial automorphism `σ` of Moore57 with `σ ^ 2 = 1` has `Equiv.Perm.sign σ = −1`. Proof. `aut_involution_fixedVertexCount_eq_56` gives `|Fix(σ)| = 56`. By Mathlib's `Equiv.Perm.sign_of_pow_two_eq_one`: `sig… Formalized auto L325
- Step 5 (paper-faithful sign-of-involution). — Proper-signature paper-faithful packaging of the core arithmetic of Step 5: every non-trivial Moore57 involution has odd sign (`sign σ = -1`). The Step 5 contradiction chain proceeds by combining this sign result with… Formalized done L355
§3.8 Valency bounds
Cameron Ch.3 §3.8 — Valency bounds — 0/3 formalized, 3 out of scope .lean
§3.9 Distance-transitive graphs
Cameron Ch.3 §3.9 — Distance-transitive graphs — 0/3 formalized, 3 out of scope .lean
§3.10 Multiplicity bounds
Cameron Ch.3 §3.10 — Multiplicity bounds — 0/3 formalized, 3 out of scope .lean
§3.11 Duality
§3.12 Wielandt's theorem
Cameron Ch.3 §3.12 — Wielandt's theorem — 0/1 formalized, 1 out of scope .lean
- Theorem 3.25 (Wielandt, primitive degree-`2p` non-2-transitive ⇒ rank 3). Out of scope out of scope L25
Main theorem
Cameron Ch.3 — top-level re-export — 1/1 formalized .lean
- Theorem 3.13 (no vertex-transitive Moore57) — full proven statement. — There is no vertex-transitive automorphism group of a Moore graph of diameter 2 and valency 57. Wraps `MacajSiran2010.S2.cor_lem2_no_vertex_transitive_aut`. The Section07_Automorphisms.lean version `theorem3_13_no_ver… Formalized auto L57