feat: add the representation theory roadmap family

[kim-em]

This PR adds a family of eleven representation-theory roadmaps under TauCetiRoadmap/RepresentationTheory/ The family covers:

• semisimple algebras and Artin-Wedderburn structure theory
• the character theory of finite groups, up to the Burnside-Dixon-Schneider algorithm that computes character tables over an exact cyclotomic type
• induction, restriction, and Mackey theory, with Artin and Brauer induction, projective representations, and the Schur multiplier
• root systems, Weyl groups, and the Cartan-Killing classification
• the highest-weight theory of semisimple Lie algebras through the Weyl character and dimension formulas, the Harish-Chandra isomorphism, and the explicit construction of the exceptional algebras
• the finite-dimensional representations of the classical groups, with the Weyl construction, Schur polynomials, and Gelfand-Tsetlin bases, the symmetric group, Specht modules, and Schur-Weyl duality for the general linear, orthogonal, and symplectic groups
• compact groups, Haar measure, and the Peter-Weyl theorem
• Lie groups and the Lie algebra correspondence
• Clifford algebras, the Pin and Spin groups, and the spin representations that supply the fundamental representations of types B and D
• quiver representations, Gabriel's theorem, and Auslander-Reiten theory.

The roadmaps cite the neighbouring reductive-groups, orthogonal-L2-bases, pivotal-spherical, and Temperley-Lieb roadmaps where relevant.

🤖 Prepared with Claude Code

[mrdouglasny]

This is a supervised, question-driven review; the blocking items are below, full analysis available in https://github.com/mrdouglasny/TauCeti-reviews-pr62.

🤖 Models Claude Opus 4.8 and Codex (GPT-5.6) suggest:

**Overall the family is strong and largely formalization-ready: the mathematics, layering, references (cited per-layer in every roadmap), and Mathlib-overlap accounting are consistently accurate. The systematic risk is signature faithfulness — Suggested.lean targets that would build green while being false or vacuous. We found 15 such blocking defects across 9 of the 11 roadmaps (only SchurWeyl and RootSystems are blocking-free), plus ~26 should-fix items and 4 coverage requirements. Every blocking item below was adversarially verified (Codex, with counterexamples).

🔴 Blocking (false or vacuous as written)

• SpinRepresentations
  • card_ker_spinToSpecialOrthogonal — false in dimension 0 (V=0 ⇒ Pin/Spin and SO(0) trivial ⇒ kernel is 1, not 2).
  • soEquivBivector — false in characteristic 2 (R=𝔽₂, n=1: ⋀²R=0 but so(1,𝔽₂)≅𝔽₂); needs ≃ₗ⁅R⁆ + [Invertible 2].
  • spinAction/spinRep — target can be empty (W=0: no unital Mat₂(ℂ)→ℂ); needs a maximal-isotropic polarization.
• CharacterTheory
  • irreducibleCharacters_span — false: irreducible characters span ClassFunction, not all of G→k (⊤ ≤ span fails for nonabelian G).
  • classMultMatrix vs centralCharacterTable_eigenvector — transpose mismatch (a(i,k,j) vs a(i,j,k); S₃ witness a_{T,T,C}=3 ≠ a_{T,C,T}=2).
  • characterPairing_nondegenerate — false if char ∣ |G| (pairing ≡ 0); needs [Invertible (card G : k)].
• QuiverRepresentations
  • dimVector_reflectionFunctor — vacuous: IsEmpty (Sᵢ ⟶ M) is unsatisfiable in a preadditive category.
  • exists_projectiveCover — false over arbitrary [Ring A] (needs semiperfect/Artinian).
  • exists_almostSplitSequence — false on the whole functor category (AR existence is for finitely-presented reps; Paquette 2011).
