Higman 1964
Finite permutation groups of rank 3
Math. Zeitschr. 86 (1964), 145–156. DOI: 10.1007/BF01111335.
92 formalized · 0 pending · 0 out of scope · total 92 · all papers · browse source on GitHub
§1 Lemma 1 — paired orbits
Higman 1964, Lemma 1 (§1, Paired orbits) — 12/12 formalized .lean
- Lemma 1 (abstract reformulation): self-paired ⇔ swap-fixed — The Moore57 framework's `IsSelfPaired` predicate (on the `orbital` quotient) is literally `swapOrbital O = O`. This restates the definition for paper-faithful clarity Formalized done L46
- Lemma 1 (diagonal instance): the diagonal orbital is always self-paired — The diagonal orbital `{(a, a)}` (more precisely, the `G`-orbit through `(a, a) ∈ Ω × Ω`) is self-paired since `(a, a).swap = (a, a)`. This is the trivial part of Lemma 1 (it holds regardless of `|G|`'s parity) Formalized done L56
- Lemma 1 (involution): pairing is an involution on the orbital quotient — The map `swapOrbital : orbital G Ω → orbital G Ω` is its own inverse. This is the structural backbone of Lemma 1: the set of orbitals splits into pairs `{O, swapOrbital O}` (size 2) and singletons (the self-paired orb… Formalized done L68
- Lemma 1 (⟸ direction, constructive): order-2 element + moved point ⟹ non-diagonal self-paired orbital — Given `τ : G` with `orderOf τ = 2` and `a : Ω` with `τ • a ≠ a`, the orbital through `(a, τ • a)` is non-diagonal and self-paired. The key computation: `τ • (a, τ • a) = (τ • a, τ² • a) = (τ • a, a)` (since `τ² = 1`),… Formalized done L83
- Lemma 1 (⟹ direction, swap-witness): non-diagonal self-paired orbital ⟹ a group element swapping the representative pair — Given a self-paired orbital `O` with representative `(a, b)`, there exists `g ∈ G` with `g • a = b` and `g • b = a`. The element `g` acts as a transposition on `{a, b}` (so its square fixes both `a` and `b`); used in… Formalized done L128
- Lemma 1 (⟹ direction, even-order conclusion): non-diagonal self-paired orbital ⟹ `|G|` even — Given a self-paired orbital `O` with non-diagonal representative `(a, b)` (`a ≠ b`), the order of any swap element `g` (with `g • a = b` and `g • b = a`) is even, hence `2 ∣ |G|` by Lagrange. Proof: `g²` fixes both `a… Formalized done L160
- Lemma 1 (Cauchy bridge): `2 ∣ |G|` ⟹ ∃ τ ∈ G with `orderOf τ = 2` — Cauchy's theorem at `p = 2`. Together with a moved-point witness (via faithfulness or an explicit `τ • a ≠ a`), this gives the reverse direction of Lemma 1: `2 ∣ |G| ⟹ ∃ non-diagonal self-paired orbital` Formalized done L209
- Lemma 1 (main form, paper-faithful packaging) — a non-diagonal self-paired orbital exists iff there is `τ ∈ G` of order 2 with a moved point. Combined with Cauchy + faithfulness (`τ ≠ 1` ⟹ ∃ a moved), this is the precise paper-faithful statement of Lemma 1. * `⟸` (… Formalized done L228
- Lemma 1 (paper conclusion, `|G|`-form) — existence of a non-diagonal self-paired orbital implies `2 ∣ |G|`. This direction is unconditional on faithfulness (the reverse direction requires Cauchy + a moved-point witness; see `lem1_non_diagonal_self_paired_iff… Formalized done L246
- Lemma 1 (paper conclusion, contrapositive) — if `|G|` is odd, then every non-diagonal orbital is **not** self-paired (so the swap involution on non-diagonal orbitals has no fixed points, pairing them up) Formalized done L258
- Lemma 1 (paper-faithful iff, conditional on faithfulness). — [done — conditional] Proper-signature paper-faithful statement of Lemma 1: `(∃ non-diagonal self-paired orbital) ↔ 2 ∣ |G|`, conditional on the moved-point witness `h_moved`: every non-trivial element of `G` has a mov… Formalized auto L279
- Lemma 1 (paired-orbit ↔ even, conditional on faithfulness) — discharged — The full paper-faithful equivalence `(∃ non-diagonal self-paired orbital) ↔ 2 ∣ |G|`, conditional on a moved-point witness for any order-2 element (i.e., faithfulness of the `G`-action on `Ω`). Replaces the prior back… Formalized done L305
§2 Lemma 2 — intersection numbers
Higman 1964, Lemma 2 (§2, Intersection numbers) — 9/9 formalized .lean
- Lemma 2 structural backbone: orbital intersection count constancy — For any group `G` acting on `Ω`, the orbital intersection count `|N_{O₁}(a) ∩ N_{O₂}(b)|` (where `N_O(a) = {c : (a, c) ∈ O}`) depends only on the orbital containing `(a, b)`, not on the specific representative. This i… Formalized done L57
- Lemma 2 arithmetic: `λ₁`, `μ₁` complement identities packaged — The standard rank-3 association-scheme identities: * `λ₁ = l − k + μ − 1` (intersection at adjacent vertices, paired orbit) * `μ₁ = l − k + λ + 1` (intersection at non-adjacent vertices, paired) are pure ℤ rearrangeme… Formalized done L72
- Lemma 2 Moore57 instance: `λ₁ = 3135` — For Moore57 with `(k, l, λ, μ) = (57, 3192, 0, 1)`: `λ₁ = l − k + μ − 1 = 3192 − 57 + 1 − 1 = 3135` Formalized done L83
- Lemma 2 Moore57 instance: `μ₁ = 3136` — For Moore57 with `(k, l, λ, μ) = (57, 3192, 0, 1)`: `μ₁ = l − k + λ + 1 = 3192 − 57 + 0 + 1 = 3136` Formalized done L90
- Lemma 2 Moore57 paired-orbit sum: `λ₁ + μ₁ = 6271` — A consistency check: `λ₁ + μ₁ = (l − k + μ − 1) + (l − k + λ + 1) = 2·(l − k) + μ + λ`. For Moore57, this gives `2·3135 + 1 = 6271` Formalized done L97
- Lemma 2 (paper-faithful conditional dispatch). — Proper-signature paper-faithful packaging: given the standard rank-3 identities `λ₁ = l - k + μ - 1` and `μ₁ = l - k + λ + 1`, the sum identity `λ₁ + μ₁ = 2l - 2k + λ + μ` holds. The geometric content (the rank-3 tran… Formalized done L111
- Lemma 2 (intersection numbers `λ, μ`) — discharged Moore57 instance — The paper's content for Moore57: with `(k, l, λ, μ) = (57, 3192, 0, 1)`, the secondary intersection numbers `(λ₁, μ₁) = (3135, 3136)` are determined by the paper's rank-3 identities `λ₁ = l - k + μ - 1`, `μ₁ = l - k +… Formalized done L130
- Lemma 2 Moore57 instance: `λ + μ = 1` (Moore57 primary intersection sum) — For Moore57 with `(λ, μ) = (0, 1)`, the primary intersection sum `λ + μ = 0 + 1 = 1` — the smallest non-trivial intersection invariant. Together with the paired sum `λ₁ + μ₁ = 6271` (see `lem2_moore57_lambda1_plus_mu1… Formalized done L144
- Lemma 2 Moore57 instance: `μ − λ = 1` (eigenvalue equation coefficient) — For Moore57 with `(λ, μ) = (0, 1)`, the difference `μ − λ = 1` appears as the linear coefficient (with sign) in the eigenvalue quadratic `x² − (λ − μ) x − (k − μ) = x² + x − 56`. This connects Lem 2's intersection num… Formalized done L154
§2 Lemma 3 — self-paired
Higman 1964, Lemma 3 (§2, Self-paired ⇔ even) — 13/13 formalized .lean
- Lemma 3 backbone: paired orbital subdegrees coincide via reverse neighborhood — If `swapOrbital O₁ = O₂` (i.e., `O₁, O₂` are paired orbitals), then for any base point `a ∈ Ω`, the reverse orbital neighborhood `{c | (c, a) ∈ O₁}` coincides with the forward orbital neighborhood `{c | (a, c) ∈ O₂}`.… Formalized done L58
- Lemma 3 backbone: subdegree is `G`-invariant — The cardinality of an orbital neighborhood `|N_O(a)|` (the "subdegree" of `O` at base point `a`) is invariant under the diagonal `G`-action: `|N_O(g•a)| = |N_O(a)|`. For a transitive `G`-action, this means the subdegr… Formalized done L77
- Lemma 3 main form (conditional) — under paired orbitals + in-deg = out-deg hypothesis (which holds under transitive + finite Ω by double counting), the two paired-orbital subdegrees coincide (`k = l` in the paper's notation). This is the conditional "… Formalized auto L98
- Lemma 3 odd-order arithmetic: `n = 2k + 1` — The paper's odd-`|G|` rank-3 conclusion: `k = l` and `n = 1 + k + l = 1 + 2k`. Packaged as a conditional identity Formalized done L113
- Lemma 3 Moore57 contrapositive: `n = 3250` is even, so no odd-order rank-3 action — For Moore57 with `n = 3250` (even), the necessary condition `n = 2k + 1` (odd) of the odd-`|G|` case *fails* — there is no `k : ℕ` with `3250 = 2k + 1`. Hence any rank-3 group acting on Moore57 has *even* order, consi… Formalized done L127
- Lemma 3 Stage A: rank 3 + odd ⟹ swap pairs non-diagonal orbitals — Conditional rank-3 packaging: three distinct orbitals `D, O₁, O₂` covering all orbitals, with `D` the diagonal at some basepoint `a₀` and `O₁, O₂` having non-diagonal representatives. Under odd `|G|` (so by Lemma 1 co… Formalized done L159
- Lemma 3 main form (k = l), conditional on in-deg = out-deg for O₁ — Combining Stage A (`lem3_swap_pairs_non_diagonal_orbitals`) with the existing in-deg = out-deg conditional (`lem3_subdegree_eq_of_paired_and_eq_in_out_deg`). Under rank-3 packaging + odd order + the in-degree = out-de… Formalized done L207
- Lemma 3 (corollary, paper-faithful) — under odd `|G|` and rank 3, the swap involution has no non-diagonal fixed points; equivalently the two non-diagonal orbitals are paired by swap. Restatement of `lem3_swap_pairs_non_diagonal_orbitals` focused on the "p… Formalized done L231
- Lemma 3 Stage B — in-degree = out-degree under transitivity + finite Ω. Paper-faithful wrap of `Moore57.orbitalNeighborhood_card_eq_orbitalReverseNeighborhood_card`: for a transitive `G`-action on `Fintype Ω` (with `Nonempty Ω`), any o… Formalized done L263
- Lemma 3 main form (unconditional) — under transitive rank-3 action on `Fintype Ω` (`Nonempty Ω`) with odd `|G|`, the two non-diagonal subdegrees coincide (`k = l` in the paper's notation). Combines Stage A (swap pairs non-diagonal orbitals — Lem 1 contr… Formalized done L279
- Lemma 3 (paper-faithful "k = l" under odd order). — Proper-signature paper-faithful packaging: given odd `|G|` + rank-3 transitive `G` action on `Ω` + the standard rank-3 orbital cover (`{diag, O₁, O₂}`), the two non-diagonal orbital subdegrees coincide: `|O₁(a)| = |O₂… Formalized done L304
- Lemma 3 (self-paired structure under parity) — discharged "k = l" form — The paper's "k = l under odd order" conclusion: under transitive rank-3 action on `Fintype Ω` (`Nonempty Ω`) with odd `|G|`, the two non-diagonal orbital subdegrees coincide (`|N_{O₁}(a)| = |N_{O₂}(a)|`). Replaces the… Formalized done L331
- Corollary to Lemma 3 (symmetry of `Δ` under even order) — discharged contrapositive form — Moore57 contrapositive: `n = 3250` is even, so there is no `k : ℕ` with `3250 = 2k + 1`. Hence the odd-`|G|` case (where `n = 2k + 1`) cannot occur for Moore57, and any rank-3 group acting on Moore57 has even order —… Formalized done L357
§2 Lemma 4 — imprimitivity
Higman 1964, Lemma 4 (§2, Imprimitivity) — 13/13 formalized .lean
- Lemma 4 Moore57 arithmetic: `58 ∤ 3250` — For Moore57 with `(n, k) = (3250, 57)`, the imprimitivity necessary condition `k + 1 = 58 ∣ n = 3250` *fails* (since `3250 = 56·58 + 2`). By the contrapositive of Lemma 4, any rank-3 group acting on a Moore57 graph (n… Formalized done L54
- Lemma 4 Moore57 arithmetic: `k = 57 ≤ l = 3192` — For Moore57 the subdegrees are `k = 57` and `l = n − 1 − k = 3192`. Trivially `k ≤ l`, satisfying the second clause of Lemma 4 (i) Formalized done L61
- Lemma 4 imprimitivity necessary condition: `k + 1 ∣ n` — The paper's necessary condition packaged: if a transitive rank-3 group satisfies the imprimitivity conditions, then `k + 1 ∣ n`. As a Lean identity this is just the hypothesis-form `h_dvd : (k + 1) ∣ n`. Contrapositiv… Formalized done L71
- Lemma 4 conditional primitive form: `k+1 ∤ n ⟹ primitive (no imprimitive case)` — The contrapositive of the imprimitivity necessary condition packaged as an `∀`-form: if a candidate "imprimitivity hypothesis form" `(k + 1) ∣ n` fails, then no imprimitivity proof of that form exists. Combined with t… Formalized done L83
- Lemma 4 Moore57 primitivity (chained) — explicit chain from `lem4_moore57_k_plus_one_not_dvd_n` through the conditional. For Moore57's `(n, k) = (3250, 57)`, the contrapositive of Lemma 4's imprimitivity necessary condition rules out the imprimitive case (a… Formalized done L95
- Lem 4 backbone: G_a ≤ G_{N_O(a)} (setwise) — The pointwise stabilizer of a base point `a` is contained in the setwise stabilizer of the orbital neighborhood `N_O(a)`. Proof: if `g • a = a`, then for any `c ∈ N_O(a)` (i.e., `⟦(a, c)⟧ = O`), `g • c ∈ N_O(g • a) =… Formalized done L120
- Lem 4 Mathlib bridge: pretransitive primitive ⟺ stabilizer maximal — Direct wrap of `MulAction.isCoatom_stabilizer_iff_preprimitive`: under a pretransitive `G`-action on a non-trivial `Ω`, primitivity is equivalent to the point stabilizer being a maximal subgroup Formalized done L165
- Lem 4 conditional form: stabilizer strict containment ⟹ ¬ primitive — If the pointwise stabilizer `G_a` is *strictly* contained in the setwise stabilizer of the orbital neighborhood `N_O(a)`, then `G_a` is not maximal (a strict superset exists — namely `G_{N_O(a)}`, modulo it being a pr… Formalized done L188
- Lem 4 (paper-faithful imprimitivity contrapositive). — Proper-signature paper-faithful form: under the strict-containment hypothesis `G_a < G_{N_O(a)}` and the properness condition `G_{N_O(a)} ≠ ⊤`, conclude `G` is not preprimitive (contrapositive of "primitive ⟹ stabiliz… Formalized done L215
- Lem 4 (imprimitivity criterion) — discharged contrapositive form — The paper's contrapositive direction (stabilizer strict containment ⟹ not preprimitive): under the strict-containment hypothesis `G_a < G_{N_O(a)}` and the properness condition `G_{N_O(a)} ≠ ⊤`, conclude `G` is not pr… Formalized done L236
- Corollary (paper-faithful Moore57 primitivity arithmetic). — Proper-signature paper-faithful form for the Moore57 instance: combining `lem4_moore57_k_plus_one_not_dvd_n` (`58 ∤ 3250`) with the Lem 4 contrapositive, any rank-3 group acting on Moore57 is **primitive**. The full g… Formalized done L254
- Corollary arithmetic: odd `n` and `(k + 1) ∣ n` ⟹ `k` even — Pure ℕ arithmetic: if `n` is odd and `(k + 1) ∣ n`, then `k` must be even. Since `n` is odd, no even number divides `n`, so `k + 1` is odd, hence `k` is even Formalized done L263
- Corollary (rank-3 of odd order is primitive) — discharged parity arithmetic — The paper's odd-order primitivity content as a pure ℕ parity identity: if `n` is odd and `(k + 1) ∣ n`, then `k` is even. Equivalently, under the odd-order rank-3 hypothesis `n = 2k + 1` (via Lem 3) combined with the… Formalized done L299
§3 Lemma 5 — block-design count
Higman 1964, Lemma 5 (§3, Block-design count) — 17/17 formalized .lean
- Lemma 5 (μl = k(k − λ − 1)) via Mathlib SRG. — The SRG-form of Higman 1964 Lemma 5: for any strongly regular graph `G : IsSRGWith n k ℓ μ` with `n > 0`, `μ * (n − k − 1) = k * (k − ℓ − 1)`. Identifying `l = n − k − 1` (degree of complement = size of second non-tri… Formalized done L60
- Lemma 5 (μl = k(k − λ − 1)) — conditional form — Given the orbital ↔ SRG bridge for a rank-3 perm group (concretely, the SRG parameters `n, k, λ, μ` arise from the orbital structure with `l = n − k − 1`), Lemma 5 follows directly from `lem5_block_design_count_srg`.… Formalized done L77
- Lem 5 rank-3 perm group form (ℤ algebraic) — from the rank-3 counting identity `λk + μl = k(k − 1)` (Higman 1964 §3, line above "Lemma 5"), deduce `μl = k(k − λ − 1)`. This is the precise paper-faithful algebraic content of Lem 5, independent of the SRG packagin… Formalized done L103
- Lem 5 paper iff form (ℤ) — the `λk + μl = k(k − 1)` counting identity is equivalent to `μl = k(k − λ − 1)` (the paper's stated form). Formalized done L112
- Lem 5 Moore57 ℤ instance via the rank-3 perm group form — for `(k, λ, μ, l) = (57, 0, 1, 3192)`, the rank-3 counting identity `0·57 + 1·3192 = 57·56` holds, so by `lem5_rank3_perm_group_form_int` we get `1·3192 = 57·(57 − 0 − 1)` Formalized done L124
- Lemma 5 (paper-faithful conditional `μl = k(k - λ - 1)`). — Proper-signature paper-faithful packaging: given an SRG `IsSRGWith n k λ μ` on `V` (the deferred orbital ↔ SRG bridge), the rank-3 paper claim `μ(n - k - 1) = k(k - λ - 1)` holds. Re-export of `lem5_block_design_count… Formalized done L173
- Lemma 5 (μl = k(k − λ − 1)) — discharged ℤ algebraic core — The paper's content as a pure ℤ algebraic identity: from the rank-3 counting identity `λk + μl = k(k − 1)` (Higman §3, line above "Lemma 5"), deduce `μl = k(k − λ − 1)`. Replaces the prior backward-compat True-stub wi… Formalized done L189
- Moore57 instance of Lemma 5. — For Moore57 = SRG(3250, 57, 0, 1): `1 * 3192 = 57 * 56` Formalized done L197
- Corollary 1 arithmetic: odd `|G|` ⟹ `λ = μ` — (the underlying equality). The standard rank-3 statement: when `|G|` is odd, the paired-orbit structure forces `λ = μ`. Combined with the rank-3 identity `μ·l = k·(k − λ − 1)` and `n = 1 + k + l`, this further gives `… Formalized done L214
- Corollary 1 Moore57 contrapositive: `λ ≠ μ` — For Moore57 with `(λ, μ) = (0, 1)`, the paired-orbit equality `λ = μ` required by odd order *fails*: `0 ≠ 1`. Hence by the contrapositive of Corollary 1, any rank-3 group acting on a Moore57 graph has *even* order. Th… Formalized done L234
- Corollary 2 arithmetic form (`μ = 0 ⇒ λ = k - 1`). — Proper-signature paper-faithful form: given the rank-3 parameter identity `λ·k + μ·l = k·(k - 1)` and `μ = 0`, conclude `λ = k - 1`. The full paper iff (`μ = 0 ⇔ G primitive and k ≤ l ⇔ λ = k − 1`) requires the rank-3… Formalized done L243
- Corollary 2 — (`μ = 0 ⇒ λ = k − 1`) — discharged arithmetic form. The paper's arithmetic content: under the rank-3 parameter identity `λ·k + μ·l = k·(k - 1)` with `μ = 0` and `k > 0`, conclude `λ = k - 1`. Replaces the prior backwa… Formalized done L261
- Corollary 3 arithmetic form (`G primitive ⇒ μ ∉ {0, k}`). — Proper-signature paper-faithful form: if `μ ≠ 0` and `μ ≠ k`, then `μ ∉ {0, k}` (as a Set). This is the disjoint form of the Cor 3 arithmetic characterization Formalized done L272
- Corollary 3 — (`G primitive ⇒ μ ∉ {0, k}`) — discharged arithmetic form. Proper-signature arithmetic form: if `μ ≠ 0` and `μ ≠ k`, then `μ ∉ {0, k}` (as a Set ℤ). Replaces the prior backward-compat True-stub with the proven `cor3_l… Formalized done L287
- Corollary 3 Moore57 instance — μ = 1 ∉ {0, 57}`. For Moore57 with `(μ, k) = (1, 57)`, the primitivity criterion `μ ∉ {0, k}` is satisfied: `1 ≠ 0` and `1 ≠ 57`. Hence any rank-3 group acting on a Moore57 graph is primitive (consistent with the Lemm… Formalized done L298
- Lemma 5 Moore57 instance (ℤ numerics): `μ · l = k · (k − λ − 1)` for `(57, 0, 1, 3192)` — The Moore57 specialization of Lemma 5's rank-3 identity: `1 · 3192 = 3192 = 57 · 56 = 57 · (57 − 0 − 1)`. This is the precise paper-faithful arithmetic witness for the Moore57 case of Lem 5 Formalized done L312
- Lemma 5 Moore57 instance: rank-3 counting identity `λk + μl = k(k − 1)` — For Moore57: `0 · 57 + 1 · 3192 = 3192 = 57 · 56 = 57 · (57 − 1)`. This is the underlying counting identity (Higman §3, line above Lem 5) that gives `μl = k(k − λ − 1)` by `lem5_rank3_perm_group_form_int` Formalized done L321
§4 Lemma 6 — two eigenvalues
Higman 1964, Lemma 6 (§4, Two eigenvalues `s, t`) — 6/6 formalized .lean
- Moore57 secondary eigenvalue arithmetic. — For Moore57 with `(λ, μ, k) = (0, 1, 57)`, the secondary eigenvalues of the adjacency matrix are roots of the quadratic `x² − (λ − μ)·x − (k − μ) = x² + x − 56`, factoring as `(x − 7)(x + 8)`. Hence the eigenvalues ar… Formalized done L50
- Lemma 6 (conditional): eigenvalue characterization via discriminant — For a rank-3 even-order block-design, the two secondary eigenvalues `s, t` are characterised by the polynomial `X² − (λ − μ)X − (k − μ) = 0`. Equivalently, an integer `x` is an eigenvalue (of multiplicity ≥ 1, besides… Formalized done L77
- Lemma 6 (paper-faithful conditional eigenvalue characterization). — Proper-signature paper-faithful form: given perfect-square discriminant `(λ - μ)² + 4(k - μ) = d²` (Lem 7 Case II hypothesis), the secondary eigenvalues `s, t` are roots of `X² - (λ - μ)X - (k - μ) = 0`, explicitly `(… Formalized done L116
- Lemma 6 (two eigenvalues `s, t`) — discharged Moore57 instance — The paper's content for Moore57: the secondary eigenvalues of the adjacency matrix are the two roots `{7, -8}` of the integer quadratic `x² + x - 56 = 0`. This is the Moore57 specialization (`(λ, μ, k) = (0, 1, 57)`)… Formalized done L132
- Lemma 6 Moore57 instance: eigenvalue sum and product (Vieta) — For Moore57 secondary eigenvalues `(s, t) = (7, -8)`: * `s + t = -1` (= λ - μ, the negation of the linear coefficient) * `s * t = -56` (= -(k - μ), the negation of the constant coefficient) These Vieta identities veri… Formalized done L146
- Lemma 6 Moore57 instance: eigenvalue difference `e = s − t = 15` — For Moore57 secondary eigenvalues `(s, t) = (7, -8)`, the difference `e := s - t = 7 - (-8) = 15`. This `e` is the integer square root of the discriminant `(λ − μ)² + 4(k − μ) = 225 = 15²` and is the key divisibility… Formalized done L156
§5 Lemma 7 — integrality cases
Higman 1964, Lemma 7 (§5, Integrality cases) — 9/9 formalized .lean
- Moore57 discriminant is a perfect square (15²). — For Moore57 with `(λ, μ, k) = (0, 1, 57)`, the discriminant `(λ − μ)² + 4(k − μ) = (−1)² + 4·56 = 1 + 224 = 225 = 15²`, placing Moore57 in Higman Lemma 7's Case II (integer eigenvalues) Formalized done L41
- Lem 7 multiplicity formula (ℤ form) — (s − t) · f₂ = −k − (n − 1) · t`. Derived from the dimension partition `f₂ + f₃ = n − 1` and the trace constraint `f₂ · s + f₃ · t = −k` via the algebraic identity `(s − t) · f₂ = (f₂ s + f₃ t) − (f₂ + f₃) · t` Formalized done L65
- Lem 7 multiplicity formula (sym ℤ form) — (t − s) · f₃ = −k − (n − 1) · s`. Same derivation as `lem7_multiplicity_formula` with the roles of `s, t` (and `f₂, f₃`) swapped Formalized done L77
- Lem 7 Moore parameter divisibility — under the integer multiplicity constraint `2 e f₂ = k(k(e + 1) − 2)`, `e` divides `k(k − 2)` Formalized done L134
- Lemma 7 (paper-faithful Moore-parameter divisibility). — Proper-signature paper-faithful form: under the rank-3 integer multiplicity constraint `2 e f₂ = k(k(e + 1) − 2)` (Moore57 specialization of Lem 7 Case II), conclude `e ∣ k(k - 2)`. Re-export of `lem7_moore_e_dvd_k_ti… Formalized done L147
- Lemma 7 (Case I / Case II structure for even `|G|`) — discharged Moore parameter content — The paper's Moore-parameter content: under the rank-3 integer multiplicity constraint `2 e f₂ = k(k(e + 1) − 2)` (Moore57 specialization of Lem 7 Case II), `e` divides `k(k - 2)`. Combined with the discriminant identi… Formalized done L164
- Lemma 7 Moore57 multiplicity instance: `(f₂, f₃) = (1729, 1520)` — For Moore57 secondary eigenvalues `(s, t) = (7, -8)` with `n = 3250`, `k = 57`, the multiplicities `(f₂, f₃)` of the two secondary eigenvalues are determined by the linear system * `f₂ + f₃ = n - 1 = 3249` (dimension… Formalized done L181
- Lemma 7 Moore57 instance: `e · f₂ = 15 · 1729 = 25935 = −k − (n − 1)·t` — For Moore57 with `(e, f₂, k, n, t) = (15, 1729, 57, 3250, -8)`, the multiplicity formula `(s − t) · f₂ = −k − (n − 1) · t` specializes to `15 · 1729 = 25935 = −57 − 3249 · (−8) = −57 + 25992 = 25935`. This is the prec… Formalized done L194
- Lemma 7 Moore57 instance: `e ∣ k(k − 2)`, witness `k(k − 2) = e · 209` — For Moore57 with `(e, k) = (15, 57)`, the Lem 7 Case II divisibility `e ∣ k(k − 2)` holds with explicit witness: `57 · 55 = 3135 = 15 · 209` Formalized done L203
§6 Theorem 1 — degree k²+1
Higman 1964, Theorem 1 (§6, Degree `k² + 1`) — 13/13 formalized .lean
- Theorem 1 Case I arithmetic core — (`k = l, n = k² + 1`, rank-3 forces `k² = 2k`). In Case I of Higman §6, `λ + 1 = μ = k/2`, so the rank-3 identity `μ·l = k·(k − λ − 1)` collapses to `l = k`. Combined with `n = k² + 1` and `n = 1 + k + l = 1 + 2k`, we… Formalized auto L84
- Theorem 1 full arithmetic conclusion — (combining Case I and Case II). Given that one of the following holds: * Case I: `n = k² + 1 = 1 + 2k` (so `k = 0` or `k = 2`); or * Case II: `4k = e² + 3` and `e² ∣ 225` (so `k ∈ {1, 3, 7, 57}`), then `k ∈ {0, 1, 2,… Formalized auto L112
- Thm 1 bridge: from `e ∣ k(k−2)` and `e² = 4k − 3`, deduce `e ∣ 15` — Proof: multiply `e ∣ k(k − 2)` by 16 to get `e ∣ 16k(k − 2)`. Substitute `4k = e² + 3` to rewrite the RHS as `e⁴ − 2e² − 15`. Then `e ∣ e⁴` and `e ∣ 2e²`, so `e ∣ (e⁴ − 2e² − 15) − (e⁴ − 2e²) = −15`, hence `e ∣ 15` Formalized done L145
- Thm 1 bridge: `e ∣ 15 ⟹ e² ∣ 225` — (ℤ form). Trivial multiplicative consequence: `e ∣ 15` ⟹ `e * e ∣ 15 * 15 = 225` Formalized done L170
- Thm 1 bridge (combined): `e ∣ k(k−2) ∧ e² = 4k − 3 ⟹ e² ∣ 225` — Composition of `theorem1_e_dvd_fifteen` and `theorem1_e_sq_dvd_225_of_e_dvd_fifteen` Formalized done L180
- Theorem 1 full (Case II, conditional) — under Moore SRG parameters (`λ = 0`, `μ = 1`, `n = k² + 1`) with Case II hypotheses (`e² = 4k − 3` perfect square, integer multiplicity condition `2 e f₂ = k(k(e + 1) − 2)`), we have `k ∈ {1, 3, 7, 57}` (ℕ form, assum… Formalized auto L213
- Theorem 1 (Higman §6, full statement) — discharged paper-faithful disjunction — A transitive rank-3 permutation group of degree `n = k² + 1` falls in Case I (`k² + 1 = 1 + 2k`) or Case II (`∃ e : ℕ, 4k = e² + 3 ∧ e² ∣ 225`) of Higman §6; the paper-faithful arithmetic disjunction concludes `k ∈ {0… Formalized done L255
- Theorem 1 (paper-faithful Case I/II disjunction). — Proper-signature paper-faithful packaging: given the Case I (`k² + 1 = 1 + 2k`) or Case II (`∃ e, 4k = e² + 3 ∧ e² ∣ 225`) arithmetic disjunction as input, conclude `k ∈ {0, 1, 2, 3, 7, 57}`. This is `theorem1_combine… Formalized done L270
- Theorem 1, Moore57 instance. — The Moore57 vertex count `n = 3250 = 57² + 1` is one of the four degrees in Higman's classification Formalized auto L280
- Theorem 1, Moore57 valence instance. — k = 57` is one of the four valences `{2, 3, 7, 57}` allowed by Theorem 1 Formalized auto L287
- Theorem 1 Moore57 Case II witness: `e² = 4k − 3` with `(e, k) = (15, 57)` — For Moore57 with `k = 57`, the Case II discriminant identity `e² = 4k − 3` holds with `e = 15`: `15² = 225 = 4 · 57 − 3`. Combined with `theorem1_e_sq_dvd_225_of_dvd_and_sq`, this discharges the input `e² ∣ 225` of `t… Formalized done L300
- Theorem 1 Moore57 instance: `e ∣ 15` with witness `15 = 15 · 1` — For Moore57's Case II witness `e = 15`, the consequence `e ∣ 15` of the bridge `theorem1_e_dvd_fifteen` holds trivially Formalized done L307
- Theorem 1 Moore57 chain (full Case II application) — from the Moore57 witnesses `e ∣ k(k − 2)` (via `15 · 209 = 3135 = 57 · 55`) and `e² = 4k − 3` (via `15² = 225 = 4·57 − 3`), conclude `e² ∣ 225`. This is the concrete Moore57 application of the bridge `theorem1_e_sq_dv… Formalized done L319