diff --git a/mckay-conjecture/.gitignore b/mckay-conjecture/.gitignore
index d24d644c..efc06392 100644
--- a/mckay-conjecture/.gitignore
+++ b/mckay-conjecture/.gitignore
@@ -1,4 +1,6 @@
 /.lake/
+/output/
+/tmp/
 *.olean
 *.ilean
 *.log
diff --git a/mckay-conjecture/README.md b/mckay-conjecture/README.md
index 073b2e1e..8529cc2a 100644
--- a/mckay-conjecture/README.md
+++ b/mckay-conjecture/README.md
@@ -21,6 +21,11 @@ tip of mathlib's `master` branch when the project was created on 2026-07-25.
   complex characters and the `p'`-degree condition.
 - `McKayConjecture/Statement.lean` defines the Sylow normalizer and the
   proposition `McKayConjecture.Statement`.
+- `docs/mckay_proof.tex` gives a detailed natural-language proof certificate,
+  including the exact reduction and final type-`D` theorem chain.
+- `docs/formalization_blueprint.tex` audits existing Lean coverage and divides
+  the complete formalization into named modules and compilation gates.
+- `docs/references.bib` records the primary mathematical and Lean sources.
 
 ## Build
 
@@ -29,5 +34,17 @@ lake exe cache get
 lake build
 ```
 
-The first milestone contains only the audited proposition; it does not assume
-the conjecture as an axiom or hide an unfinished proof behind `sorry`.
+To build the documents:
+
+```bash
+cd docs
+latexmk -pdf -interaction=nonstopmode -halt-on-error \
+  -outdir=../output/pdf mckay_proof.tex
+latexmk -pdf -interaction=nonstopmode -halt-on-error \
+  -outdir=../output/pdf formalization_blueprint.tex
+```
+
+The statement milestone contains only the audited proposition; it does not
+assume the conjecture as an axiom or hide an unfinished proof behind `sorry`.
+The blueprint keeps the same trust boundary: an assumed reduction theorem or
+CFSG family result is explicitly not counted as a complete formal proof.
diff --git a/mckay-conjecture/docs/formalization_blueprint.tex b/mckay-conjecture/docs/formalization_blueprint.tex
new file mode 100644
index 00000000..00ea480d
--- /dev/null
+++ b/mckay-conjecture/docs/formalization_blueprint.tex
@@ -0,0 +1,966 @@
+\documentclass[11pt]{article}
+
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage{lmodern}
+\usepackage[margin=0.9in]{geometry}
+\usepackage{microtype}
+\usepackage{amsmath,amssymb,amsthm,mathtools}
+\usepackage{booktabs}
+\usepackage{enumitem}
+\usepackage{longtable}
+\usepackage{tabularx}
+\usepackage{pdflscape}
+\usepackage{needspace}
+\usepackage{xcolor}
+\usepackage{listings}
+\usepackage{hyperref}
+\usepackage[nameinlink,noabbrev]{cleveref}
+
+\definecolor{linkblue}{HTML}{174A7E}
+\definecolor{codegray}{HTML}{F3F5F7}
+\hypersetup{
+  colorlinks=true,
+  linkcolor=linkblue,
+  citecolor=linkblue,
+  urlcolor=linkblue,
+  pdftitle={Formalization Blueprint for the McKay Equality},
+  pdfauthor={Clawristotle contributors}
+}
+\lstdefinelanguage{Lean}{
+  morekeywords={abbrev,axiom,by,class,def,deriving,else,end,example,extends,
+    false,for,forall,fun,if,import,in,inductive,instance,let,match,namespace,
+    noncomputable,opaque,open,private,protected,section,set_option,structure,
+    theorem,true,variable,where,with},
+  sensitive=true,
+  morecomment=[l]{--},
+  morecomment=[s]{/-}{-/},
+  morestring=[b]"
+}
+\lstset{
+  language=Lean,
+  basicstyle=\ttfamily\small\mdseries\upshape,
+  backgroundcolor=\color{codegray},
+  frame=single,
+  framesep=5pt,
+  columns=fullflexible,
+  keepspaces=true,
+  breaklines=true,
+  showstringspaces=false
+}
+
+\newtheorem{invariant}{Design invariant}[section]
+\newtheorem{milestone}{Milestone}[section]
+\newcommand{\Irr}{\operatorname{Irr}}
+\newcommand{\Aut}{\operatorname{Aut}}
+\newcommand{\Norm}{\operatorname{N}}
+\newcommand{\Cent}{\operatorname{C}}
+\newcommand{\Syl}{\operatorname{Syl}}
+\newcommand{\IMK}{\mathrm{iMK}}
+\newcommand{\Ad}{\mathrm{A}(d)}
+\newcommand{\Bd}{\mathrm{B}(d)}
+
+\title{\textbf{Formalization Blueprint for the McKay Equality}\\
+\large Lean 4 architecture, dependency audit, and proof obligations}
+\author{Clawristotle contributors}
+\date{July 2026}
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+This document turns the proof certificate in
+\texttt{mckay\_proof.tex} into a Lean 4 implementation plan.  It records
+the exact theorem to be delivered, the mathematical dependency graph, the
+parts already available in mathlib and public Lean repositories, the
+missing interfaces, a proposed file structure, and a sequence of
+compilation gates.  The plan deliberately distinguishes a theorem proved
+from definitions from a theorem made conditional on an unformalized
+classification result.  The latter is useful scaffolding, but it is not a
+completed formal proof of the McKay conjecture.
+\end{abstract}
+
+\clearpage
+\tableofcontents
+\clearpage
+
+\section{Deliverable and trust boundary}
+
+\subsection{The exact target}
+
+For a finite group \(G\), a prime \(p\), and a Sylow
+\(p\)-subgroup \(P\), the target is
+\[
+  |\Irr_{p'}(G)|
+  =
+  |\Irr_{p'}(\Norm_G(P))|.
+\]
+The checked Lean statement is named
+\texttt{McKayConjecture.Statement}.  Its two sides are cardinalities of
+subtypes of ordinary irreducible complex characters.  The degree is a
+natural number and the predicate ``\(p'\)-degree'' is literally
+\(\neg\,p\mid\chi(1)\).
+
+The project is pinned to mathlib commit
+\texttt{9cebae57f419f984d008f357605b2621a1d9f13b} and Lean
+\texttt{v4.33.0-rc1}.  That commit was the tip of mathlib's
+\texttt{master} branch when this package was created on 2026-07-25.
+Pinning the dependency is part of reproducibility: ``latest mathlib'' is
+a moving target and cannot be a stable build input.
+
+\subsection{What counts as completion}
+
+A final declaration counts as a formal proof only if all of the following
+hold.
+
+\begin{enumerate}
+  \item \texttt{lake build} succeeds from a fresh dependency checkout.
+  \item The proof imports only declarations with Lean terms.  In
+  particular, the reduction theorem, the family verification, and the
+  type-\(D\) theorem may not be introduced with \texttt{axiom},
+  \texttt{sorry}, \texttt{admit}, an empty \texttt{opaque} declaration,
+  or an inconsistent typeclass instance.
+  \item \texttt{\#print axioms McKayConjecture.mckay} reports no
+  project-specific assumptions.  Standard logical dependencies such as
+  quotient soundness, propositional extensionality, and classical choice
+  are acceptable when inherited from mathlib.
+  \item No file raises \texttt{maxHeartbeats}.  Long proofs are divided
+  into named lemmas and modules instead.
+  \item The exported theorem has exactly the hypotheses and conclusion of
+  \path{McKayConjecture.Statement}; it is not merely a conditional
+  theorem with the inductive McKay condition as an extra hypothesis.
+\end{enumerate}
+
+\begin{invariant}[No theorem-shaped placeholders]
+A declaration such as
+\begin{lstlisting}
+axiom all_simple_covers_satisfy_iMK : ...
+\end{lstlisting}
+would make downstream files compile but would move the entire theorem
+outside Lean's kernel-checked proof.  It is a useful way to test an
+interface on a temporary branch, never an acceptable final artifact.
+\end{invariant}
+
+\section{Semantic design of irreducible characters}
+
+\subsection{Current audited representation}
+
+The statement milestone represents an irreducible character by its class
+function and a natural degree, together with a witness that both arise
+from a simple finite-dimensional complex representation:
+
+\Needspace{14\baselineskip}
+\begin{lstlisting}
+structure IrreducibleCharacter (G : Type u) [Group G] where
+  values : G -> Complex
+  degree : Nat
+  exists_representation :
+    exists V : FDRep Complex G,
+      Simple V /\
+      V.character = values /\
+      Module.finrank Complex V = degree
+\end{lstlisting}
+
+Characters are therefore identified extensionally, rather than by an
+arbitrary choice of representation carrier.  Evaluation at the identity
+proves that equal character functions have equal degrees, so this
+representation cannot count one irreducible character twice merely
+because it has two witnesses.  The statement uses
+\texttt{Cardinal.mk}; this avoids the bad convention by which
+\texttt{Nat.card} returns zero for an infinite type before finiteness of
+the irreducible-character type has been developed.
+
+\begin{invariant}[Mathematical objects, not presentations]
+Every later indexing type must identify isomorphic irreducible
+representations.  It may use characters as functions, primitive central
+idempotents, or an explicit quotient by representation equivalence.  It
+must not count raw representation structures.
+\end{invariant}
+
+\subsection{Full character-theory layer}
+
+The proof needs considerably more than the statement.  Introduce a
+canonical class-function API with the following data and theorems.
+
+\begin{enumerate}
+  \item A finite type \(\Irr(G)\) for finite \(G\), together with an
+  equivalence between it and the current extensional wrapper.
+  \item A theorem
+  \(\chi(1)=\operatorname{finrank}_{\mathbb C} V_\chi\), expressed as a
+  positive natural cast, and a natural-valued
+  \texttt{IrreducibleCharacter.degree}.
+  \item Character inner products, irreducible orthonormality, and
+  completeness of the irreducibles.
+  \item Transport along group isomorphisms and the action of
+  \(\Aut(G)\), with proofs that degree and \(p'\)-degree are invariant.
+  \item Restriction, induction, Frobenius reciprocity, constituents, and
+  integrality/nonnegativity of multiplicities.
+  \item Clifford theory for \(N\trianglelefteq G\): lying over,
+  conjugation, inertia groups, the Clifford decomposition, and Clifford
+  correspondence.
+  \item Character extension, extension maps, transversals, and maximal
+  extendibility, all with equivariance data.
+\end{enumerate}
+
+The finiteness theorem permits a later refinement of the public statement
+to \texttt{Fintype.card}.  An equivalence between the two subtypes should
+prove that this is definitionally irrelevant to the original
+\texttt{Cardinal.mk} equality.
+
+\section{Proof dependency graph}
+
+The natural-language proof has four sharply different layers:
+\[
+\begin{gathered}
+\text{ordinary and projective character theory}\\
+\Downarrow\\
+\text{central isomorphisms, Butterfly, and the definition of }\IMK\\
+\Downarrow\\
+\text{CFSG family verification, ending with type }D\\
+\Downarrow\\
+\text{Rossi reduction and normalizer-index induction}.
+\end{gathered}
+\]
+The last implication is short.  The third layer contains almost all of
+the published difficulty and cannot be replaced by the statement that a
+bijection implies equal cardinalities.
+
+\subsection{Exact literature chain to encode}
+
+The declarations should mirror the following named results from
+Cabanes--Sp{\"a}th \cite{CabanesSpath2026}.
+
+\begin{longtable}{p{0.15\textwidth}p{0.75\textwidth}}
+\toprule
+Paper result & Lean-facing obligation \\
+\midrule
+\endfirsthead
+\toprule
+Paper result & Lean-facing obligation \\
+\midrule
+\endhead
+Theorem 2.8 &
+Butterfly transport for centrally isomorphic character triples. \\
+Theorem 2.10 &
+Rossi's reduction: if all universal covering groups of nonabelian finite
+simple groups satisfy \(\IMK\), then all finite groups do. \\
+Theorem 2.11 &
+The already completed alternating, sporadic, defining-characteristic,
+small-prime, exceptional, and non-\(D\) Lie-type cases. \\
+Theorem 2.21 &
+For the finite-reductive setup, the local conditions \(\Ad\) and
+\(\Bd\), together with the global extension input, imply \(\IMK\). \\
+Theorem 4.1 &
+The doubly regular and rank-four type-\(D\) cases. \\
+Lemma 5.8 &
+The exhaustive trichotomy: doubly regular, cyclotomic multiplicity at
+most one, or a disconnected maximal-rank subgroup with two type-\(D\)
+factors. \\
+Theorem 5.20 &
+Stable transversals and character extensions for the subgroup \(M\). \\
+Proposition 6.3 &
+Transport of the relevant correspondences by central isomorphisms. \\
+Theorem 6.4 and Corollary 6.5 &
+Stable transversals and maximal extendibility for the local normalizer. \\
+Propositions 6.7--6.8 &
+Equivariant extension maps, including compatibility with linear twists. \\
+Theorem 6.9 &
+Assembly of \(\Ad\) and \(\Bd\) in the non-doubly-regular case. \\
+Lemmas 6.10--6.11 &
+Transport between the twisted Frobenius model and the original finite
+group. \\
+Theorem 6.12 &
+\(\IMK\) for quasisimple groups of type \(D\) and \({}^{2}D\) in the
+remaining nondefining odd characteristics. \\
+Theorem B &
+The final equivariant bijection from a group to its Sylow normalizer,
+obtained by induction on the normalizer index. \\
+\bottomrule
+\end{longtable}
+
+\section{Audit of existing Lean libraries}
+
+\subsection{Pinned mathlib}
+
+Mathlib \cite{Mathlib} provides a strong general algebraic base:
+
+\begin{itemize}
+  \item \texttt{Sylow p G}, existence of Sylow subgroups, conjugacy, and
+  the normalizer/stabilizer lemmas;
+  \item \texttt{Subgroup.normalizer}, quotient groups, group actions,
+  semidirect products, and finite cardinal arithmetic;
+  \item \texttt{FDRep}, representation characters, irreducibility, the
+  character inner product, orthonormality, and Maschke semisimplicity;
+  \item abstract induced and coinduced representations;
+  \item group extensions and group cohomology;
+  \item perfect and simple groups; and
+  \item root pairings, root data, Weyl groups, and Coxeter groups.
+\end{itemize}
+
+The precise Sylow declarations already used or expected by the assembly
+layer include:
+
+\begin{itemize}
+  \item \path{Sylow.nonempty} and
+  \path{Sylow.smul_eq_iff_mem_normalizer};
+  \item \path{Sylow.stabilizer_eq_normalizer} and
+  \path{Sylow.equivQuotientNormalizer}; and
+  \item \path{Sylow.card_eq_card_quotient_normalizer} and
+  \path{Sylow.card_eq_index_normalizer}.
+\end{itemize}
+
+Mathlib does not currently provide the complete finite indexing type of
+ordinary irreducible characters needed here, Clifford theory, projective
+character triples, central isomorphisms, \(\IMK\), finite reductive
+groups, Deligne--Lusztig theory, or a formal classification of finite
+simple groups.
+
+\subsection{Odd Order}
+
+The most immediately reusable public development is the
+\texttt{yawara/odd-order} project \cite{OddOrderLean}.  At the inspected
+commit it contains:
+
+\begin{itemize}
+  \item \texttt{IrreducibleCharacter} and
+  \texttt{finite\_irreducibleCharacter};
+  \item the positive natural-cast theorem for evaluation at the identity;
+  \item row and column orthogonality and the sum-of-squared-degrees
+  identity;
+  \item restriction, induction, and Frobenius reciprocity;
+  \item \texttt{LiesOver}, conjugation, inertia groups, the Clifford
+  decomposition, and Clifford correspondence; and
+  \item cyclic and canonical extension theorems.
+\end{itemize}
+
+\begin{landscape}
+\subsection{Coverage matrix}
+
+\scriptsize
+\begin{longtable}{p{0.165\linewidth}p{0.085\linewidth}p{0.10\linewidth}p{0.09\linewidth}p{0.09\linewidth}p{0.10\linewidth}p{0.19\linewidth}}
+\toprule
+Concept & mathlib & odd-order & Qiuzhen & TauCeti &
+TNLean / lean-pool & Missing action \\
+\midrule
+\endfirsthead
+\toprule
+Concept & mathlib & odd-order & Qiuzhen & TauCeti &
+TNLean / lean-pool & Missing action \\
+\midrule
+\endhead
+Finite groups, Sylow normalizers &
+strong & uses & uses & no & pool: isolated cases &
+adapter lemmas only \\
+Finite-dimensional complex representations &
+strong & extends & extends & no & TNLean: concrete matrices &
+normalize APIs \\
+Finite \(\Irr(G)\), degrees, orthogonality &
+partial & strong finite indexing & partial & no & no &
+port and bridge; add canonical degree accessor \\
+Induction and Frobenius reciprocity &
+categorical only & strong character API & strong formula & no & no &
+port character formulas \\
+Mackey theory &
+absent at character level & partial & useful theorem & no & no &
+license clearance and heartbeat refactor, or reprove \\
+Clifford theory &
+absent & substantial & module-level part & no & no &
+port a clean character-level equivalence \\
+Extensions and Gallagher theory &
+small & useful partial & cyclic quotient & no & no &
+maximal extendibility and equivariant extension maps \\
+Projective representations and factor sets &
+\(H^2\), cocycles & absent & absent & no &
+TNLean: concrete scaffold; pool: crossed products &
+generalize and connect to characters \\
+Central isomorphism and Butterfly &
+absent & absent & absent & no & absent &
+entire new layer \\
+Quasisimple groups, components, and \(F^*\) &
+partial & strong structural layer & uses & no & no &
+universal covers and Schur multipliers \\
+CFSG family exhaustion &
+absent & Feit--Thompson only & rank-one work & roadmap & no &
+classification and every family verification \\
+Root data and Weyl groups &
+abstract foundations & no & partial & lattice-level &
+pool: types \(A/BC\) only &
+explicit type \(D\) and algebraic-group bridge \\
+Algebraic groups and split tori &
+early foundations & no & no & early foundations & no &
+reductive, Borel, parabolic, Levi, and classification layers \\
+Uniform finite groups of Lie type &
+absent & small rank-one islands & rank-one work & absent & no &
+all classical and exceptional families \\
+Sylow \(d\)-tori and relative Weyl groups &
+absent & absent & absent & absent & absent &
+entire new layer \\
+Finite-reductive character theory &
+absent & absent & absent & absent & absent &
+Deligne--Lusztig, Harish--Chandra, Jordan, and Lusztig series \\
+\(\mathrm{A}(\infty)\), \(\Ad\), and \(\Bd\) &
+absent & absent & absent & absent & absent &
+formalize the family papers \\
+\(\IMK\), Rossi reduction, and type \(D\) &
+absent & absent & absent & absent & absent &
+formalize the complete Annals dependency chain \\
+\bottomrule
+\end{longtable}
+\normalsize
+\end{landscape}
+
+This is substantial but not a finished Clifford API:
+\texttt{clifford\_decomposition} repackages decomposition data supplied
+as a hypothesis, while other files prove important irreducibility,
+injectivity, and single-orbit components.  A clean character-level
+equivalence still has to be assembled.
+
+These results live primarily in
+\texttt{IrrIndexing.lean},
+\texttt{CharacterCount.lean},
+\texttt{ZIrrFourier.lean},
+\texttt{Clifford.lean}, and
+\texttt{CliffordCorrespondence.lean}.  They target Lean 4.32 and an
+older mathlib commit, approximately 850 mathlib commits behind this
+package.  Reuse therefore requires a controlled port; downgrading this
+package would violate the latest-mathlib requirement and would merely
+defer the port.
+
+\subsection{Other audited repositories and version boundaries}
+
+The Qiuzhen CFSG project \cite{QiuzhenCFSG} has another partial
+ordinary-character development, including completeness, orthogonality,
+induction, Frobenius reciprocity, Mackey theory, a genuine module-level
+Clifford theorem, and a cyclic-quotient extension result.  Its completed
+classification work reaches an odd-order/rank-one \(BN\)-pair result,
+not the CFSG.  No repository license was present at the audited commit,
+so its code must not be copied until reuse permission is clarified.
+
+TauCeti \cite{TauCeti} contains genuine foundations for affine group
+schemes, Hopf algebras, functors of points, diagonalizable groups, split
+tori, and character/cocharacter lattices.  Its roadmap still lists
+reductive groups, Borel/parabolic/Levi theory, extraction of root data,
+Bruhat and \(BN\)-pair theory, and classification as future layers.
+
+The inspected lean-pool revision \cite{LeanPool} contains isolated
+finite-group and representation-theoretic results, including a
+normal-Sylow argument for groups of order \(pq\), but no ordinary
+character-theory library usable for the McKay reduction.  Searches of
+these projects and public formal-conjecture collections found no existing
+formal statement or proof of the general McKay theorem.
+
+TNLean \cite{TNLean} supplies the most concrete projective-representation
+scaffold found in the search:
+\texttt{ScalarCocycle}, \texttt{ProjectiveRepresentation}, associativity
+of the cocycle, cohomology of scalar cocycles, and an \(H^2\) quotient.
+It represents matrices in
+\(\operatorname{GL}(\operatorname{Fin} D,\mathbb C)\) and permits all
+units of \(\mathbb C\), rather than specifically \(U(1)\).  It has no
+ordinary characters, induction, restriction, or invariant-character
+construction.  Its two-file cocycle layer is useful, but must be
+generalized and connected to mathlib's representation and cohomology
+APIs.
+
+The version boundary is strict.  Odd Order and lean-pool use Lean
+4.32.0-rc1 with mathlib \texttt{360da6f\ldots}; Qiuzhen, TauCeti, and
+TNLean use Lean 4.32.0 with mathlib \texttt{81a5d25\ldots}.  This package
+uses Lean 4.33.0-rc1 and mathlib \texttt{9cebae5\ldots}.  These packages
+cannot be placed unchanged in one Lake graph.  Selected files must be
+ported to the current pin and reviewed there.
+
+\subsection{Minimal port plan under the heartbeat restriction}
+
+The first port should be the following Apache-licensed, heartbeat-clean
+slice from Odd Order:
+
+\begin{lstlisting}
+import OddOrder.GroupTheory.RepresentationTheory.ColumnOrthogonality
+import OddOrder.GroupTheory.RepresentationTheory.InducedCharacter
+import OddOrder.GroupTheory.RepresentationTheory.Clifford
+import OddOrder.GroupTheory.RepresentationTheory.CliffordAlgClosed
+import OddOrder.GroupTheory.RepresentationTheory.CyclicCharacterExtension
+\end{lstlisting}
+
+The combined internal closure is 30 Odd Order files.  At the audited
+commit it contains no live \texttt{sorry}, axiom declaration,
+\texttt{maxHeartbeats}, or \texttt{maxRecDepth}.  For the generalized
+Fitting subgroup used in the reduction proof, add:
+
+\begin{lstlisting}
+import OddOrder.Isaacs.Ch09_MoreSubnormality.GeneralizedFitting
+\end{lstlisting}
+
+Its 11-file internal closure is also heartbeat-clean.
+
+Do not import the full Odd Order
+\texttt{CliffordDecomposition}/\texttt{OrbitOnIrr} closure unchanged:
+its 101-file closure reaches two subnormality files with scoped
+\texttt{maxHeartbeats 1200000}.  The corresponding Qiuzhen Mackey closure
+sets \texttt{maxHeartbeats 800000}, and its cyclic-extension closure
+reaches a scoped value of \(4{,}000{,}000\).  Under this project's
+constraint, the relevant theorems must be isolated and refactored until
+they compile at the default limit.  TNLean's
+\texttt{Algebra.CocycleCohomology} import is a heartbeat-clean two-file
+candidate for the later projective layer.  TauCeti and lean-pool should
+not be early dependencies: their current results are too far below the
+missing finite-reductive character theory to reduce near-term work.
+
+\section{Proposed Lean interfaces}
+
+The snippets in this section specify interfaces, not unchecked
+implementations.  Universe parameters and existing mathlib names should
+be reused wherever possible.
+
+\subsection{Character operations}
+
+\begin{lstlisting}
+namespace McKayConjecture
+
+def IrreducibleCharacter.degree
+    (chi : IrreducibleCharacter G) : Nat := ...
+
+def PPrimeIrreducibleCharacter
+    (p : Nat) (G : Type u) [Group G] :=
+  { chi : IrreducibleCharacter G // Not (Dvd.dvd p chi.degree) }
+
+def IrreducibleCharacter.map
+    (e : MulEquiv G H) :
+    Equiv (IrreducibleCharacter G) (IrreducibleCharacter H) := ...
+
+theorem degree_map (e : MulEquiv G H) (chi : IrreducibleCharacter G) :
+    (chi.map e).degree = chi.degree := ...
+
+def IrreducibleCharacter.restrict
+    (H : Subgroup G) (chi : IrreducibleCharacter G) :
+    VirtualCharacter H := ...
+
+end McKayConjecture
+\end{lstlisting}
+
+The restriction of an irreducible character need not be irreducible, so
+the codomain must be a character or virtual-character object rather than
+\(\Irr(H)\).  Constituents and their multiplicities should be separate
+definitions.
+
+\Needspace{28\baselineskip}
+\subsection{Character triples}
+
+\begin{lstlisting}[basicstyle=\ttfamily\footnotesize\mdseries\upshape]
+structure CharacterTriple
+    (ambient : Type u) [Group ambient] where
+  normal : Subgroup ambient
+  isNormal : normal.Normal
+  chi : IrreducibleCharacter normal
+  invariant : forall a : ambient, chi.conjBy a = chi
+
+structure ProjectiveRepresentation
+    (k : Type v) (G : Type u) (V : Type w)
+    [Field k] [Group G] [AddCommGroup V] [Module k V] where
+  matrix : G -> LinearEquiv k V V
+  factorSet : G -> G -> Units k
+  mul_matrix : forall x y,
+    matrix x * matrix y =
+      SMul.smul (factorSet x y : k) (matrix (x * y))
+
+def CharacterTriple.CentrallyIsomorphic
+    (T : CharacterTriple A) (H : Subgroup A)
+    (U : CharacterTriple H) : Prop := ...
+\end{lstlisting}
+
+The actual projective-representation structure should encode nonzero
+factor-set values and prove the normalized 2-cocycle identity.  Whenever
+possible, it should reuse mathlib's multiplicative cocycles and group
+cohomology rather than introducing a parallel theory.
+
+For \(T=(A,X,\chi)\) and \(U=(H,M,\chi')\), the
+central-isomorphism data must carry the group conditions
+\[
+  \Cent_A(X)\leq H\leq A,\qquad A=XH,\qquad H\cap X=M,
+\]
+associated projective representations whose factor sets agree on
+\(H\times H\), and equality of their scalar matrices on
+\(\Cent_A(X)\).  Omitting these fields would make the relation too weak
+for Butterfly transport.
+
+The central-isomorphism relation needs named theorems for:
+
+\begin{lstlisting}
+theorem CentrallyIsomorphic.refl : T.CentrallyIsomorphic T := ...
+theorem CentrallyIsomorphic.trans :
+    T.CentrallyIsomorphic U ->
+    U.CentrallyIsomorphic V ->
+    T.CentrallyIsomorphic V := ...
+theorem CentrallyIsomorphic.restrict : ... := ...
+theorem CentrallyIsomorphic.butterfly : ... := ...
+\end{lstlisting}
+
+The Butterfly theorem must expose exactly the automorphism compatibility
+needed during the final induction.  A vague relation carrying only a
+cardinality equality will be too weak.
+
+\Needspace{24\baselineskip}
+\subsection{The inductive McKay package}
+
+\begin{lstlisting}
+structure InductiveMcKayData
+    (X : Type u) [Finite X] [Group X]
+    (p : Nat) [Fact p.Prime] (S : Sylow p X) where
+  local : Subgroup X
+  normalizer_le : SylowNormalizer S <= local
+  proper_of_not_normal :
+    Ne (SylowNormalizer S) (top : Subgroup X) -> Ne local top
+  equivariantCorrespondence :
+    Equiv (PPrimeIrreducibleCharacter p X)
+      (PPrimeIrreducibleCharacter p local)
+  tripleCompatibility : ...
+
+def InductiveMcKay ... : Prop :=
+  Nonempty (InductiveMcKayData X p S)
+\end{lstlisting}
+
+The automorphism group stabilizing \(S\), its action on both character
+sets, and stabilizers of individual characters belong in
+\texttt{tripleCompatibility}.  Keeping the correspondence as an
+equivalence makes the cardinal step immediate while retaining data for
+composition.
+
+\subsection{The final induction}
+
+Once \texttt{InductiveMcKayData} exists for every finite group, the
+normalizer induction is comparatively small:
+
+\Needspace{15\baselineskip}
+\begin{lstlisting}
+theorem pPrimeEquiv_sylowNormalizer_of_all_iMK
+    (all_iMK :
+      forall (X : Type u) [Finite X] [Group X]
+        (p : Nat) [Fact p.Prime] (S : Sylow p X),
+        InductiveMcKay X p S) :
+    Equiv (PPrimeIrreducibleCharacter p G)
+      (PPrimeIrreducibleCharacter p (SylowNormalizer P)) := by
+  -- Strong induction on the finite index [G : N_G(P)].
+  ...
+\end{lstlisting}
+
+The proof must establish in Lean that:
+
+\begin{enumerate}
+  \item \(P\) is Sylow in the intermediate subgroup \(N\);
+  \item \(\Norm_N(P)=\Norm_G(P)\), using
+  \(\Norm_G(P)\leq N\);
+  \item the normalizer index strictly decreases when \(N<G\);
+  \item automorphism actions restrict correctly; and
+  \item central-isomorphism witnesses compose by restriction, Butterfly,
+  and transitivity.
+\end{enumerate}
+
+Only after the stronger equivalence is constructed should the public
+cardinal equality be obtained.
+
+\section{Finite-reductive and classification interfaces}
+
+\subsection{Finite reductive setup}
+
+Avoid baking matrix models into the generic API.  Define a Frobenius
+endomorphism of an algebraic group, its fixed-point subgroup, regular
+embeddings with connected center, and compatible field/graph
+automorphisms.  The first reusable targets are:
+
+\begin{enumerate}
+  \item finite fixed points of a Frobenius endomorphism;
+  \item tori, centralizers, and normalizers compatible with fixed points;
+  \item Sylow \(d\)-tori and generic Sylow theorems;
+  \item relative Weyl groups;
+  \item regular embeddings and induced diagonal automorphisms; and
+  \item equivariant parametrizations of global and local characters.
+\end{enumerate}
+
+The character theory then requires formal versions of Harish--Chandra
+induction, Deligne--Lusztig induction, Lusztig series, and Jordan
+decomposition.  These are not cosmetic abstractions: they provide the
+global/local bijections and automorphism equivariance used by
+Theorem 2.21.
+
+\subsection{\texorpdfstring{Conditions \(\mathrm{A}(\infty)\), \(\Ad\),
+  and \(\Bd\)}{Conditions A(infinity), A(d), and B(d)}}
+
+Represent a stable transversal as chosen representatives plus proofs of
+coverage, pairwise orbit separation, stability under the outer action,
+and extension to stabilizers.  Represent an extension map as a dependent
+function whose codomain is the irreducible characters of the appropriate
+inertia group, with restriction, equivariance, and twist compatibility
+fields.
+
+\begin{lstlisting}
+structure EquivariantExtensionMap ... where
+  extension : forall chi, IrreducibleCharacter (inertia chi)
+  restrict_extension : forall chi, ...
+  action_compatible : forall a chi, ...
+  twist_compatible : forall lambda chi, ...
+
+structure LocalConditionA ...
+structure LocalConditionB ...
+\end{lstlisting}
+
+Separate these structures from type \(D\).  Other Lie families should be
+able to instantiate the same interfaces.
+
+\subsection{\texorpdfstring{Type-\(D\) arithmetic and subgroup construction}
+  {Type-D arithmetic and subgroup construction}}
+
+The type-\(D\) portion should be divided into:
+
+\begin{enumerate}
+  \item cyclotomic multiplicities in the polynomial order;
+  \item the predicate that \(d\) is doubly regular;
+  \item the rank-four and doubly regular correspondence;
+  \item the exhaustive Lemma 5.8 trichotomy;
+  \item the twisted Frobenius \(F'=\nu F_q\) and construction of the
+  disconnected maximal-rank algebraic subgroup \(\mathbf M\), with
+  \((\mathbf M^\circ)_{\mathrm{der}}\) of type
+  \(D_{l_1}\times D_{l_2}\);
+  \item Clifford analysis through
+  \(M_0=G_1.G_2\trianglelefteq
+  M^\circ=(\mathbf M^\circ)^{F'}\trianglelefteq
+  M=\mathbf M^{F'}\), retaining
+  \([M:M_0]=2\gcd(2,q-1)\);
+  \item stable transversals and extensions (Theorem 5.20);
+  \item transport and local extension maps (Section 6); and
+  \item the cases of Theorem 6.12, including the cyclic-Sylow branch.
+\end{enumerate}
+
+Arithmetic statements about the polynomial order should be proved in
+generic polynomial/cyclotomic modules.  The representation-theoretic
+consequences belong in later files.  This separation keeps normalization
+and finite-field calculations from overwhelming character arguments.
+
+\subsection{CFSG family coverage}
+
+The reduction theorem quantifies over universal covers of all nonabelian
+finite simple groups.  A formal proof needs:
+
+\begin{enumerate}
+  \item a formal classification theorem or an equivalent exhaustive
+  family-recognition interface;
+  \item constructions of the universal covers and their centers;
+  \item the previously proved \(\IMK\) instances for alternating and
+  sporadic groups and every Lie family in Theorem 2.11; and
+  \item the new type-\(D\) instance from Theorem 6.12.
+\end{enumerate}
+
+An enumeration datatype whose ``exhaustive'' constructor is assumed is
+not enough.  The theorem connecting an arbitrary finite simple group to
+one of the families must itself be kernel-checked.
+
+\section{File and namespace plan}
+
+Files should follow mathematical boundaries and remain small enough that
+ordinary heartbeat limits diagnose local problems.  The proposed layout
+is:
+
+\begin{description}[style=nextline,leftmargin=2em,labelindent=0pt]
+  \item[\texttt{Character/Basic.lean}]
+  Class functions, characters, irreducibility, and the bridge to the
+  audited statement wrapper.
+  \item[\texttt{Character/Degree.lean}]
+  Natural degrees, positivity, invariance under isomorphism, and
+  \(p'\)-degree.
+  \item[\texttt{Character/Finite.lean}]
+  Finiteness of \(\Irr(G)\), the finite \(p'\)-subtype, and cardinal
+  comparison.
+  \item[\texttt{Character/Operations.lean}]
+  Automorphism actions, induction, restriction, constituents, and
+  Frobenius reciprocity.
+  \item[\texttt{Character/Clifford.lean}]
+  Lies-over, conjugation, inertia, decomposition, and correspondence.
+  \item[\texttt{Character/Extension.lean}]
+  Extensions, transversals, extension maps, and maximal extendibility.
+  \item[\texttt{CharacterTriple/ProjectiveRepresentation.lean}]
+  Factor sets, cocycles, scalar actions, and projective characters.
+  \item[\texttt{CharacterTriple/CentralIsomorphism.lean}]
+  Central-isomorphism data and induced character correspondences.
+  \item[\texttt{CharacterTriple/Butterfly.lean}]
+  Restriction, transitivity, and Butterfly transport.
+  \item[\texttt{InductiveMcKay/Basic.lean}]
+  Automorphism stabilizers, equivariant correspondence, and \(\IMK\).
+  \item[\texttt{InductiveMcKay/LocalCriterion.lean}]
+  Conditions \(\mathrm{A}(\infty)\), \(\Ad\), \(\Bd\), and
+  Theorem 2.21.
+  \item[\texttt{InductiveMcKay/Reduction.lean}]
+  The Isaacs--Malle--Navarro/Rossi reduction.
+  \item[\texttt{FiniteReductive/Frobenius.lean}]
+  Algebraic groups with Frobenius and finite fixed points.
+  \item[\texttt{FiniteReductive/RegularEmbedding.lean}]
+  Connected-center embeddings and induced automorphisms.
+  \item[\texttt{FiniteReductive/SylowDTorus.lean}]
+  Sylow \(d\)-tori and generic Sylow theory.
+  \item[\texttt{FiniteReductive/RelativeWeyl.lean}]
+  Local normalizers and relative Weyl groups.
+  \item[\texttt{FiniteReductive/CharacterCorrespondence.lean}]
+  Harish--Chandra, Deligne--Lusztig, and Jordan parametrizations.
+  \item[\texttt{TypeD/DoublyRegular.lean}]
+  Polynomial order, double regularity, and Theorem 4.1.
+  \item[\texttt{TypeD/Trichotomy.lean}]
+  Cyclotomic arithmetic and Lemma 5.8.
+  \item[\texttt{TypeD/MaximalRankSubgroup.lean}]
+  Construction and structure of \(M\).
+  \item[\texttt{TypeD/StableTransversal.lean}]
+  Clifford strata and Theorem 5.20.
+  \item[\texttt{TypeD/ExtensionMap.lean}]
+  Propositions 6.3, 6.7, 6.8, Theorem 6.4, and Corollary 6.5.
+  \item[\texttt{TypeD/InductiveMcKay.lean}]
+  Theorems 6.9 and 6.12 plus Frobenius transport.
+  \item[\texttt{CFSG/FamilyCoverage.lean}]
+  Formal family exhaustion and Theorem 2.11.
+  \item[\texttt{Proof/NormalizerInduction.lean}]
+  The well-founded induction from an intermediate subgroup to
+  \(\Norm_G(P)\).
+  \item[\texttt{Proof/Main.lean}]
+  Family coverage, reduction, final equivalence, and the exported
+  cardinal equality.
+\end{description}
+
+Namespace names should describe stable concepts rather than paper
+section numbers.  Theorem-number aliases may be supplied locally for
+traceability, but declarations exported to downstream users should have
+semantic names such as
+\path{LocalCondition.impliesInductiveMcKay} and
+\path{TypeD.inductiveMcKay}.
+
+\section{Implementation sequence and compile gates}
+
+\begin{milestone}[Port the ordinary-character core]
+Port the minimum odd-order modules to the pinned mathlib, keeping the
+upstream theorem names when sensible.  Prove an equivalence with
+\texttt{McKayConjecture.IrreducibleCharacter}.  Gate:
+\texttt{lake build McKayConjecture.Character} and a finite
+\(\Irr(G)\) instance without new axioms.
+\end{milestone}
+
+\begin{milestone}[Clifford and extension API]
+Port restriction/induction, Clifford theory, and extension results.
+Fill gaps in equivariance and maximal extendibility.  Gate: compile
+small examples for normal subgroups of cyclic, dihedral, and symmetric
+groups, and verify restriction/induction multiplicities by the general
+theorems rather than computation-specific axioms.
+\end{milestone}
+
+\begin{milestone}[Central character triples]
+Develop projective representations, central isomorphism, restriction,
+transitivity, and Butterfly.  Gate: construct the identity central
+isomorphism, prove compositional laws, and replay the cyclic-quotient
+extension case.
+\end{milestone}
+
+\begin{milestone}[Abstract normalizer induction]
+Define \(\IMK\) and prove that \(\IMK\) for every finite group yields the
+full equivariant bijection with the Sylow normalizer.  Gate: the theorem
+must use a well-founded measure on subgroup index and must compile without
+assuming the McKay equality.
+\end{milestone}
+
+\begin{milestone}[Finite reductive foundations]
+Integrate the needed TauCeti/mathlib algebraic-group foundations and
+formalize Frobenius fixed points, regular embeddings, Sylow \(d\)-tori,
+and relative Weyl groups.  Gate: recover the local normalizer structures
+used by Theorem 2.21 in representative classical groups.
+\end{milestone}
+
+\begin{milestone}[Character correspondences and local criterion]
+Formalize the global and local parametrizations and prove the generic
+\(\mathrm{A}(\infty)+\Ad+\Bd\) criterion.  Gate: instantiate it for each
+already developed family without type-\(D\)-specific definitions leaking
+into the interface.
+\end{milestone}
+
+\begin{milestone}[Final type \(D\)]
+Formalize the polynomial arithmetic, doubly regular case, Lemma 5.8,
+the subgroup \(M\), Theorem 5.20, and the Section 6 extension maps.
+Gate: a theorem named \path{TypeD.inductiveMcKay} covering exactly
+Theorem 6.12 with no assumed local conditions.
+\end{milestone}
+
+\begin{milestone}[Classification and reduction]
+Connect every universal cover in the formal CFSG exhaustion to a proved
+\(\IMK\) instance, then formalize Rossi's reduction.  Gate:
+\path{allFiniteGroups_inductiveMcKay} has no family-coverage or
+classification assumption in its type or axiom report.
+\end{milestone}
+
+\begin{milestone}[Export and audit]
+Compose reduction with normalizer induction and export the final theorem.
+Gate:
+\begin{lstlisting}
+lake build
+rg -n 'sorry|axiom|admit|maxHeartbeats' McKayConjecture
+#check McKayConjecture.mckay
+#print axioms McKayConjecture.mckay
+\end{lstlisting}
+The text search must be reviewed manually because comments may discuss
+forbidden placeholders, while generated dependencies may legitimately
+contain standard axioms.
+\end{milestone}
+
+\section{Testing strategy}
+
+\subsection{Semantic tests}
+
+Use small groups to test interfaces, not to replace general proofs:
+
+\begin{itemize}
+  \item trivial and cyclic groups test degree-one characters and the
+  self-normalizing base case;
+  \item \(S_3\) at \(p=2,3\) tests restriction, induction, and different
+  Sylow normalizers;
+  \item \(A_4\) at \(p=2,3\) tests nontrivial automorphism orbits and
+  Clifford decomposition;
+  \item small dihedral groups test cyclic-index-two extensions; and
+  \item isomorphic copies of the same finite group test that the count is
+  independent of representation carriers and chosen Sylow subgroup.
+\end{itemize}
+
+Each example should prove equality by specializing the general theorem
+once that theorem exists.  Before then, direct computations are regression
+tests for definitions only.
+
+\subsection{Build and dependency tests}
+
+Continuous integration should:
+
+\begin{enumerate}
+  \item install the exact Lean toolchain from \texttt{lean-toolchain};
+  \item restore the mathlib cache and run \texttt{lake build};
+  \item reject merge conflicts and unexpected dependency changes;
+  \item run a source audit for unfinished proofs and heartbeat overrides;
+  \item compile a small file containing \texttt{\#print axioms} for the
+  exported theorem; and
+  \item build the two LaTeX documents with warnings treated as review
+  failures.
+\end{enumerate}
+
+\section{Feasibility assessment}
+
+The current ecosystem already supports a faithful statement and a
+meaningful first implementation phase: ordinary character indexing,
+degree arithmetic, much of Clifford theory, and the elementary final
+normalizer induction.  It does not contain the decisive mathematical
+inputs.  A complete proof additionally requires a large project in
+projective character theory, finite reductive groups, the full
+family-by-family inductive McKay verification, and a formal CFSG
+exhaustion.
+
+This assessment changes the schedule, not the theorem.  The correct
+engineering response is to preserve a strict trust boundary, build the
+reusable lower layers at the latest mathlib revision, and keep every
+unformalized literature theorem visible as an open proof obligation.
+Replacing those obligations by assumptions would produce a compiling
+demonstration of the assembly but not the requested fully formal proof.
+
+\begingroup
+\footnotesize
+\bibliographystyle{alpha}
+\bibliography{references}
+\endgroup
+
+\end{document}
diff --git a/mckay-conjecture/docs/mckay_proof.tex b/mckay-conjecture/docs/mckay_proof.tex
new file mode 100644
index 00000000..6b04e92b
--- /dev/null
+++ b/mckay-conjecture/docs/mckay_proof.tex
@@ -0,0 +1,681 @@
+\documentclass[11pt]{article}
+
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+\usepackage{lmodern}
+\usepackage[margin=1in]{geometry}
+\usepackage{microtype}
+\usepackage{amsmath,amssymb,amsthm,mathtools}
+\usepackage{booktabs}
+\usepackage{enumitem}
+\usepackage{longtable}
+\usepackage{tabularx}
+\usepackage{xcolor}
+\usepackage{hyperref}
+\usepackage[nameinlink,noabbrev]{cleveref}
+
+\definecolor{linkblue}{HTML}{174A7E}
+\hypersetup{
+  colorlinks=true,
+  linkcolor=linkblue,
+  citecolor=linkblue,
+  urlcolor=linkblue,
+  pdftitle={A Detailed Proof of the McKay Equality},
+  pdfauthor={Clawristotle contributors}
+}
+
+\newtheorem{theorem}{Theorem}[section]
+\newtheorem{proposition}[theorem]{Proposition}
+\newtheorem{lemma}[theorem]{Lemma}
+\newtheorem{definition}[theorem]{Definition}
+\newtheorem{remark}[theorem]{Remark}
+
+\newcommand{\Irr}{\operatorname{Irr}}
+\newcommand{\Aut}{\operatorname{Aut}}
+\newcommand{\Inn}{\operatorname{Inn}}
+\newcommand{\Out}{\operatorname{Out}}
+\newcommand{\Norm}{\operatorname{N}}
+\newcommand{\Cent}{\operatorname{C}}
+\newcommand{\Syl}{\operatorname{Syl}}
+\newcommand{\Z}{\operatorname{Z}}
+\newcommand{\Ind}{\operatorname{Ind}}
+\newcommand{\Res}{\operatorname{Res}}
+\newcommand{\IMK}{\mathrm{iMK}}
+\newcommand{\Ad}{\mathrm{A}(d)}
+\newcommand{\Bd}{\mathrm{B}(d)}
+\newcommand{\Ainf}{\mathrm{A}(\infty)}
+\newcommand{\F}{\mathbf{F}}
+\newcommand{\G}{\mathbf{G}}
+\newcommand{\M}{\mathbf{M}}
+\newcommand{\Sbf}{\mathbf{S}}
+
+\title{\textbf{A Detailed Natural-Language Proof of the McKay Equality}\\
+\large A proof certificate through the inductive McKay condition}
+\author{Clawristotle contributors}
+\date{July 2026}
+
+\begin{document}
+
+\maketitle
+
+\begin{abstract}
+For a finite group \(X\), a prime \(\ell\), and a Sylow
+\(\ell\)-subgroup \(S\), the McKay equality says that \(X\) and
+\(\Norm_X(S)\) have the same number of irreducible complex characters
+whose degrees are not divisible by \(\ell\).  The first complete proof is
+not a short argument: it combines the Isaacs--Malle--Navarro reduction,
+the classification of finite simple groups, a family-by-family verification
+of the inductive McKay condition, and the final type-\(D\) analysis of
+Cabanes and Sp{\"a}th.
+
+This document gives a detailed proof at the correct level of granularity:
+every major imported theorem is stated, every family in the classification
+is accounted for, the final type-\(D\) trichotomy is expanded, and the last
+induction from an intermediate local subgroup to the Sylow normalizer is
+proved explicitly.  It is a proof by fully identified literature results,
+not a claim to reproduce the several hundred pages of character theory and
+the classification on which those results depend.
+\end{abstract}
+
+{\small\tableofcontents}
+\clearpage
+
+\section{Statement and conventions}
+
+Let \(X\) be a finite group.  An ordinary complex character of \(X\) is
+the trace of a finite-dimensional complex representation.  Write
+\(\Irr(X)\) for the set of characters afforded by irreducible
+representations, with isomorphic representations counted once.  The
+degree of \(\chi\in\Irr(X)\) is
+\[
+  \chi(1)=\dim_{\mathbb C} V_\chi\in\mathbb Z_{>0}.
+\]
+For a prime \(\ell\), define
+\[
+  \Irr_{\ell'}(X)
+  :=\{\chi\in\Irr(X)\mid \ell\nmid \chi(1)\}.
+\]
+
+\begin{theorem}[McKay equality]\label{thm:mckay}
+Let \(X\) be a finite group, let \(\ell\) be prime, and let
+\(S\in\Syl_\ell(X)\).  Then
+\[
+  \bigl|\Irr_{\ell'}(X)\bigr|
+  =
+  \bigl|\Irr_{\ell'}(\Norm_X(S))\bigr|.
+\]
+\end{theorem}
+
+The theorem does not depend on the chosen Sylow subgroup: any two Sylow
+\(\ell\)-subgroups are conjugate, conjugation identifies their
+normalizers, and a group isomorphism transports irreducible characters
+without changing their degrees.
+
+\section{The stronger inductive condition}
+
+\subsection{Character triples}
+
+A \emph{character triple} is a triple \((A,X,\chi)\) in which
+\(X\trianglelefteq A\) and \(\chi\in\Irr(X)\) is invariant under \(A\).
+Given a second triple \((H,M,\chi')\) with
+\[
+  \Cent_A(X)\leq H\leq A,\qquad A=XH,\qquad H\cap X=M,
+\]
+the relation
+\[
+  (A,X,\chi)\geq_c(H,M,\chi')
+\]
+of centrally isomorphic character triples records substantially more than
+an equality of cardinalities.  Definition 2.6 of
+\cite{CabanesSpath2026} requires associated projective representations
+of \(A\) and \(H\) whose factor sets agree on \(H\times H\), and whose
+scalar matrices agree on \(\Cent_A(X)\).  The relation supplies character
+correspondences over the normal subgroups and has three structural
+properties used below:
+
+\begin{enumerate}[label=(\roman*)]
+  \item it is transitive;
+  \item it can be restricted to suitable subgroups of the outer action;
+  \item its two sides can be transported through the ``Butterfly''
+        construction when they induce the same automorphisms.
+\end{enumerate}
+
+The precise relation and these closure properties are developed in
+Navarro--Sp{\"a}th's language and in Rossi's reformulation
+\cite{Rossi2023,Navarro2018}.  They are the mechanism that makes a
+classification-based argument inductive rather than merely a list of
+numerical coincidences.
+
+\subsection{\texorpdfstring{Definition of \(\IMK\)}{Definition of iMK}}
+
+Fix \(S\in\Syl_\ell(X)\) and put
+\(\Gamma=\Aut(X)_S\).  The condition \(\IMK(X,\ell)\) asserts that there
+are:
+
+\begin{enumerate}
+  \item a \(\Gamma\)-stable subgroup
+  \[
+    \Norm_X(S)\leq N\leq X,
+  \]
+  with \(N\neq X\) whenever \(\Norm_X(S)\neq X\); and
+  \item a \(\Gamma\)-equivariant bijection
+  \[
+    \Omega:\Irr_{\ell'}(X)\longrightarrow\Irr_{\ell'}(N)
+  \]
+  such that, for every \(\chi\) with \(\Omega(\chi)=\chi'\),
+  \[
+    (X\rtimes\Gamma_\chi,X,\chi)
+      \geq_c
+    (N\rtimes\Gamma_\chi,N,\chi').
+  \]
+\end{enumerate}
+
+For universal covers of nonabelian finite simple groups, this is
+equivalent to the inductive McKay condition of
+Isaacs--Malle--Navarro \cite{IsaacsMalleNavarro2007}; see the comparison
+in \cite[Section 2.B]{CabanesSpath2026}.
+
+\begin{theorem}[Reduction theorem]\label{thm:reduction}
+Fix a prime \(\ell\).  If the universal covering group of every
+nonabelian finite simple group satisfies \(\IMK\) at \(\ell\), then every
+finite group satisfies \(\IMK\) at \(\ell\).
+\end{theorem}
+
+The original reduction is due to Isaacs--Malle--Navarro
+\cite{IsaacsMalleNavarro2007}.  The exact centrally-isomorphic-triple
+form used here is Rossi's Theorem B \cite{Rossi2023}, recalled as
+Theorem 2.10 in \cite{CabanesSpath2026}.
+
+\subsection{Inside the reduction theorem}
+
+For completeness, here is the logical mechanism hidden inside
+\cref{thm:reduction}.  A clean equality-level version is Sp{\"a}th's
+Theorem 3.15 \cite{Spath2018}; Rossi's stronger proof follows the same
+minimal-counterexample spine while retaining the central-isomorphism
+data.
+
+One first proves a relative form over each character of the center.
+Assume that this form fails and choose a counterexample \(A\) minimizing
+\(|A/\Z(A)|\).  The reduction proceeds as follows.
+
+\begin{enumerate}
+  \item Local character correspondences and the Glauberman
+  correspondence show that both the largest normal \(\ell\)-subgroup
+  and the largest normal \(\ell'\)-subgroup of \(A\) lie in \(\Z(A)\).
+  Otherwise one passes to a proper quotient or normalizer and contradicts
+  minimality.
+  \item The generalized Fitting subgroup
+  \(F^*(A)=F(A)E(A)\) now has no noncentral solvable part.  A noncentral
+  minimal normal section therefore comes from the layer \(E(A)\).  There
+  is a normal subgroup \(L\) with
+  \[
+    L/\Z(A)\cong T^m
+  \]
+  for a nonabelian finite simple group \(T\) whose order is divisible by
+  \(\ell\).
+  \item The assumed \(\IMK\) correspondence for the universal cover of
+  \(T\) is extended to the \(m\) components, including their permutation
+  action, and then descended through the relevant central quotient.
+  This produces a proper local subgroup of \(L\), containing the needed
+  Sylow normalizer, and a character correspondence compatible with the
+  action of \(A\).
+  \item Clifford theory lifts that correspondence from \(L\) to \(A\).
+  The resulting intermediate subgroup is proper, so minimality applies
+  again and replaces it by the actual Sylow normalizer.
+  \item Restriction and Butterfly transport align the automorphism
+  actions on the two stages; transitivity of central isomorphism composes
+  their character-triple witnesses.  This contradicts the choice of
+  \(A\).
+\end{enumerate}
+
+Thus a hypothetical counterexample would contain a simple section whose
+universal cover violates \(\IMK\).  The hypothesis of
+\cref{thm:reduction} excludes every such section, proving the result.
+
+\subsection{\texorpdfstring{Why \(\IMK\) gives the actual Sylow normalizer}
+  {Why iMK gives the actual Sylow normalizer}}
+
+\begin{proposition}\label{prop:imk-to-mckay}
+If every finite group satisfies \(\IMK\) at \(\ell\), then
+\cref{thm:mckay} holds at \(\ell\).
+\end{proposition}
+
+\begin{proof}
+We prove a stronger statement by induction on
+\[
+  m(X,S):=[X:\Norm_X(S)].
+\]
+If \(m(X,S)=1\), then \(S\trianglelefteq X\) and
+\(\Norm_X(S)=X\), so the identity map is the required bijection.
+
+Assume \(m(X,S)>1\).  The condition \(\IMK(X,\ell)\) supplies a subgroup
+\[
+  \Norm_X(S)\leq N<X
+\]
+and a bijection
+\[
+  \Omega_X:\Irr_{\ell'}(X)\xrightarrow{\sim}\Irr_{\ell'}(N).
+\]
+The subgroup \(S\) is also a Sylow \(\ell\)-subgroup of \(N\): its order
+already contains the full \(\ell\)-part of \(|X|\), hence of \(|N|\).
+Moreover
+\[
+  \Norm_N(S)=N\cap\Norm_X(S)=\Norm_X(S),
+\]
+because \(\Norm_X(S)\leq N\).  Since \(N<X\),
+\[
+  [N:\Norm_N(S)]<[X:\Norm_X(S)].
+\]
+The induction hypothesis applied to \(N\) therefore gives a bijection
+\[
+  \Omega_N:\Irr_{\ell'}(N)
+    \xrightarrow{\sim}
+  \Irr_{\ell'}(\Norm_N(S))
+  =
+  \Irr_{\ell'}(\Norm_X(S)).
+\]
+The composite \(\Omega_N\circ\Omega_X\) proves the desired equality.
+
+For the stronger equivariant statement, one restricts the second outer
+action to the image of \(\Gamma\), applies the Butterfly property, and
+uses transitivity of \(\geq_c\).  This is the final induction in the proof
+of Theorem B of \cite{CabanesSpath2026}.
+\end{proof}
+
+\section{Verification on universal covers}
+
+By \cref{thm:reduction,prop:imk-to-mckay}, it remains to verify
+\(\IMK\) for the universal covering groups of the nonabelian finite
+simple groups.  The classification divides these into alternating
+groups, sporadic groups, and groups of Lie type.  The proof is cumulative:
+the 2026 paper closes the only family left by the preceding results.
+
+\begin{longtable}{p{0.24\textwidth}p{0.50\textwidth}p{0.18\textwidth}}
+\toprule
+Family or prime & Result supplying \(\IMK\) & Source \\
+\midrule
+\endfirsthead
+\toprule
+Family or prime & Result supplying \(\IMK\) & Source \\
+\midrule
+\endhead
+Alternating and sporadic groups
+  & Inductive McKay for simple groups not of Lie type
+  & \cite{Malle2008} \\
+Groups of Lie type in defining characteristic
+  & Inductive McKay in defining characteristic
+  & \cite{Spath2012} \\
+\(\ell=2\), all families
+  & Equivariant character correspondence for odd-degree characters
+  & \cite{MalleSpath2016} \\
+\(\ell=3\), all families
+  & Type-\(D\) extension results, together with the earlier families
+  & \cite{Spath2025II} \\
+Types \(A\) and \({}^{2}A\)
+  & Equivariant character correspondences
+  & \cite{CabanesSpath2017A} \\
+Type \(C\)
+  & Verification of the inductive condition
+  & \cite{CabanesSpath2017C} \\
+Types \(B,E_6,{}^{2}E_6,E_7\)
+  & Descent equalities and local extension conditions
+  & \cite{CabanesSpath2019} \\
+Exceptional types \({}^{3}D_4,E_8,F_4,{}^{2}F_4,G_2\)
+  & Equivariance and extendibility in connected-center groups
+  & \cite{CabanesSpath2013} \\
+Suzuki and Ree types \({}^{2}B_2,{}^{2}G_2\)
+  & Cases contained in the original reduction analysis
+  & \cite{IsaacsMalleNavarro2007} \\
+Type \(D_l\) and \({}^{2}D_l\), remaining non-defining primes
+  & Final local conditions \(\Ad\) and \(\Bd\)
+  & \cite{CabanesSpath2026} \\
+\bottomrule
+\end{longtable}
+
+This inventory is formalized as Theorem 2.11 of
+\cite{CabanesSpath2026}: before its new type-\(D\) argument, only
+\(D_l\) and \({}^{2}D_l\) at primes \(\ell\geq5\) different from the
+defining characteristic remain.
+
+\section{The local criterion for groups of Lie type}
+
+\subsection{Finite reductive setup}
+
+Let \(\G\) be a simple simply connected linear algebraic group over
+\(\overline{\mathbb F}_p\), let \(F:\G\to\G\) be a Frobenius
+endomorphism defining an \(\mathbb F_q\)-structure, and set
+\[
+  G=\G^F.
+\]
+A regular embedding \(\G\leq\widetilde{\G}\) with connected center
+produces
+\[
+  G\trianglelefteq\widetilde G=\widetilde{\G}^{\,F}.
+\]
+Field and graph automorphisms form a group \(E\), and
+\(\widetilde G\rtimes E\) induces the relevant outer automorphisms of
+\(G\).
+
+For an odd prime \(\ell\nmid q\), let
+\[
+  d=d_\ell(q)
+\]
+be the multiplicative order of \(q\) modulo \(\ell\).  A Sylow
+\(d\)-torus \(\Sbf\) of \((\G,F)\) is the finite-reductive analogue of
+a Sylow subgroup.  Generic Sylow theory
+\cite{BroueMalle1992,MalleTesterman2011} relates
+\(\Norm_G(\Sbf)\) to a Sylow \(\ell\)-subgroup of \(G\).  Set
+\[
+\begin{aligned}
+  N&=\Norm_G(\Sbf),\\
+  \widehat N&=\Norm_{G\rtimes E}(\Sbf),\\
+  \widetilde N&=\Norm_{\widetilde G}(\Sbf),\\
+  \widetilde C&=\Cent_{\widetilde G}(\Sbf).
+\end{aligned}
+\]
+
+\subsection{The three extension conditions}
+
+The global condition \(\Ainf\) says that there is an \(E\)-stable
+\(\widetilde G\)-transversal in \(\Irr(G)\) whose members extend to
+their stabilizers in \(G\rtimes E\).  Sp{\"a}th's Theorem A
+\cite{Spath2025II}, together with the earlier type-\(A\), type-\(C\), and
+type-\(B/E\) results, establishes \(\Ainf\) in all types;
+\cite{Spath2023I,Spath2025II} supplies the final type-\(D\) part.
+
+The local condition \(\Ad\) says that there is a
+\(\widehat N\)-stable \(\widetilde N\)-transversal in \(\Irr(N)\)
+whose members extend to the appropriate stabilizers.  The local
+condition \(\Bd\) says:
+
+\begin{enumerate}
+  \item maximal extendibility holds for
+  \(N\trianglelefteq\widetilde N\) and
+  \(\widetilde C\trianglelefteq\widetilde N\); and
+  \item there is an extension map for
+  \(\widetilde C\trianglelefteq\widetilde N\) equivariant under both
+  the linear-character twists of \(\widetilde G/G\) and the outer
+  normalizer action.
+\end{enumerate}
+
+The local criterion, Theorem 2.21 of \cite{CabanesSpath2026} (imported
+from \cite{CabanesSpath2019}), states:
+
+\begin{proposition}[Local criterion]\label{prop:local-criterion}
+Assume \(\ell\nmid 6q\), \(G/\Z(G)\) is simple, \(G\) is its universal
+cover, and \(\Ad\) and \(\Bd\) hold for
+\(d=d_\ell(q)\).  Then \(G\) satisfies \(\IMK\) at \(\ell\), with
+local subgroup \(\Norm_{\G}(\Sbf)^F\).
+\end{proposition}
+
+The proof combines \(\Ainf\), the local extension data, and a common
+parametrization of global and local characters obtained through
+generic Harish--Chandra theory and Jordan decomposition
+\cite{Malle2007,BroueMalleMichel1993}.  The resulting bijection is
+outer-equivariant and its paired characters define centrally
+isomorphic character triples.
+
+\section{\texorpdfstring{The final type-\(D\) verification}
+  {The final type-D verification}}
+
+\subsection{Arithmetic organization}
+
+Take
+\[
+  G=D_{l,\mathrm{sc}}^\varepsilon(q),
+  \qquad l\geq4,\quad \varepsilon\in\{1,-1\}.
+\]
+The polynomial order of \((\G,F)\) is
+\[
+ P_{(\G,F)}(X)
+ =
+ X^{l^2-l}
+ (X^2-1)(X^4-1)\cdots(X^{2l-2}-1)(X^l-\varepsilon).
+\]
+Let \(a_{(\G,F)}(m)\) be the multiplicity of a primitive \(m\)-th root
+of unity as a root of this polynomial.
+
+An integer \(d\geq3\) is \emph{doubly regular} for \((\G,F)\) when
+\[
+  d\mid 2l
+  \quad\text{and}\quad
+  \frac{2l}{d}
+  \begin{cases}
+    \text{is even},&\varepsilon=1,\\
+    \text{is odd},&\varepsilon=-1.
+  \end{cases}
+\]
+This is stronger than ordinary regularity: it controls the centralizer
+of a Sylow \(\ell\)-subgroup both in the type-\(D_l\) group and in the
+ambient type-\(B_l\) overgroup.
+
+\subsection{Doubly regular case}
+
+Theorem 4.1 of \cite{CabanesSpath2026} proves that if \(d\) is doubly
+regular, then \(\Ad\) and \(\Bd\) hold.  Its construction uses:
+
+\begin{enumerate}
+  \item explicit Tits-group representatives in the torus normalizer;
+  \item relative Weyl groups
+  \(\Norm_{\G}(\Sbf,\xi)^F/\Cent_{\G}(\Sbf)^F\);
+  \item compatible extension maps for characters of the torus
+  centralizer; and
+  \item control of field, graph, and diagonal automorphisms.
+\end{enumerate}
+
+Consequently \cref{prop:local-criterion} gives \(\IMK\) for every odd
+prime \(\ell\nmid q\) with \(d_\ell(q)=d\).  Since \(d\geq3\), such a
+prime is at least \(5\).  The same theorem separately settles rank
+\(l=4\).
+
+\subsection{The trichotomy}
+
+For \(l\geq5\) and \(d\geq3\), Lemma 5.8 of
+\cite{CabanesSpath2026} proves that at least one of the following three
+alternatives holds:
+
+\begin{enumerate}[label=(\alph*)]
+  \item \(d\) is doubly regular;
+  \item \(a_{(\G,F)}(d)\leq1\), and
+  \(a_{(\G,F)}(dm)=0\) for every odd \(m\geq3\); or
+  \item there are \(l_1,l_2>0\), signs
+  \(\varepsilon_1,\varepsilon_2\), and \(j\in\{1,2\}\) such that
+  \[
+    l_1+l_2=l,\qquad
+    \varepsilon_1\varepsilon_2=\varepsilon,
+  \]
+  the \(j\)-th type-\(D\) factor has rank \(l_j\geq4\), \(d\) is
+  doubly regular for that factor, and its \(d\)-multiplicity equals
+  \(a_{(\G,F)}(d)\).
+\end{enumerate}
+
+Case (a) is already done.  For case (b), the needed cyclotomic step is
+the following: for odd \(\ell\),
+\[
+  \ell\mid\Phi_m(q)
+  \quad\Longleftrightarrow\quad
+  m=d\ell^a\text{ for some }a\geq0
+\]
+\cite[Lemma 5.2(a)]{Malle2007}.  Alternative (b), applied with
+\(m=\ell^a\), gives
+\(a_{(\G,F)}(d\ell^a)=0\) for \(a\geq1\).  Thus the entire
+\(\ell\)-part of \(|G|\) lies in a Sylow \(d\)-torus of rank at most one,
+so the Sylow \(\ell\)-subgroup is cyclic.  The inductive Alperin--McKay
+theorem for cyclic-defect blocks \cite{KoshitaniSpath2016} implies the
+required \(\IMK\) condition.
+
+\subsection{\texorpdfstring{The subgroup \(\M\) in the non-doubly-regular case}
+  {The subgroup M in the non-doubly-regular case}}
+
+In case (c), Cabanes and Sp{\"a}th pass to a twisted Frobenius
+\[
+  F'=\nu F_q
+\]
+and construct a generally disconnected maximal-rank algebraic subgroup
+\(\M\leq\G\), stable under \(F'\), such that
+\[
+  (\M^\circ)_{\mathrm{der}}
+  \text{ has type }
+  D_{l_1}\times D_{l_2},
+  \qquad
+  |\M/\M^\circ|=2.
+\]
+At fixed points,
+\[
+  M_0=G_1.G_2\trianglelefteq
+  M^\circ=(\M^\circ)^{F'}
+\]
+is a central product.  Only the distinguished factor \(G_j\) is
+guaranteed to have rank \(l_j\geq4\); the other can have low rank and
+need not be quasisimple.  The distinguished factor contains a Sylow
+\(d\)-torus with the same \(d\)-multiplicity as \(G\), and \(d\) is
+doubly regular there.  Thus its already proved correspondence can be
+transported into \(M=\M^{F'}\).
+
+The technical core is Clifford theory across
+\[
+  M_0=G_1.G_2
+   \trianglelefteq M^\circ
+   \trianglelefteq M,
+\]
+where
+\[
+  [M:M_0]=2\gcd(2,q-1);
+\]
+the quotient therefore has order \(4\) for odd \(q\), but order \(2\)
+for even \(q\).  Characters are partitioned according to their
+stabilizers and extension behavior.  Theorem 5.20 of
+\cite{CabanesSpath2026} constructs an \(E(M)\)-stable
+\(\widetilde M\)-transversal in \(\Irr(M)\), and its chosen characters
+extend to the required stabilizers.  In the exceptional case
+\(2\mid f\), \(\varepsilon=1\), and \(\varepsilon_1=-1\), the theorem
+also controls the central element \(h_0\): when \(h_0\in\ker(\chi)\), it
+chooses an extension with \(vF_q\) in its kernel.
+
+Proposition 6.3 transports the needed character correspondences using
+central isomorphisms of character triples.  Theorem 6.4 proves
+extendibility for the chosen transversal with respect to
+\(N\trianglelefteq\widehat N\), and Corollary 6.5 proves maximal
+extendibility for \(N\trianglelefteq\widetilde N\).  Propositions 6.7
+and 6.8 construct the required equivariant extension maps.  Theorem 6.9
+assembles these results for the normalizer of a Sylow \(d\)-torus in
+\(G\), proving:
+
+\begin{enumerate}
+  \item a \(\widehat N\)-stable \(\widetilde N\)-transversal of
+  \(\Irr(N)\), whose members extend to their stabilizers in
+  \(\widehat N\);
+  \item maximal extendibility for \(N\trianglelefteq\widetilde N\);
+  \item on a chosen \(\widehat N\)-stable
+  \(\widetilde C\)-transversal in \(\Irr(C)\), a
+  \(\widehat N\)-equivariant extension map for
+  \(C\trianglelefteq N\); and
+  \item a
+  \(\operatorname{Lin}(\widetilde N/N)\rtimes\widehat N\)-equivariant
+  extension map for
+  \(\widetilde C\trianglelefteq\widetilde N\), which also gives maximal
+  extendibility for that inclusion.
+\end{enumerate}
+
+The first item is \(\Ad\).  The second and fourth items give \(\Bd\);
+the third is the auxiliary extension map used in their construction.
+Therefore \cref{prop:local-criterion} applies in every
+non-doubly-regular case with \(a_{(\G,F)}(d)\geq2\).
+
+\begin{proposition}[Final type-\(D\) case]\label{prop:type-d}
+Let \(q\) be a prime power and let \(\ell\nmid 2q\) be prime.  Then
+\(\IMK\) holds for \(D_{l,\mathrm{sc}}^\varepsilon(q)\), for every
+\(l\geq4\) and \(\varepsilon\in\{1,-1\}\).
+\end{proposition}
+
+\begin{proof}
+For \(l=4\), use the rank-four clause of the doubly regular theorem.
+For \(l\geq5\), put \(d=d_\ell(q)\).  The cases \(d=1,2\) were already
+proved in the odd-degree/local-extension work
+\cite{MalleSpath2016}.  Thus assume \(d\geq3\) and apply the trichotomy.
+The doubly regular case follows from Theorem 4.1; the multiplicity-at-most
+one case has cyclic Sylow subgroup and follows from
+\cite{KoshitaniSpath2016}; the remaining case follows from Theorem 6.9
+and the local criterion.  These cases are exhaustive.
+\end{proof}
+
+This is Theorem 6.12 of \cite{CabanesSpath2026}.  Lemma 6.10 chooses the
+ranks, signs, and subgroup \(M\), and proves the Sylow-\(d\)-torus and
+normalizer containments in the twisted setup.  Lemma 6.11 constructs the
+conjugation/isomorphism transport back to the original \(F\)-fixed group.
+
+\section{Assembly of the full theorem}
+
+\begin{proof}[Proof of \cref{thm:mckay}]
+Fix a prime \(\ell\).  By the classification of finite simple groups,
+every nonabelian finite simple group is alternating, sporadic, or of Lie
+type.  The results in the table of Section 3 verify \(\IMK\) for the
+universal covers of all families except the remaining type-\(D\) cases.
+Those cases are supplied by \cref{prop:type-d}.  Hence the universal
+cover of every nonabelian finite simple group satisfies \(\IMK\) at
+\(\ell\).
+
+Apply the reduction theorem, \cref{thm:reduction}.  Every finite group
+now satisfies \(\IMK\) at \(\ell\).  Apply
+\cref{prop:imk-to-mckay} to obtain a bijection between
+\(\Irr_{\ell'}(X)\) and
+\(\Irr_{\ell'}(\Norm_X(S))\) for every finite \(X\) and
+\(S\in\Syl_\ell(X)\).  Taking cardinalities proves the equality.
+\end{proof}
+
+\section{Was a simpler proof available?}
+
+We searched the post-2024 literature and the cited character-correspondence
+literature for a proof that avoids the inductive condition or the
+classification.  No such proof of the theorem for \emph{all} finite
+groups was found.  The Annals authors themselves organize the result as
+the last step of a classification-based program
+\cite{CabanesSpath2026}.
+
+There are important simpler proofs in restricted settings:
+
+\begin{itemize}
+  \item the Okuyama--Wajima argument proves the blockwise height-zero
+  counting equality, hence McKay's equality, for \(p\)-solvable groups
+  \cite{OkuyamaWajima1980};
+  \item a modern equivariant version still assumes a \(p\)-solvable
+  quotient \cite{MaltempoVallejo2026};
+  \item the prime \(2\) admits a much more focused Harish--Chandra
+  analysis \cite{MalleSpath2016}; and
+  \item cyclic Sylow/defect cases follow from the cyclic-defect theory
+  \cite{KoshitaniSpath2016}.
+\end{itemize}
+
+None of these covers the non-\(p\)-solvable type-\(D\) families that
+constituted the final obstruction.  Treating a special-case proof as a
+general proof would therefore leave a genuine logical gap.  The proof
+above is the complete route documented by the cited primary literature:
+it compresses the classification work behind named theorems, but does
+not disguise or omit it.
+
+\section{Dependency summary}
+
+The logical spine of the argument is:
+\[
+\begin{gathered}
+\text{ordinary character theory and character triples}\\
+\Downarrow\\
+\text{family-specific equivariant bijections and extension maps}\\
+\Downarrow\\
+\IMK\text{ for every universal cover (CFSG case split)}\\
+\Downarrow\quad\text{\cite{IsaacsMalleNavarro2007,Rossi2023}}\\
+\IMK\text{ for every finite group}\\
+\Downarrow\quad\text{induction on }[X:\Norm_X(S)]\\
+|\Irr_{\ell'}(X)|
+=
+|\Irr_{\ell'}(\Norm_X(S))|.
+\end{gathered}
+\]
+
+\begingroup
+\footnotesize
+\bibliographystyle{alpha}
+\bibliography{references}
+\endgroup
+
+\end{document}
diff --git a/mckay-conjecture/docs/references.bib b/mckay-conjecture/docs/references.bib
new file mode 100644
index 00000000..dff3e90c
--- /dev/null
+++ b/mckay-conjecture/docs/references.bib
@@ -0,0 +1,292 @@
+@article{CabanesSpath2026,
+  author  = {Marc Cabanes and Britta Sp{\"a}th},
+  title   = {The {McKay} Conjecture on Character Degrees},
+  journal = {Annals of Mathematics},
+  volume  = {203},
+  number  = {3},
+  pages   = {933--1032},
+  year    = {2026},
+  doi     = {10.4007/annals.2026.203.3.5},
+  eprint  = {2410.20392},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{IsaacsMalleNavarro2007,
+  author  = {I. Martin Isaacs and Gunter Malle and Gabriel Navarro},
+  title   = {A Reduction Theorem for the {McKay} Conjecture},
+  journal = {Inventiones Mathematicae},
+  volume  = {170},
+  pages   = {33--101},
+  year    = {2007},
+  doi     = {10.1007/s00222-007-0057-y}
+}
+
+@article{Rossi2023,
+  author  = {Damiano Rossi},
+  title   = {The {McKay} Conjecture and Central Isomorphic Character Triples},
+  journal = {Journal of Algebra},
+  volume  = {618},
+  pages   = {42--55},
+  year    = {2023},
+  doi     = {10.1016/j.jalgebra.2022.12.004},
+  eprint  = {2204.10300},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{Malle2008,
+  author  = {Gunter Malle},
+  title   = {The Inductive {McKay} Condition for Simple Groups Not of Lie Type},
+  journal = {Communications in Algebra},
+  volume  = {36},
+  pages   = {455--463},
+  year    = {2008},
+  doi     = {10.1080/00927870701716090}
+}
+
+@article{Spath2012,
+  author  = {Britta Sp{\"a}th},
+  title   = {Inductive {McKay} Condition in Defining Characteristic},
+  journal = {Bulletin of the London Mathematical Society},
+  volume  = {44},
+  pages   = {426--438},
+  year    = {2012},
+  doi     = {10.1112/blms/bdr100},
+  eprint  = {1009.0463},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.GR}
+}
+
+@incollection{Spath2018,
+  author    = {Britta Sp{\"a}th},
+  title     = {Reduction Theorems for Some Global--Local Conjectures},
+  booktitle = {Local Representation Theory and Simple Groups},
+  series    = {EMS Series of Lectures in Mathematics},
+  publisher = {European Mathematical Society},
+  pages     = {23--61},
+  year      = {2018},
+  doi       = {10.4171/185-1/2}
+}
+
+@article{MalleSpath2016,
+  author  = {Gunter Malle and Britta Sp{\"a}th},
+  title   = {Characters of Odd Degree},
+  journal = {Annals of Mathematics},
+  volume  = {184},
+  pages   = {869--908},
+  year    = {2016},
+  doi     = {10.4007/annals.2016.184.3.6},
+  eprint  = {1506.07690},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{CabanesSpath2013,
+  author  = {Marc Cabanes and Britta Sp{\"a}th},
+  title   = {Equivariance and Extendibility in Finite Reductive Groups with Connected Center},
+  journal = {Mathematische Zeitschrift},
+  volume  = {275},
+  pages   = {689--713},
+  year    = {2013},
+  doi     = {10.1007/s00209-013-1156-7}
+}
+
+@article{CabanesSpath2017A,
+  author  = {Marc Cabanes and Britta Sp{\"a}th},
+  title   = {Equivariant Character Correspondences and Inductive {McKay} Condition for Type {A}},
+  journal = {Journal f{\"u}r die reine und angewandte Mathematik},
+  volume  = {728},
+  pages   = {153--194},
+  year    = {2017},
+  doi     = {10.1515/crelle-2014-0104},
+  eprint  = {1305.6407},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{CabanesSpath2017C,
+  author  = {Marc Cabanes and Britta Sp{\"a}th},
+  title   = {Inductive {McKay} Condition for Finite Simple Groups of Type {C}},
+  journal = {Representation Theory},
+  volume  = {21},
+  pages   = {61--81},
+  year    = {2017},
+  doi     = {10.1090/ert/497},
+  eprint  = {1612.03741},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{CabanesSpath2019,
+  author  = {Marc Cabanes and Britta Sp{\"a}th},
+  title   = {Descent Equalities and the Inductive {McKay} Condition for Types {B} and {E}},
+  journal = {Advances in Mathematics},
+  volume  = {356},
+  pages   = {106820},
+  year    = {2019},
+  doi     = {10.1016/j.aim.2019.106820},
+  eprint  = {1903.11667},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{Spath2023I,
+  author  = {Britta Sp{\"a}th},
+  title   = {Extensions of Characters in Type {D} and the Inductive {McKay} Condition, {I}},
+  journal = {Nagoya Mathematical Journal},
+  volume  = {252},
+  pages   = {906--958},
+  year    = {2023},
+  doi     = {10.1017/nmj.2023.14},
+  eprint  = {2109.08230},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{Spath2025II,
+  author  = {Britta Sp{\"a}th},
+  title   = {Extensions of Characters in Type {D} and the Inductive {McKay} Condition, {II}},
+  journal = {Inventiones Mathematicae},
+  volume  = {242},
+  pages   = {45--122},
+  year    = {2025},
+  doi     = {10.1007/s00222-025-01354-9},
+  eprint  = {2304.07373},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{KoshitaniSpath2016,
+  author  = {Shigeo Koshitani and Britta Sp{\"a}th},
+  title   = {The Inductive Alperin--{McKay} and Blockwise Alperin Weight Conditions for Blocks with Cyclic Defect Groups and Odd Primes},
+  journal = {Journal of Group Theory},
+  volume  = {19},
+  pages   = {777--813},
+  year    = {2016},
+  doi     = {10.1515/jgth-2016-0006},
+  eprint  = {1310.5512},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@article{Malle2007,
+  author  = {Gunter Malle},
+  title   = {Height 0 Characters of Finite Groups of Lie Type},
+  journal = {Representation Theory},
+  volume  = {11},
+  pages   = {192--220},
+  year    = {2007}
+}
+
+@article{BroueMalle1992,
+  author  = {Michel Brou{\'e} and Gunter Malle},
+  title   = {Th{\'e}or{\`e}mes de {Sylow} G{\'e}n{\'e}riques pour les Groupes R{\'e}ductifs sur les Corps Finis},
+  journal = {Mathematische Annalen},
+  volume  = {292},
+  pages   = {241--262},
+  year    = {1992}
+}
+
+@article{BroueMalleMichel1993,
+  author  = {Michel Brou{\'e} and Gunter Malle and Jean Michel},
+  title   = {Generic Blocks of Finite Reductive Groups},
+  journal = {Ast{\'e}risque},
+  volume  = {212},
+  pages   = {7--92},
+  year    = {1993}
+}
+
+@book{Navarro2018,
+  author    = {Gabriel Navarro},
+  title     = {Character Theory and the {McKay} Conjecture},
+  publisher = {Cambridge University Press},
+  year      = {2018}
+}
+
+@book{Isaacs1976,
+  author    = {I. Martin Isaacs},
+  title     = {Character Theory of Finite Groups},
+  publisher = {Academic Press},
+  year      = {1976}
+}
+
+@book{MalleTesterman2011,
+  author    = {Gunter Malle and Donna Testerman},
+  title     = {Linear Algebraic Groups and Finite Groups of Lie Type},
+  publisher = {Cambridge University Press},
+  year      = {2011}
+}
+
+@article{OkuyamaWajima1980,
+  author  = {Tetsuro Okuyama and Masayuki Wajima},
+  title   = {Character Correspondence and {$p$}-Blocks of {$p$}-Solvable Groups},
+  journal = {Osaka Journal of Mathematics},
+  volume  = {17},
+  number  = {3},
+  pages   = {801--806},
+  year    = {1980},
+  doi     = {10.18910/5457}
+}
+
+@article{MaltempoVallejo2026,
+  author  = {Adele Maltempo and Carolina Vallejo},
+  title   = {The {McKay} Conjecture with Group Automorphisms and the {Okuyama--Wajima} Argument},
+  journal = {Journal of Pure and Applied Algebra},
+  volume  = {230},
+  number  = {1},
+  pages   = {108155},
+  year    = {2026},
+  doi     = {10.1016/j.jpaa.2025.108155},
+  eprint  = {2512.13406},
+  archivePrefix = {arXiv},
+  primaryClass  = {math.RT}
+}
+
+@misc{Mathlib,
+  author       = {{Mathlib Community}},
+  title        = {Mathlib},
+  howpublished = {\url{https://github.com/leanprover-community/mathlib4}},
+  note         = {Inspected at commit 9cebae57f419f984d008f357605b2621a1d9f13b},
+  year         = {2026}
+}
+
+@misc{OddOrderLean,
+  author       = {Yawara Ishida and contributors},
+  title        = {OddOrder: finite group and ordinary character theory in Lean},
+  howpublished = {\url{https://github.com/yawara/odd-order}},
+  note         = {Inspected at commit 0bff8689b6f1090e64c4230e45a55f4ed7b71d13},
+  year         = {2026}
+}
+
+@misc{LeanPool,
+  author       = {Vasil Vasilev and contributors},
+  title        = {lean-pool},
+  howpublished = {\url{https://github.com/Vilin97/lean-pool}},
+  note         = {Inspected at commit ea6540439a2ff9e8b4ab6314e8507b0649761efd},
+  year         = {2026}
+}
+
+@misc{TauCeti,
+  author       = {{Tau Ceti Project}},
+  title        = {TauCeti},
+  howpublished = {\url{https://github.com/TauCetiProject/TauCeti}},
+  note         = {Inspected at commit 3096557b3362bc9d7a6ecbc0d253072ec750683a},
+  year         = {2026}
+}
+
+@misc{QiuzhenCFSG,
+  author       = {{Qiuzhen CFSG Project}},
+  title        = {{CFSG}: a formalization project for the classification of finite simple groups},
+  howpublished = {\url{https://github.com/Qiuzhen-CFSG/CFSG}},
+  note         = {Inspected at commit 2519b281516d7e26de9891fd00f88ef7668e9706; no repository license was present},
+  year         = {2026}
+}
+
+@misc{TNLean,
+  author       = {{TNLean contributors}},
+  title        = {{TNLean}},
+  howpublished = {\url{https://github.com/LionSR/TNLean}},
+  note         = {Inspected at commit 585319610d94eaa8c2b4b453097790c1b1bf6068},
+  year         = {2026}
+}