• ClassicalGroups — schurFunctor_iso_irreducible, character_irreducible_eq_schurPoly, and gtPatternEquivSSYT all false without the row bound ℓ(μ) ≤ n.
• InductionRestriction — brauer_characterization false without a class-function hypothesis, even over ℂ (S₃ counterexample); the splitting-field fix alone does not repair it.
• SemisimpleAlgebras — card_blocks_eq false: zero-size Wedderburn blocks break the count (needs ∀ i, NeZero (d i)).
• LieHighestWeight — sl2_finrank_of_hasPrimitiveVector / sl2_irreducible_ext false without "the triple spans L" (sl₃-adjoint counterexample).
• CompactGroups — schur_orthogonality_self false (conjugation on the wrong factor under Mathlib's inner-product convention).
• LieGroups — weyl_integration_formula false: μG, μT, weylDensity are free unconstrained parameters.

🟠 Should-fix and coverage (detail in the bundle)

~26 should-fix items (missing hypotheses, vacuous Prop := sorry anti-vacuity predicates, too-weak isos), plus four coverage requirements written up as standalone notes: (1) pin the representation ring R(G) + injective character ring-hom (tensor-product decomposition currently has no spec — only the additive shadow is pinned); (2) pin the executable character-table summit's cyclotomic bridge (Cyclotomic e / embedding / lift); (3) extend the Frobenius–Schur reality trichotomy to compact groups (present for finite groups only — needed for spinor/matter reality types); (4) add a "Scope & boundaries" paragraph to the family README (the deliberate exclusions — modular theory, noncompact rep theory, affine types — are nowhere stated).

Recurring themes: faithfulness-over-falsity (a green build won't catch these); unpinned cross-roadmap interfaces promised in prose but not machine-checked; and Prop := sorry predicates that leave a summit only as strong as an unwritten definition.

📦 Full analysis (linked)

Supporting material — too long for this comment — is at https://github.com/mrdouglasny/TauCeti-reviews-pr62:

• reviews/ — per-roadmap findings (blocking + should-fix + notes) and the family synthesis; 01_INDEPENDENT_ADVERSARIAL_AUDIT.review.md is Codex's independent audit.
• VERIFICATION.md — Codex's counterexample-level verification of the original blockers.
• OVERVIEW.md — structures defined, Lean design choices, one major theorem per roadmap, and a per-definition universal-property / canonicity scorecard.
• DEFINITIONS.md — a checklist of all 238 defs, each linking to its exact source line.
• APPLICATIONS.md / APPLICATIONS_AG.md — a downstream-support audit (mathematical physics; algebraic geometry, Fulton–Harris) of whether the foundations expose what good downstream definitions will need.
• comments/ — the four coverage requirements above, as postable notes.
• roadmaps/ — the reviewed PR #62 snapshot (head 37f34c8), so each review sits next to the roadmap it reviews.

Happy to discuss or open per-finding threads.

[kim-em]

Thanks Michael — this is a genuinely valuable review, and the bundle format (per-roadmap findings + counterexample-level verification + postable coverage notes) made it directly actionable. Everything below is now on the branch: all 15 blocking findings (17 targets), the confirmed should-fixes, all four coverage requirements, the minor findings, and — since the roadmap-writing guide now forbids the pattern (#64) — real bodies for all 25 def _ : Prop := sorry predicates, not only the load-bearing ones. lake build is green; a second adversarial pass (Codex, ~130k tokens, same "would it build green while false" standard as your review) was then run over the full remediation diff — it confirmed the focal repairs (the ᵥ* eigenrow computation, IsCharacterTableSpec adequacy, the polarization data's satisfiability, the Weyl density, the restricted-sl₂ instance meaning, the Tits sign) and caught 11 residual defects in our own newly authored targets, all fixed in a final commit and folded into the descriptions below. One commit per roadmap; dispositions below, with the three places we adopted a different repair than prescribed called out explicitly.

Blocking findings

🤖 Claude+Codex say: SpinRepresentations card_ker_spinToSpecialOrthogonal — fixed as prescribed: 0 < finrank ℂ V added, docstring records why (V = 0 gives kernel 1).

🤖 Claude+Codex say: SpinRepresentations soEquivBivector — fixed, with the repair upgraded beyond the prescription: [Invertible (2 : R)] added and the equivalence upgraded to ≃ₗ⁅R⁆, but a LieEquiv needs a named bracket on ⋀², so the bracket is defined on the Clifford-commutator side (scoped bivectorLieRing/bivectorLieAlgebra instances) — transporting so's bracket backwards would have made the Lie equivalence tautological — and the advertised action-normalization lemma is pinned (soEquivBivector_wedge_mulVec, with the polar-convention factor 2 explicit).

🤖 Claude+Codex say: SpinRepresentations spinAction/spinRep — fixed, repair upgraded: a bare maximal-isotropic W hypothesis is still underspecified (the action of a general v needs the W'/line components), so a SpinPolarizationData Q structure now bundles W, a complementary isotropic W' in perfect polar-pairing, and the anisotropic line for odd dimension, threaded through spinAction, spinRep, spinPlus, spinPlus_invariant, spinRep_isIrreducible_of_odd, and the dimension targets.

🤖 Claude+Codex say: CharacterTheory irreducibleCharacters_span — fixed as prescribed: conclusion is now ClassFunction k G ≤ span …, and ClassFunction itself (previously a Submodule := sorry, which could have re-vacuized the repaired statement) now has its real conjugacy-invariant body.

🤖 Claude+Codex say: CharacterTheory classMultMatrix vs centralCharacterTable_eigenvector — the inconsistency is real and is fixed, but we adopted the other valid repair: the matrix convention (Mᵢ)ⱼₖ = aᵢₖⱼ is kept and the eigen-relation is restated on row vectors via ᵥ* — with vⱼ = ω(Kⱼ), (v ᵥ* Mᵢ)ₖ = Σⱼ ω(Kⱼ) aᵢₖⱼ = ω(Kᵢ)ω(Kₖ) by the coordinate identity and commutativity of the class algebra, so the rows of Ω are common left eigenvectors. As your verification itself noted, neither declaration is false in isolation — it is a convention choice; it is now pinned in the classMultMatrix docstring, swept through IsCharacterTableSpec.row_eigen, normalized_eigenrow_iff_algHom, and the README ("columns" → "rows/left" everywhere), with an explicit do-not-mix warning.

🤖 Claude+Codex say: CharacterTheory characterPairing_nondegenerate — fixed: [Invertible (Nat.card G : k)] added (spelled with Nat.card to match the pairing; the file's Invertible (Fintype.card …) hypotheses were normalized to Nat.card throughout for one consistent spelling).

🤖 Claude+Codex say: QuiverRepresentations dimVector_reflectionFunctor — fixed: the unsatisfiable IsEmpty hom-type guard is replaced by the biproduct no-summand form ¬ ∃ N, Nonempty (M ≅ simpleRep k Q i ⊞ N) (which also sidesteps the sink/source orientation trap your verification flagged in the retract formulation), and the sink hypothesis is now part of reflectionFunctor's signature.

🤖 Claude+Codex say: QuiverRepresentations exists_projectiveCover — fixed as prescribed: stated over a finite-dimensional algebra ([Field k] [Algebra k A] [FiniteDimensional k A]), with the ℤ/2-over-ℤ failure recorded in the docstring.

🤖 Claude+Codex say: QuiverRepresentations exists_almostSplitSequence — fixed, repair upgraded per the second opinion: a finiteness hypothesis on M alone would not have left the full functor category, so a pointwise-finite-dimensionality predicate IsFinDim now scopes the entire AR layer — IsAlmostSplit is a real Prop-structure (short exactness, non-splitness, indecomposable endpoints, left/right almost-split lifting) whose lifting quantifiers are themselves restricted to finite-dimensional objects, matching the Paquette counterexample precisely.

🤖 Claude+Codex say: ClassicalGroups schurFunctor_iso_irreducible / character_irreducible_eq_schurPoly / gtPatternEquivSSYT — fixed as prescribed: μ.colLen 0 ≤ n added to all three, weightOfShape's intended domain pinned in its docstring.

🤖 Claude+Codex say: InductionRestriction brauer_characterization — fixed as prescribed: conjugacy-invariance hypothesis (stated inline so the file does not hard-depend on CharacterTheory's ClassFunction) and [IsAlgClosed k], with your S₃ counterexample recorded; IsElementary has its real p-elementary body (internal direct product of a cyclic prime-to-p part and a p-group via IsComplement' + commutation).

🤖 Claude+Codex say: SemisimpleAlgebras card_blocks_eq — fixed as prescribed: [∀ i, NeZero (d i)] on both presentations, docstring records the zero-block padding failure and extends the caveat to any chosen-presentation object.

🤖 Claude+Codex say: LieHighestWeight sl2_finrank_of_hasPrimitiveVector / sl2_irreducible_ext — the finding is accepted (your sl₃-adjoint counterexample is airtight, and the section header's "applies verbatim to root triples" claim is corrected), but we adopted the minimal repair your verification itself identified rather than htop: sl2_finrank… hypothesizes irreducibility over t.toLieSubalgebra K (of which htop is the special case), and — one step further, from our own second opinion — sl2_irreducible_ext concludes the equivalence over the subalgebra (≃ₗ⁅K, t.toLieSubalgebra K⁆), since restricted irreducibility cannot force an L-equivalence (the actions outside the sl₂ may differ); the L-level statement is recorded as the htop specialization.

🤖 Claude+Codex say: CompactGroups schur_orthogonality_self — fixed as prescribed: conjugation moved to the first factor, the S¹ scalar check and Mathlib's first-slot convention recorded in the docstring, with the note that the basis form hides the misplacement (real Kronecker deltas) — which is exactly why the coordinate-free form needed the pin.

🤖 Claude+Codex say: LieGroups weyl_integration_formula — fixed as prescribed, in full: μG/μT are pinned as normalized Haar (IsHaarMeasure + IsProbabilityMeasure), and weylDensity is now a real definition — |det_ℝ((Ad(t⁻¹) − 1) on 𝔤/Lie(T))| via Submodule.mapQ, with the descent lemma (ad_lieSubalgebraOfSubgroup_le), continuity companion, and the positive-root identity ∏_{α>0}|1−α(t)⁻¹|² recorded; weylGroup is now really N(T)/T (the Group instance is automatic via Subgroup.normal_in_normalizer). Stated first for continuous class functions per the second opinion; the Integrable generalization is a corollary.

The 25 predicate bodies

🤖 Claude+Codex say: every def _ : Prop := sorry in the family now has a real body or became a Prop-structure/data-structure with documented fields — the count is 25, not ~24 (the multiline IsPeterWeylBasis evades line-oriented grep; verified with rg -U ': Prop\s*:=\s*sorry', which now returns nothing). Highlights beyond those above: IsCharacterTableSpec is a Prop-structure (degrees, Σd² = |G|, weighted row orthonormality, the ᵥ* eigenrow field) together with the new normalized_eigenrow_iff_algHom lemma making the uniqueness argument visible (eigenrows = class-algebra homomorphisms); IsIrrepSkeleton/IsPeterWeylBasis carry the Schur-style inequivalence/exhaustiveness and the element-level √d-normalized matrix-coefficient identity the README demanded; IsMaximalTorus is the purely topological maximal-compact-connected-abelian predicate; the Lie-subgroup notions became Nonempty of data structures (EmbeddedLieSubgroupData with topological embedding + injective mfderiv; ImmersedLieSubgroupData with a separate leaf-topology carrier, which a bare Subgroup genuinely cannot express); and the Iwasawa cluster became CartanInvolution (with reductivity fields — our second opinion caught that a smooth involution with compact fixed set does not characterize reductivity: the Euclidean motion group is a counterexample) plus IwasawaData (fixed subgroup K, maximal abelian 𝔞 ⊆ 𝔭, A = exp 𝔞, closed nilpotent N completing the Lie-algebra Iwasawa complement, chamber cone), with the old predicate names kept as existential wrappers so the decomposition theorems' shapes are stable.

Should-fix and minor findings

🤖 Claude+Codex say: all confirmed should-fixes are applied: the equivariant schurWeylDecomposition and the algebra-map faithfulness target (permActionAlgHom + injectivity at the honest n ≤ d threshold); Dominates/standardCount/youngSubgroup combinatorial pins; character_galois_pow with one σ for all g; the GL₂ cuspidal degree-2 and θ-regularity hypotheses; rat_rep_iso_of_res_cyclic restated on averaged fixed-point sums (the earlier hypothesis was equivalent to global character equality); Brauer/Artin aligned with the algebraically-closed char-0 regime; the Clifford character-form witnesses pinned (e ≠ 0, reps a genuine transversal of the inertia group); exists_chevalleySystem bundling root-space membership, ⁅eᵢ,fᵢ⁆ = coroot, and eigenvalue relations; the Harish-Chandra ρ-shift dropped so the raw ξ targets the dot-invariants consistently; Verma universal property (restated after the second pass as unique factorization through the named vermaHighestWeightVector — the first phrasing was satisfied by φ = 0) and the L(λ)-has-a-highest-weight-vector anti-vacuity pin, plus the transposed Cartan matrix in serre_presentation_equiv (Mathlib's cartanMatrix i j = αᵢ(hⱼ) against Matrix.ToLieAlgebra's bracket convention — the Bₙ/Cₙ swap, caught by the second pass); the machine-pinned quiver ↔ root-system bridge (exists_rootPairing_titsForm: symmetrized Tits Gram = base Cartan matrix, roots = Tits-form-1 vectors) with [IsAlgClosed k] dropped from the field-independent simply-laced Gabriel targets; Morita admissibility (rad^N ⊆ ker f ⊆ rad²) with the Ext-quiver companion named; the LieGroups de-vacuizations (exists_complexification with injectivity + universal property; exists_holomorphic_extension against complexification data including the universal property — the second pass showed injective continuous ι alone is not enough, via U(1) ⊂ SL₂(ℂ); and bruhat_decomposition now consuming an IsTitsSystem Prop-structure of elementary BN-pair axioms, statable with no reductive API yet sufficient for the decomposition — with a bare section over N(T)/T a self-normalizing B = T still falsified it); and the Layer-8/9 summit pins (Borel–Weil module structure + translation representation + the borelWeilSpaceAlg equivariant-embedding anti-vacuity pin — the finite-dimensionality/irreducibility statements we first wrote over arbitrary (Gc, B, lam) were themselves false-or-vacuous per the second pass, so those summit halves return to the README until reductive/dominance hypotheses are expressible, one place where your original prescription could not be carried out faithfully yet; the global Cartan polar decomposition; the one-parameter-subgroup bijection). The second pass also hardened IwasawaData (N connected and exponential-of-its-algebra, exp injective on 𝔞 — ruling out a ℤ-in-ℝ counterfeit — and a spanning chamber, with kakDecomposition drawing K and the chamber from the same datum) and the quiver AR layer ([Nonempty Q] on the root-pairing bridge, a finite path algebra on AR existence, the tau_iso field connecting IsAlmostSplit to arTranslate, and the uniqueness companion almostSplitSequence_unique). The minor findings are all applied too (arTranslate as an object-level operation, GT-generator indexing reconciliation, finrank_exteriorAlgebra renaming with the rep-level corollary, ContinuousLinearMap.finite_dimensional_eigenspace citation, README fixes including the ⟨Ind 1, Ind 1⟩ double-coset formula, Bourbaki/FH chapter corrections, Quiver.Symmetrify, and the SemisimpleAlgebras README target-list reconciliation).

🤖 Claude+Codex say: three review suggestions turned out not to hold when checked against the elaborator, and are documented in place rather than applied: mackeyDecomp's [HasFiniteBiproducts] instance is required (removal fails instance synthesis); IndRes Layer 7's universe-0 pin is forced by groupCohomology over ℤ (polymorphizing fails); and the two file-scope set_option backward.isDefEq.respectTransparency false are load-bearing (checked by removal) — each now carries an annotation, including the note that the built library must thread transparency explicitly since TauCeti/ bans set_option.

Coverage requirements

🤖 Claude+Codex say: representation ring — CharacterTheory Layer 4b pins repRing k G as a CommRing in characteristic zero with the character ring homomorphism into class functions and its injectivity over a char-0 splitting field (the AddSubgroup shadow stays for positive characteristic, per your note), and LieHighestWeight pins formalCharacter_tensor, the multiplicativity that makes the formal character the Grothendieck-ring homomorphism into ℤ[X].

🤖 Claude+Codex say: cyclotomic bridge — Cyclotomic e now carries its ring structure and generator, cyclotomicEmbedding is a ring hom with injectivity and the primitive-root pin, cyclotomicRingEquiv : Cyclotomic e ≃+* CyclotomicRing e ℤ ℚ (with NeZero e, discharged in application by the finite-group exponent), and liftCyclotomic_spec pins the lift — stated (after the second pass caught that unconditional existence is false for bound = 0 with nonzero residues) conditionally on an admissible witness, which the lift then uniquely returns; cyclotomicReduce_gen pins the reduction at the generator, and the review's low-confidence caveat about Dixon 1967's exact constant is recorded on DixonPrimeData.large. The second pass also confirmed 2·bound < p is exactly the right window and that orderOf α = e (not mere divisibility) is required.

🤖 Claude+Codex say: compact Frobenius–Schur — CompactGroups Layer 6b adds the Haar-integral indicator, the trichotomy, the orthogonal/symplectic invariant-form characterizations, and the structure-map (J² = ±1) reality criterion, with the wording restricted to compact groups per the audit correction; LieHighestWeight pins the −w₀λ = λ self-duality criterion (via invariant forms, with w₀ characterized chamber-to-negative-chamber so no length function is imported) and the exact Tits-sign criterion (−1)^{⟨λ,2ρ^∨⟩} separating real from quaternionic.

🤖 Claude+Codex say: scope & boundaries — the family README now has the section, with the audit-corrected wording: the exclusions are modular finite-group representation theory (not "characteristic zero" wholesale — SemisimpleAlgebras/Quiver work over general fields, the IndRes functorial layer over commutative rings), noncompact unitary representation theory (noncompact structure theory stays, since the compact theory consumes it), and affine/Kac–Moody root systems.

The two rejected findings

🤖 Claude+Codex say: lieSubalgebraOfSubgroup's totality and the NormedSpace.exp signatures are unchanged, per the audit's own withdrawal of those findings (the README's NormedSpace.exp ℝ spelling is modernized, as the audit suggested instead).

Ready for re-review — happy to open per-finding threads on anything above, especially the three divergent repairs (the ᵥ* convention choice, the minimal sl₂ hypothesis, and the polarization/AR-subcategory upgrades).

🤖 Prepared with Claude Code

[mrdouglasny]

Re-reviewed the remediation on bb664ecd — this is a thorough, faithful pass and I'm approving. I re-verified the parts most likely to hide a regression (the three divergent repairs, the 25 de-vacuized predicates, and the returned-to-README summit); everything holds.

The three divergences you flagged — all confirmed sound, and two are improvements on what the review prescribed:

1. ᵥ* row/left-eigenvector convention — correct and internally consistent. Keeping (Mᵢ)ⱼₖ = aᵢₖⱼ and restating on rows gives (v ᵥ* Mᵢ)ₖ = Σⱼ ω(Kⱼ)aᵢₖⱼ = ω(Kᵢ)ω(Kₖ), so the rows are common left eigenvectors — exactly the alternative the verification noted was equally valid. IsCharacterTableSpec is a genuine 4-field spec and normalized_eigenrow_iff_algHom makes uniqueness an argument. 👍

2. Minimal sl₂ hypothesis — sound, and more careful than the htop I suggested: irreducibility over t.toLieSubalgebra K (the sl₃-adjoint counterexample confirms ambient-L fails), with sl2_irreducible_ext correctly weakened to a subalgebra-equivalence since an L-equivalence would be false under the restricted hypothesis. The htop specialization is the right way to keep the L-level statement. 👍

3. Polarization / AR-subcategory upgrades — both genuinely stronger and counterexample-matched: SpinPolarizationData supplies exactly what spinAction needs to be well-defined, and IsAlmostSplit's lifting quantifiers restricted to IsFinDim objects match Paquette 2011 precisely (with tau_iso + the added almostSplitSequence_unique). 👍

Also verified: all former def _ : Prop := sorry predicates now carry genuine, parameter-constraining bodies (rg -U ': Prop\\s*:=\\s*sorry' is empty; the Nonempty <Data> predicates witness structures with real proof fields, not trivial inhabitants); and the Borel–Weil summit over arbitrary (Gc, B, lam) is honestly reclassified to LieGroups/README.md (only the carrier + the borelWeilSpace_embeds anti-vacuity pin remain in Lean), which is the right call under the omit-rather-than-pin-falsely convention.

No residual blocking or should-fix findings on the current head. Nice work — and the second adversarial pass catching 11 of its own residuals is exactly the standard we want.