lean-formalization

name	lean-formalization
description	Use when working on Phase 3 formalization — translating mathematical text into Lean 4 statements and proofs, or filling sorry placeholders.
allowed-tools	Read, Edit, Write, Bash, Glob, Grep

Lean Formalization Skill

Patterns for formalizing mathematics textbooks into Lean 4 with Mathlib. Derived from Phase 2 analysis of 583 items across 10 chapters of Etingof's Representation Theory.

Session Setup

Before the first lake build or lake env lean in any session:

lake exe cache get

This downloads pre-built Mathlib oleans. Skipping it triggers a full Mathlib rebuild (1800+ jobs).

To read a Mathlib lemma's exact signature, don't assume .lake/packages/mathlib is under your own worktree — a per-agent worktree often has none, and the shared checkouts under sibling worktrees get garbage-collected mid-session (a path that grepped fine minutes ago vanishes). Re-resolve each time with find <project-root> -path '*/packages/mathlib/Mathlib/<Dir>/<File>.lean' | head -1, or just verify signatures against the compiler (example : <sig> := by exact? / a scratch #check) rather than trusting a cached source path.

Never cd into .lake/packages/mathlib (or any subdir) — read absolute paths from the worktree root instead. The shell's cwd persists across Bash calls, and .lake/packages/mathlib is itself a lake project: once cwd is inside it, lake build EtingofRepresentationTheory.<Module> fails with a confusing "unknown target", and a bare lake build silently builds Mathlib and reports success — a green build that never touched your project. If builds report "unknown target" or an unexpected job count, run pwd and cd back to the worktree root before trusting any result.

Typecheck with lake build EtingofRepresentationTheory.<Module>, NOT lake env lean <file>. lake env lean does not apply the lakefile's [leanOptions] — in particular maxSynthPendingDepth = 3 (lakefile.toml; the Lean default is 2). Deep instance chains in this project (e.g. the Subalgebra → Module.End centralizer-module instances: Module ↥(centralizer A) (V →ₗ[A] E) from centralizerModuleHom) need depth 3, so under lake env lean they throw spurious synthInstanceFailed errors that do not occur under lake build. If a file fails lake env lean with instance-synthesis errors on centralizer/Subalgebra hom-spaces but you suspect the proof is fine, re-check with lake build <Module> before debugging — the on-main file fails lake env lean too. (Some places below still say lake env lean; prefer lake build when the file uses these instances.)

Reading background-build results: grep the teed log for error:, do not trust a wrapper's exit code or tail. lake build prints Lean errors before the final Build completed / ✖ summary, so ... | tee log | tail -40 can hide them, and a separate poller/sleep-loop you spawn to wait has its own exit status unrelated to the build's. Always confirm success by grep -nE "error:|✖|Build completed" log on the full teed file (and check #print axioms for sorryAx) — never infer "build passed" from a poller returning exit 0.

Build-environment recovery (shared .lake/packages across pod worktrees):

• Lean exited with code 139 (SIGSEGV) on dependency files you did not touch has two distinct causes. (a) Corrupted Mathlib oleans from a concurrent lake exe cache get writing the shared dir — fix with lake exe cache get!, then rebuild. (b) Memory pressure from build parallelism — if the SAME heavy file builds fine in isolation (lake build EtingofRepresentationTheory.Chapter5.<File>) but segfaults during a big parallel build, it is OOM, not corruption. Build the heavy files one at a time, then the target.
• failed to read file '...olean', incompatible header means main bumped the Lean toolchain mid-session. lake exe cache get only fetches Mathlib oleans, NOT the upstream deps (batteries/aesop/Qq/importGraph/Cli/plausible) — those keep old-toolchain oleans and keep throwing incompatible header. Recovery order:
  1. git fetch origin main; if origin/main:lean-toolchain changed, rebase onto origin/main.
  2. The shared .lake/packages/mathlib checkout itself can lag the manifest (lake update may not move it): grep -A2 '"name": "mathlib"' lake-manifest.json for the pinned rev, then git -C .lake/packages/mathlib checkout <rev> so its lean-toolchain matches the project.
  3. lake exe cache get, then rebuild the stale upstream deps (lake build Batteries Aesop ..., or just build your target and let lake regenerate them).
• A stale session in another worktree still on the pre-bump toolchain can rebuild the shared dep oleans back to the old version, re-corrupting your build in a loop. Check pgrep -fl 'v4.28' (the old version); if a lake/lean from an obsolete worktree is running, terminate that specific PID (targeted, not pkill).

Pre-Flight Checklist (Before Starting Any Proof)

Run this checklist before writing a single tactic. Skipping it has caused agents to waste entire context windows on dead-ends.

1. Check Known Dead-Ends. Scan the "Known Dead-Ends" section below. If your proof requires any of these patterns, sorry it immediately and move on:

   • ExteriorAlgebra ↔ PiTensorProduct bridging
   • if-branching obj fields in QuiverRepresentation-like structures — NOT a dead-end for reasoning about a single fibre (#6160, simpleRep_isIrreducible in Chapter3/Problem3_9_3.lean). Gotcha: for simpleRep i whose obj v := Fin (if v = i then 1 else 0) → k, the fibre (simpleRep i).obj i is defeq to Fin (if i = i then 1 else 0) → k but NOT to Fin 1 → k — the if is stuck because the Decidable (i = i) from an abstract [DecidableEq Q] never reduces to isTrue. Consequences: (a) instance search cannot find AddCommGroup ((simpleRep i).obj i) / finrank-lemmas since .obj i is not syntactically a Pi; (b) is_simple_module_of_finrank_eq_one apply fails to unify the bundled instAddCommMonoid against AddCommGroup.toAddCommMonoid. Fix: keep the honest stuck-if type — build an identity LinearEquiv e : (simpleRep i).obj i ≃ₗ[k] (Fin (if i = i then 1 else 0) → k) (all fields fun _ => rfl; target is syntactically a Pi, so TC finds AddCommGroup/Pi.module), get IsSimpleOrder (Submodule k (Fin (if i = i then 1 else 0) → k)) from is_simple_module_of_finrank_eq_one (by simp [Module.finrank_fin_fun]), then transport the eq_bot_or_eq_top dichotomy back with Submodule.orderIsoMapComap e (f.injective (by rw [h, map_bot])). Off-vertex fibres Fin 0 → k are Subsingleton (submodules are ⊥/⊤ via Submodule.eq_bot_iff/eq_top_iff' + Subsingleton.elim). The full round-trip (reflectionFunctor compositions) below remains a dead-end.
   • Abstract ρ : QuiverRepresentation k Q (not simpleRep): finrank/simple-module API needs AddCommGroup on every carrier — install it once with acg. The obj carriers bundle only AddCommMonoid, so isSimpleModule_iff_finrank_eq_one, Module.Free.of_divisionRing, and FiniteDimensional.nonempty_linearEquiv_of_finrank_eq (all require [AddCommGroup M]) don't fire on ρ.obj v. Fix (mirrors extDiff): letI : ∀ v, AddCommGroup (ρ.obj v) := fun _ => Etingof.Problem6_9_3.acg (k := k) as the first proof line — acg = { inst with neg := (-1)•·, … } keeps toAddCommMonoid defeq to the bundled instance, so Module k (ρ.obj v) stays compatible and TC now finds Free/finrank lemmas. Worked example: irreducible_isSimpleRep (#6166) proves an abstract irreducible ρ over a finite acyclic quiver is ≃ a vertex simple — all arrows vanish (well-founded induction on fun a b => Nonempty (a ⟶ b), whose Relation.TransGen is irreflexive by NoOrientedCycles→positive Quiver.Path i i, hence WF via Finite.wellFoundedOn+Subrelation.wf), then IsSimpleModule k (ρ.obj v₀) gives finrank=1 and nonempty_linearEquiv_of_finrank_eq builds the vertexwise iso (commutes is free since both sides' arrow maps are 0). Two tactic gotchas there: (a) a ⊥=⊤ → Subsingleton helper written as a local have ∀ {M : Type*} triggers AddConstAsyncResult.commitConst: constant has level params […] — a universe-polymorphic have breaks async elaboration; make it a top-level private theorem instead. (b) to read off Function.update f v₀ U v₀ = U from a let F := Function.update …, rw [Function.update_self] fails (can't see through the let); use simpa only [F, Function.update_self] (simp only [F] DOES unfold a let-bound local).
   • Decidable.casesOn composition (double round-trip) in reflectionFunctorPlus/Minus proofs — the composition F⁻(F⁺(V)) creates types Lean can't reduce through. Note: Individual arrow-level helper lemmas (e.g., reversedArrow_ne_ne_is_cast, reversedArrow_ne_ne_twice) ARE provable using eqRec_heq_self and Subsingleton.elim patterns (see HEq section below). The dead-end is the full Sigma-level round-trip, not individual components.
   • reflFunctorPlus_mapLinear_ne_ne / reflFunctorMinus_mapLinear_ne_ne API (missing) — RESOLVED: both now exist in Chapter6/Definition6_6_3.lean / Definition6_6_4.lean (plus _eq_ne, _equivAt_ne, _equivAt_eq); use them directly for reflection-functor naturality (ne/ne and eq/ne cases).
   • Representation W over a non-ambient Quiver instance (e.g. reversedAtVertex Q i): dot-notation resolves the WRONG quiver. W.obj/W.sinkMap/W.instAddCommMonoid/W.mapLinear synthesize the ambient [Quiver Q] for their instance arg, not reversedAtVertex Q i, giving "synthesized inst✝ / inferred reversedAtVertex Q i" or "failed to synthesize AddCommMonoid (W.obj v)". Fix: write everything with explicit @ pinning the quiver (@Etingof.QuiverRepresentation.sinkMap k _ Q (Etingof.reversedAtVertex Q i) W i), and provide the per-component DirectSum/lof/component instances via letI acmW : ∀ b, AddCommMonoid (@…obj … (reversedAtVertex Q i) W b.fst) := fun b => @…instAddCommMonoid k Q _ (reversedAtVertex Q i) W b.fst (and modW for Module). To transport such a rep back to the ambient quiver, package the vertex-space transport as a LinearEquiv via match I₂, h with | _, rfl => LinearEquiv.refl (turns the accessor HEqs into plain equations — see objTransportEquiv/transportReversedTwiceEquiv in Chapter7/Exercise7_9_8.lean).
   • Definition-level sorry : Type for AlgIrrepGL — RESOLVED (Wave 35): SchurModule constructed in PR #1740, AlgIrrepGL instances via show ... from inferInstance in PR #1752. Some downstream definition sorrys remain (formalCharacter, kostkaNumber).
   • Nilpotent operator structure theorem (cyclic decomposition / Jordan chains) — not in Mathlib, blocks Problem6_9_1. — RESOLVED (Wave 47): Problem6_9_1 proved without cyclic decomposition via direct IsCompl argument (#2215).
   • Clifford theory (semidirect product orbit method) — blocks Mackey machine (Theorem5_27_1) — RESOLVED (Wave 47): All Mackey machine sorries proved. PRs #2034, #2047, #2049 all merged after CI fix (#2240). The original 500-line estimate was too pessimistic — bypass approaches proved sufficient.
   • Submodule.map of complementary submodules through non-injective maps — does NOT preserve complementarity. Problem6_9_1 IsCompl conditions hit this fundamental gap. — RESOLVED (Wave 47): Bypassed via 7-step IsCompl proof that avoids map_of_complementary entirely (#2215).
   • Lemma5_13_3 (Young symmetrizer idempotency) over general fields — currently only works over ℂ. Blocks the trace-based approach to Weyl character formula.
   • Corner ring Morita equivalence (eAe Morita equivalent to A for full idempotent e) — not in Mathlib, ~200-300 lines. Blocks BasicAlgebraExistence.
   • basic_morita_algEquiv (basic + Morita equivalent ⟹ isomorphic) — fundamental circularity: all non-circular approaches require Krull-Schmidt theorem or progenerator theory, neither in Mathlib.
   • Right-multiplication dominance for polytabloids — RESOLVED (Wave 46): The tabloid module approach (TabloidModule.lean) bypasses the right-multiplication issue entirely. Linear independence uses tabloid projections + unitriangularity, not direct dominance comparison. The remaining bottleneck is polytabloid_syt_dominance which needs a cross-column entry comparison argument (issue #2124).
   • columnInvCount' as straightening WF order — PROVEN FALSE (counterexample in #2104): for partition (2,2), σ = swap(1,2) has columnInvCount' = 1, but Garnir terms can also have columnInvCount' = 1. The correct WF order is tabloid dominance (multiset-based), not pointwise column inversion count. PR #2119 was closed as stale; straightening needs a fresh implementation using tabloidDominance from TabloidModule.lean.
   • Non-commutative TensorProduct — Mathlib requires CommSemiring. Balanced tensor product A ⊗_{eAe} N (or M ⊗_A N, M right / N left over a noncommutative A) must be built as a manual quotient. Worked sorry-free template: Chapter8/Definition8_2_3.lean (Tor, #5628). Recipe: right A-modules are ModuleCat Aᵐᵒᵖ (right action m*a = MulOpposite.op a • m); M ⊗_A N := TensorProduct ℤ M N ⧸ S, S = AddSubgroup.closure {(op a • m) ⊗ₜ[ℤ] n - m ⊗ₜ[ℤ] (a • n)}; the induced map for f : M ⟶ M' is QuotientAddGroup.map S S' (TensorProduct.map f.hom.toAddMonoidHom.toIntLinearMap LinearMap.id).toAddMonoidHom h (containment h: AddSubgroup.closure_le + rintro ⟨a,m,n,rfl⟩ + subset_closure ⟨a, f.hom m, n, by simp [map_smul,…]⟩); then Functor.leftDerived over AddCommGrpCat gives the derived functor (#print axioms shows only propext/choice/Quot.sound, no sorryAx). Functor-law proof pattern (cost me several iterations): (a) extract the induced morphism as a named def … : tensorOver M →+ tensorOver M' plus a @[simp] _mk lemma (f ↑(m ⊗ₜ n) = ↑(f.hom m ⊗ₜ n) := rfl) — you cannot simp [theFunctor] inside the functor's own where block (self-reference error), and ext drills to different depths (bare tensor for single-morphism goals like map_id; only to the quotient for sum goals like Additive.map_add, where you then need obtain ⟨y, rfl⟩ := QuotientAddGroup.mk_surjective x); (b) induction x (TensorProduct): tmul by simp, add a b ha hb by simp only [map_add, ha, hb]; coercion-additivity ↑(p+q) = ↑p + ↑q is map_add (QuotientAddGroup.mk' _) p q. Unblocks corner ring Morita equivalence and BasicAlgebraExistence. Feeding a commutative-ring module to this right-module Etingof.Tor (statement pass for Problem 8.2.7, Chapter8/Problem8_2_7.lean): the argument is ModuleCat Aᵐᵒᵖ, but for commutative A (ℤ, k[X]) a left module has no automatic Module Aᵐᵒᵖ; supply it as a noncomputable local instance … : Module Aᵐᵒᵖ M := Module.compHom M ((RingHom.id A).fromOpposite fun x y => mul_comm x y) (do NOT make it a global instance — for M = A it diamonds with Semiring.toOppositeModule). To write a cyclic-module answer A/gcd without any GCDMonoid/DecidableEq A instance (unavailable for a general field's k[X]), use A ⧸ Ideal.span {f, g} — in a PID (f)+(g) = (gcd). Proof pass — higher Tor/Ext vanishing for cyclic R/(a) over a PID (#6263, Problem8_2_7.lean, all four _vanish; the content is projective dimension ≤ 1 via the length-1 resolution 0 → R →(·a) R → R/(a) → 0). Ext: build the resolution in ModuleCat R (ModuleCat.shortComplexOfCompEqZero f g eq0 + ModuleCat.shortComplex_shortExact from Function.Exact f g/inj/surj proved on the bare LinearMaps — f := (a:R) • LinearMap.id, g := Algebra.linearMap/(Ideal.span {p}).mkQ), then ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃ 1 (both free terms projective; import Mathlib.CategoryTheory.Abelian.Projective.Dimension) gives HasProjectiveDimensionLT (R/(a)) 2, and HasProjectiveDimensionLT.subsingleton _ 2 (n+2) (by omega) _ kills Extⁱ for i≥2. Tor (right module lives in ModuleCat Rᵐᵒᵖ): build the same resolution over Rᵐᵒᵖ — the ·a map's map_smul' closes by simp only [RingHom.id_apply, MulOpposite.smul_eq_mul_unop]; ring (the Semiring.toOppositeModule action is r•x = x*r.unop), and the quotient map's map_smul' by rw [MulOpposite.smul_eq_mul_unop]; change …; rw [← map_smul]; …mul_comm (the Module.compHom action r•z is defeq r.unop•z, so change/rfl bridge the two) — then squeeze the middle Tor between the two vanishing free-term Tor (Functor.isZero_leftDerived_obj_projective_succ) inside Etingof.Functor.leftDerived_sixTerm_exact F hS (n+1) (n+2) rfl, extracting the ShortComplex.Exact at the middle with hExact.exact' 1 2 3 then Exact.isZero_X₂ (h1.eq_of_src _ _) (h3.eq_of_tgt _ _). a=0/f=0 edge: R/(0) ≅ R is free; do NOT rely on Projective (ModuleCat.of Rᵐᵒᵖ (R/(0))) instance search (it heartbeat-loops on ZMod 0) — transport IsZero along an explicit Rᵐᵒᵖ-linear equiv to the free module ({ e0.toAddEquiv with map_smul' := fun r z => by change …; rw [smul_eq_mul, mul_comm] }, e0 := Submodule.quotEquivOfEqBot; keep x : R on the domain side of the equiv so HMul doesn't get stuck on the ZMod 0/quotient carrier). The degree-0/1 Tor/Ext ≅ R/gcd identifications are still sorry (out of scope of #6263). When the module structure is the external tensor product over a noncommutative A₁ ⊗[k] A₂ (Künneth, Problem 8.2.8, Chapter8/Problem8_2_8.lean) the compHom shortcut no longer applies and TensorProduct.Algebra.module only builds Module (A⊗B) M from commuting actions on a single M — the external structure (A₁ on the first factor, A₂ on the second; plus Algebra.TensorProduct.opAlgEquiv : (A₁⊗A₂)ᵐᵒᵖ ≃ₐ A₁ᵐᵒᵖ⊗A₂ᵐᵒᵖ on the right-module Tor side) is not a defeq-safe instance. For a statement pass, don't construct it: take Module (A₁⊗[k]A₂) … / Module (A₁⊗[k]A₂)ᵐᵒᵖ … as instance-implicit theorem parameters pinned by a hypothesis fixing the action on simple tensors ((a₁⊗ₜa₂) • (x₁⊗ₜx₂) = (a₁•x₁)⊗ₜ(a₂•x₂); wrap the right side in MulOpposite.op for the ᵐᵒᵖ case). Simple tensors generate and • is additive, so the pin determines the structure uniquely — faithful, and sidesteps statement-irrelevant instance plumbing. RHS ⨁_{j+m=i} is DirectSum over {p : ℕ × ℕ // p.1 + p.2 = i} with TensorProduct ℤ summands (group-level shadow of the book's ⊗ₖ, matching Problem 8.2.7). HasExt (ModuleCat.{v} R): resolves from Small.{v} R (free when R : Type v), but synthesis heartbeat-times-out unless you import Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences alongside …ModuleCat.Ext.HasExt.
   • Tensor of an acyclic complex is acyclic, over a field (Problem 7.8.7(ii), #6304, Chapter7/Problem7_8_7.lean). Route: (a) helper acyclic_of_homotopy_id_zero : Homotopy (𝟙 X) 0 → X.Acyclic — Homotopy.homologyMap_eq gives 𝟙 (Hⁱ X) = homologyMap (𝟙 X) i = homologyMap 0 i = 0, then exactAt_iff_isZero_homology + IsZero.iff_id_eq_zero. (b) Etingof.Exercise7_8_4 K hK : Nonempty (Homotopy (𝟙 K) 0) (over a field an acyclic complex is contractible). (c) Whisker that homotopy through the tensor bifunctor with HomologicalComplex.mapBifunctorMapHomotopy₁ (homotopy in the first arg — use for the C-acyclic case) / mapBifunctorMapHomotopy₂ (second arg — D-acyclic case), from Mathlib/Algebra/Homology/BifunctorHomotopy.lean. tensorObj/tensorHom on HomologicalComplex are defeq to mapBifunctor/mapBifunctorMap for F := curriedTensor (ModuleCat k), c := ComplexShape.up ℤ. Bridge the homotopy's endpoints to 𝟙/0 with Homotopy.ofEq: mapBifunctorMap (𝟙)(𝟙) = 𝟙 by rw [mapBifunctorMap, CategoryTheory.Functor.map_id, NatTrans.id_app, CategoryTheory.Functor.map_id, Category.id_comp, HomologicalComplex₂.total.map_id]; rfl, and mapBifunctorMap 0 g = 0 (and f 0 = 0) by apply HomologicalComplex.hom_ext; intro j; apply HomologicalComplex.mapBifunctor.hom_ext; intro i₁ i₂ hji; simp (the ι_mapBifunctorMap simp lemma + the bifunctor killing 0). Two gotchas: (i) Functor.map_id/Functor.map_zero resolve to the applicative _root_.Functor (id <$> x) and silently mismatch — always qualify CategoryTheory.Functor.map_id. (ii) Acyclic is a Prop but Homotopy is data (Type): rcases/split the C.Acyclic ∨ D.Acyclic disjunction first (while the goal is still the Prop Acyclic), then build the homotopy inside each branch — you cannot eliminate an Or into a Homotopy.
   • garnir_reduction' algebraic approach — The standard approach using a_λ · G = 0 (Garnir element annihilated by row symmetrizer) and Lemma 5.13.1 collapses to a tautology when trying to extract the linear combination. The algebraic identity only shows the existing tabloid is in the span — it doesn't produce the smaller tabloids needed for the inductive step. Needs tabloid-level reasoning (James' approach: work with equivalence classes of fillings under row permutations) instead.
   • Polytabloid transfer map tabloidProjection(polytabloid T) = polytabloidTab T — PROVEN FALSE (Wave 46-49): For partition (3,2), two distinct SYTs can map to the same inverse-tabloid. The dominance property (swap_column_dominance) fails for σ_T⁻¹. 4+ agent sessions were wasted on this approach across issues #2189, #2212. The correct approach uses tabloid-level unitriangularity (Track 2 in TabloidModule.lean), not direct transfer.
   • iso_of_formalCharacter_eq_schurPoly — Requires GL_N complete reducibility (Schur-Weyl duality), which is NOT in Mathlib. — RESOLVED: now sorry-free at SchurWeylFormalCharacterIso.lean:992, built on decompose_polynomial_gl_rep (GL_N-equivariant complete reducibility, PolynomialGLDecomposition) + schurPoly_linearIndependent + the highest-weight identification. The ~300-line infrastructure was built. Use it as the GL char→iso keystone: it takes halg : IsAlgebraicRepresentation, h_span (ℕ-weight spaces span ⊤), and h : formalCharacter = schurPoly N lam, and returns Nonempty (M ≅ SchurModule k N lam). Do NOT treat highest-weight / character→iso work (e.g. the §5.23 contragredient identity) as blocked on this.

   Before recording a "missing from Mathlib" / "needs a helper Mathlib lacks" claim in a docstring or issue, grep the relevant Mathlib file — pessimistic absent-API notes propagate and block successors who trust them. (#5320: a prior clength_additive docstring said the second-isomorphism diagram chase "needs a pseudoelement-membership helper Mathlib does not yet have"; in fact Abelian.Pseudoelement.sub_of_eq_image/pseudo_pullback and the categorical snake lemma Mathlib.Algebra.Homology.ShortComplex.SnakeLemma are all present and make the route reachable.) When the section introduction blob states a standing assumption (e.g. §9.6 "every object has finite length"), check whether the formalized class actually carries it — dropped standing assumptions are a fidelity gap that makes per-section theorems unprovable as stated (#5320: IsFiniteAbelianCategory omits finite length; the §9.6 carrier is IsFiniteAbelianCategoryOverField.finiteLength). The flip side — discharging an over-hypothesis: when a Ch9 theorem carries a [IsNoetherianRing …] / [FiniteDimensional …] / [Module.Finite …] side condition on an End/Hom object that the book never states, it is almost always auto-satisfied via the over-field carrier — Etingof.IsFiniteAbelianCategoryOverField.finiteDimensional_hom : FiniteDimensional k (X ⟶ Y) (Introduction_9_6.lean) proves every Hom-space is finite-dim over k. From there (End P)ᵐᵒᵖ Noetherian is a 3-liner (finiteDimensional_hom P P → Module.Finite k (End P)ᵐᵒᵖ via the Mathlib opposite instance → isNoetherian_of_tower k inferInstance; the algebra/opposite Module k diamond is defeq, so inferInstance chains cleanly). #5665 removed exactly such a [IsNoetherianRing (End P)ᵐᵒᵖ] from Theorem_9_6_4 this way. Do NOT reach for the abstract subobject↔submodule (Galois) correspondence to derive these — it needs arbitrary sups the finite-length subobject lattice doesn't carry in Mathlib; the over-field finiteDimensional_hom route is the intended lever. Pattern for keeping ring-level consumers (§9.7 Introduction_9_7_Morita.lean is deliberately k-free) working: keep the Noetherian-hypothesis proof as a general _of_isNoetherian engine and make the book-faithful theorem a thin over-field wrapper that derives the instance and delegates.

   Forming Fin n- (or ι-)indexed biproducts in an abstract abelian category [Category.{v} C] — two instance traps (#6206, Exercise9_6_3.lean, progenerator characterization). (a) Abelian.hasFiniteBiproducts is only an attribute [local instance] in Mathlib, so HasFiniteBiproducts C is not found by global TC search — HasBiproduct (fun _ : Fin n => P) fails to synthesize until you add haveI : HasFiniteBiproducts C := Abelian.hasFiniteBiproducts (then the global hasBiproductsOfShape_finite instance fires for any [Finite J]). (b) Mathlib's Projective (⨁ g) instance is declared {β : Type v} sharing the morphism universe v, so it does not apply to g : Fin n → C (Fin n : Type 0) when v is an arbitrary universe variable. Restate it universe-polymorphically: theorem projective_biproduct {β : Type*} (g : β → C) [HasZeroMorphisms C] [HasBiproduct g] [∀ b, Projective (g b)] : Projective (biproduct g) where factors f e _ := ⟨biproduct.desc fun b => Projective.factorThru (biproduct.ι g b ≫ f) e, by refine biproduct.hom_ext' _ _ (fun b => ?_); simp [Projective.factorThru_comp]⟩, and also supply [∀ b, Projective (g b)] explicitly (haveI : ∀ b, Projective (g b) := fun _ => inferInstance — the Pi-instance is not auto-derived from [Projective P]). Note Etingof.wellFoundedLT_subobject (Length.lean) gives IsArtinianObject X via isArtinianObject.is_of_prop, unlocking Mathlib's exists_simple_subobject for simple-quotient/subobject peeling inductions on Etingof.clength (clength_additive/clength_strictMono are the length arithmetic).

2. Search for existing definitions and infrastructure. Before defining any concept or building any equivalence/isomorphism, search the codebase:

   grep -r "def.*YourConceptName\|abbrev.*YourConceptName" EtingofRepresentationTheory/
   

   Duplicate definitions across chapters create incompatibility bugs that require manual refactoring later (e.g., duplicate inducedCharacter' in Ch5, duplicate IsIndecomposable in Ch2/Ch6). Also search for infrastructure you might need — PRs #1682, #1685, #1690 independently built the same GL₂(𝔽_q) BorelSubgroup equivalence because agents didn't check what already existed. Before building group/subgroup equivalences, coset decompositions, or character computation helpers, search for them first.

   The same trap applies to whole theorems, not just helpers: a headline result is often already proven sorry-free under a different book-item name than the issue you claimed. Book theorems and later problem-set problems frequently establish the same mathematical fact (a theorem states it; an exercise re-derives it via a guided route). Before starting — or accepting a multi-session decomposition of — a proof of a headline result, grep for an existing proof of the same statement under any name and just read your conclusion off it (per CLAUDE.md "use earlier results in the project"). #5311 (Problem 2.15.1(h)–(k), sl₂ complete reducibility) was decomposed into a multi-session build (#5316/#5317/#5318), but ComplementedLattice (LieSubmodule ℂ sl2 V) was already proven sorry-free as Theorem_2_1_1_ii (Theorem 2.1.1(ii)) via the same Casimir argument; the final complete_reducibility sorry was a one-line exists_isCompl away. Grep by the mathematical content (ComplementedLattice, IsCompl, the target conclusion), not just the item id.

   When verifying Mathlib lemma names/signatures, grep this project's own .lake/packages/mathlib, never another Mathlib checkout elsewhere on the machine. This repo pins a recent Mathlib; other local clones (e.g. lean-training-data) can be months behind, with renamed or absent API. Confirming against the wrong checkout sends you down dead ends — e.g. hand-rolling a matrix-charpoly-eigenvector argument because the project's cleaner Module.End.trace_eq_sum_roots_charpoly_of_splits / hasEigenvalue_iff_isRoot_charpoly (and the single-argument Polynomial.Splits) weren't visible in the stale checkout (#5129). The same drift hits import module paths, not just lemma names — modules get split and relocated between versions. Before writing a new import Mathlib.…, confirm the file exists: find .lake/packages/mathlib/Mathlib -name 'GeomSum.lean' (or grep for the lemma and read its file's module path). Guessing from memory wastes a build cycle on bad import — e.g. (#5287) Mathlib.Algebra.GeomSum → Mathlib.Algebra.Ring.GeomSum, Mathlib.Algebra.Polynomial.Eval → Mathlib.Algebra.Polynomial.Eval.Defs. For a new file, just import Mathlib (every project file does). The pinned Mathlib uses the module/public import system, so granular import Mathlib.Foo.Bar lines silently fail to expose public declarations — symptom is a baffling Unknown identifier 'Basis' at the variable line even though the import "succeeded". Also note Basis is now Module.Basis: a fresh file needs open Module for bare Basis/End/finrank/finBasis to resolve (#5638). These two cost ~4 build cycles when writing Chapter5/DiagonalCoordinate.lean from scratch. The same granular-import gap can hit individual Basis.* lemmas even when the Basis type itself resolves: in a pre-existing granular-import file, apply Basis.ext … / rw [Basis.constr_basis] reported Unknown identifier while Pi.basisFun worked fine. Fix: use dot notation — b.ext fun i => …, b.constr_basis … — which resolves through the term's type even when the fully-qualified name doesn't (#5301). (Adding a granular import Mathlib.LinearAlgebra.Basis.Basic did not help.) In a pre-existing granular-import file (no open Module) the basis constructor and finrank-from-basis lemma need the Module. prefix: Module.Basis.mk hli hsp (bare Basis.mk is Unknown identifier) and Module.finrank_eq_card_basis (bare finrank_eq_card_basis is unknown), provided by import Mathlib.LinearAlgebra.Dimension.Finrank + …Dimension.Finite. Eigenvalue theory over IsAlgClosed (Module.End.exists_eigenvalue, HasEigenvalue.exists_hasEigenvector, Module.End.mem_eigenspace_iff) needs import Mathlib.LinearAlgebra.Eigenspace.Triangularizable; IsAlgClosed needs import Mathlib.FieldTheory.IsAlgClosed.Basic (#6189). A clean "central element acts as a scalar on a simple f.d. module over IsAlgClosed k" (Schur) is: take an eigenvalue of Algebra.lsmul k k V z, its eigenspace is a nonzero WeylAlgebra-invariant k-submodule (z central), hence ⊤ by IsSimpleModule — no need for the Module.End-is-a-division-ring machinery. Reusing a lemma from a section under a different typeclass regime — a section variable [CharZero k] gets stamped onto every declaration in that section, even ones that never use it (the unusedSectionVars linter confirms this by warning), so calling such a lemma under [CharP k p] fails with failed to synthesize CharZero k. Symptom while proving center_charP (#6188): the char-free adx/ady monomial lemmas lived inside section CharZeroSimple and would not apply in characteristic p. Fix: hoist genuinely hypothesis-free infrastructure into its own section with only the minimal variable (k) [Field k], above the char-specific sections, so both a [CharZero k] and a [CharP k p] consumer can use it. Cheaper than re-proving the lemmas per characteristic.

3. Verify the statement. Cross-reference the Lean statement against the book's text. Missing hypotheses (algebraic closure, field characteristic, orientation constraints) are a recurring source of wasted proof attempts. If the proof fails at a fundamental level after 1 attempt, suspect a statement bug before trying alternative tactics.

4. Estimate your context budget. Difficulty 3/3 proofs consume 60-80% of a context window on average. If you're already past the midpoint of your session, consider claiming an easier item instead. Partial progress on a hard proof with no commit is worth zero — a completed easy proof is worth one sorry removed.

5. Check dependency readiness. Verify that imports compile and key helper lemmas are sorry-free (or that sorry'd helpers won't block your proof). Use lake build <module> for the specific file. A "closed/merged" dependency can still fail to compile. A .lean file absent from its ChapterN.lean aggregator is never built by CI, so it rots silently when an upstream lemma it cites changes signature. Before consuming a cited dependency, grep "ChapterN.Module" EtingofRepresentationTheory/ChapterN.lean to confirm it is in the build graph, then lake build that exact module — do not trust that #closed ⟹ compiles. And when you create a new file, add it to the ChapterN.lean aggregator in the same PR (otherwise it will not be CI-checked and the next signature change will break it undetected). Concretely (#4695): KernelLemmaK.lean (the #4694 kernel-lemma assembly) was never in the aggregator and had stopped compiling against the corrected kernelLemmaK'; the fix had to be made before the assembly could even be attempted. Note also: when wiring a low-level file (e.g. a localization stack) back into a higher-level one, watch for import cycles — if file A imports B only for one small lemma, relocate that lemma to a leaf (Mathlib-only) file imported by both, rather than creating the cycle. A specific recurring trap for "discharge the sorry at File.lean:L" issues: the machinery you need may sit downstream of the statement file and transitively import it. This pipeline creates statement files early and proves the machinery in later files, so the engine often imports the very file holding the sorry. Before assuming you can import the machinery into the statement file, compute the closure (small Python DFS over import EtingofRepresentationTheory.… lines) and check whether the statement file is in it. When it is, the importing edges are frequently doc-comment-only (grep -nE "<defined-ident>" Importer.lean shows hits only in /-! … -/): delete those stale imports to break the cycle (verify the importers still build). Diagnosed in #5478/#5488: PolynomialGLDecomposition reached Theorem5_23_2 only via CauchyDetQuotient and SchurModuleSpecialBlock, both comment-only.

   Use set -o pipefail when piping lake build through tee/tail — otherwise the pipeline's exit code is tee's 0 and a real build failure reads as success. For "mechanical glue"/aggregation issues, also audit that the generality of every input lemma matches the goal — closed/merged ≠ usable. An issue can have all its named dependencies merged yet still be unwritable because the inputs are proved at a narrower generality than the target. Concretely (#2708, Schur-Weyl C-4a): the goal schurModuleSubmodule_isSimple_centralizer is over a generic alg-closed CharZero field k, but every per-block input it must feed (trace_symGroupAction_eq_spechtModuleCharacter:1029, youngSym_action_vanishes_off_block:2158, youngSym_action_on_special_block_rank_one_scaled_proj:2279) is hardcoded to ℂ, and generic k does not base-change from ℂ. grep the input lemmas' signatures for the field type before claiming. If they are ℂ-only while the goal is generic, the issue is mis-scoped: coordination skip to replan with the two paths (specialize the goal to ℂ — usually correct when the rest of that chapter's backbone is ℂ-only and nothing consumes the generic statement; or first generalize the inputs to generic k). Do not rewrite the goal's generality unilaterally.

6. Code the framework before deep analysis. When a proof has an obvious high-level structure (e.g., "use Schur's lemma + nonvanishing"), code that framework with sorry placeholders within the first 15 minutes. Don't spend the majority of your session analyzing whether the hard step is provable before writing any Lean. The framework commit has value even if the hard sorry remains — it reduces the problem for future agents. Deep mathematical analysis should happen AFTER the framework compiles, focused on the specific sorry goals.

Endgame Protocol (≥99% Sorry-Free)

When the project is near completion (581/583 items sorry-free as of Wave 49), the remaining sorries are qualitatively different — they're the hardest problems, not low-hanging fruit. Agents must adjust their approach.

Definition Audit Before Proof Attempts

When a proof is stuck after 2 attempts, audit the definition against the textbook BEFORE trying more proof approaches.

The polytabloid definition was non-standard (T-dependent form κ_T · of(τ) · a_λ instead of standard of(τ) · c_λ). This caused 4+ agent sessions of wasted work across multiple waves. Once the definition was refactored to match the textbook, 3 sorries were eliminated trivially.

Checklist when stuck:

1. Read the blob file for the relevant definition
2. Compare the Lean definition's structure against the book's mathematical definition
3. Check: does the Lean definition use the same decomposition/factoring as the book?
4. If not, consider whether a definition refactoring would simplify the proof
5. A definition refactoring that makes proofs trivial is MORE valuable than a clever proof of a bad definition

Counterexample-First Verification

Before investing a full session in a hard proof, spend 5-10 minutes checking the statement is correct:

1. Instantiate with concrete examples. If the theorem is about all graphs with property P, check P for the simplest non-trivial case.

2. Check boundary cases. The hypothesis h_dim : Module.finrank k M = Module.finrank k (SchurModule k N lam) was added to iso_of_formalCharacter_eq_schurPoly after discovering a counterexample: M = SchurModule ⊕ det⁻¹. formalCharacter is a truncated invariant — it records only ℕ-valued weight spaces and is blind to det-twists — so it is NOT a complete invariant, and SIMPLICITY does not rescue it. Any lemma deriving "M is polynomial" (⨆ μ, glWeightSpace = ⊤) or "M ≅ L_λ" from IsSimpleModule + formalCharacter M = schurPoly N lam alone is false (#4948): counterexample M = det⁻¹ ⊗ Sym³(std), N=2 — simple, 4-dim, formalCharacter = x₁+x₂ = schurPoly 2 (1,0) (the (-1,-1) shift sends (3,0),(2,1),(1,2),(0,3) ↦ (2,-1),(1,0),(0,1),(-1,2), only (1,0),(0,1) ∈ ℕ² survive) yet ℕ-weight spaces span only 2 of 4 dims and M ≇ std. Polynomiality must be a threaded hypothesis (hLtop : ⨆ μ, glWeightSpace = ⊤), discharged from the rep's actual polynomial source (e.g. transport M's h_span to a simple summand L across the equivariant iso via glWeightSpace_map_eq_of_rep_iso + Submodule.map_iSup), never manufactured from simplicity. When a planner decomposes a hard theorem into "isolated sorry ingredients", an ingredient can itself be unsound — verify each ingredient is TRUE (seek a counterexample) before grinding on its proof. Tactic gotcha (weight-space dim work): rw of a submodule-valued subterm sitting under Module.finrank (e.g. rw [glWeightSpace_eq_glWeightSpaceℤ …] or glWeightSpaceℤ_charTwist_shift inside finrank k (glWeightSpace …)) fails with motive is not type correct — the [Module k ↥S] instance can't be abstracted over the rewritten S. Fix: prove the submodule equality S = T first (rewrites there are fine), then bridge to the ℕ-level finrank equation with a congrArg helper congrArg (fun U : Submodule k V => Module.finrank k U) (h : S = T) : finrank k S = finrank k T (and rw that). The p-fold det-twist character formula formalCharacter_charTwist_detChar_pow (AlgIrrepGLNonIso.lean, induction via formalCharacter_shift_of_weightSpace_finrank) is a worked example.

3. If two "different" accounts/objects produce suspiciously similar data, investigate.

4. Indecomposability of explicit affine-Dynkin reps: build a small decomposition first. The Ch6 *Rep_kQ_isIndecomposable family (D̃/Ẽ/T(p,q,r), orientation-generic) is built from a single nilpotent twist N, which is too weakly coupled and yields decomposable reps. Already refuted for the sporadic cases (Ẽ₆/Ẽ₇/T(1,2,5), #4548, progress/indecomposability-framework-investigation.md) and for the D̃ family in reversed-leaf orientations (D̃₄ #4523 → #4566: explicit m=1 complementary pair). The needed fix is the homogeneous-tube redesign, not a cleverer proof. Before claiming any open d5/d6/d7/d8/dTilde/etilde/t125 *_kQ_isIndecomposable issue, check #4566/#4548 — most are likely still false. A reversed leaf removes the coupling its forward edge supplied, so test a reversed orientation at m=1 for span-level decompositions. (Note: the canonical all-sink D̃₄ starRepGen_isIndecomposable is genuinely indecomposable — only the orientation-generic statements are at risk.) This also refutes the *_kQ_leaf_equalities sub-lemmas (e.g. #2853, and the d6/d7/d8 analogs) that feed those _isIndecomposable theorems: the mixed orientations (one leaf pushed, one pulled at a shared center) force only an M-twisted relation M(W⟨leaf⟩) = W⟨other⟩ with M = (I−N)⁻¹ (derivable via linearEquiv_invariant_isCompl_symm_mem + gammaInv_embed_general_F + the v=2 core_F), and no edge supplies the leaf N-invariance needed to untwist it — so leaf equality is false there (D̃₅ m=1: W⟨0⟩=span{(1,1)}, forced W⟨5⟩=(I−N)W⟨0⟩=span{(0,1)}). Don't grind on a _leaf_equalities issue over arbitrary orientations; only the all-canonical and all-leaves-reversed branches are provable. To land a sorry-free _leaf_equalities, restrict the statement rather than leaving bare sorries (#4743 for D̃₅): add explicit Hom-direction hypotheses to the signature (hc02/hc12/hc23 : Nonempty (@Quiver.Hom (Fin n) Q ⟨a⟩ ⟨b⟩) pinning each canonical edge, plus a same-direction Iff for the two shared-center leaves, e.g. hv3 : Nonempty (Hom 4 3) ↔ Nonempty (Hom 5 3)), then discharge every off-restriction rcases hOrient_edge branch with (hOrient.2.2 i j h_canonical h_reversed).elim — IsOrientationOf's third conjunct (OrientationDefs.lean:41) is exactly the antisymmetry "no arrows both ways". This keeps the existing case tree intact; only the previously-sorry leaves change to one-line contradictions (minimal diff). If the lemma is consumed generically (e.g. by _isIndecomposable, which only uses it in its all-canonical branch), move the call into the branch that can supply the hypotheses — there the canonical arrows give ⟨a02⟩ ⟨a12⟩ ⟨a23⟩ and same-direction v3 leaves give iff_of_true ⟨a43⟩ ⟨a53⟩. Reusable across the open D̃₆/₇ leaf_equalities (#4722/#4689). Construction tip for the homogeneous-tube def (sub-A of each shape, e.g. t125Rep_kQ #4559 mirroring etilde7Rep_kQ #4568): the *RepMap_kQ match must produce (Fin (*Dim m a) → F) →ₗ (Fin (*Dim m b) → F), and the leaf vertex has dimension m+1 (not 1*(m+1)) in *Dim. Since 1*(m+1) is not defeq to m+1, the a=1 block maps (suffixBlockEmbed_F F 1 2, prefixBlockEmbed_F F 1 _) fail to typecheck at the leaf — use starEmbed2_F/starSecond_F (suffix) or starEmbed1_F/starFirst_F (prefix), which produce the bare Fin (m+1) shape. The 2…6-coefficient block maps are fine. To extract >2 input blocks for a wide eigenvalue arm (T(1,2,5)'s arm 1 is F^{3(m+1)}), the fixed-N blockEmbedAt_F won't fit; use the general blockEmbedAtN_F/blockProjAtN_F (FieldGenericT125.lean, target dim a raw ℕ). 3-arm tube caveat (Ẽ₆/T(p,q,r), #4638): even the all-canonical "three leaf subspaces equal W⟨leaf_i⟩ all equal" collapse is circular and NOT a usable stepping stone — unlike D̃₄ where each arm's diagonal embed hits both center blocks (so compl_le_forces_eq gives W⟨leaf⟩=W⟨1⟩=W⟨2⟩ for any pair), each tube arm embeds its leaf line into only 2 of the ≥3 center blocks. The proven membership criteria (etilde6_arm{A,B,C}_criterion, FieldGenericETilde6.lean) give x∈W₁⟨2⟩ ↔ (0,x,x)∈W₁⟨0⟩, x∈W₁⟨4⟩ ↔ (x,0,x)∈W₁⟨0⟩; the inclusion W₁⟨2⟩≤W₁⟨4⟩ that compl_le_forces_eq needs is (0,x,x)∈W₁⟨0⟩ ⟹ (x,0,x)∈W₁⟨0⟩, false for general W₁⟨0⟩ (e.g. ⟨(0,1,1)⟩). Leaf-equality holds only because the surviving pairs are trivial — i.e. it is a corollary of indecomposability, not a route to it. The correct route (sub-C assembly) is the §3 brick contradiction consuming the criteria + etilde6_arm*_plane_split (each plane π_i=(W₁⟨0⟩⊓π_i)⊕(W₂⟨0⟩⊓π_i)) + the eigenvalue site, concluding W₁⟨0⟩∈{⊥,⊤} directly. Once a shape's corrected homogeneous-tube def lands, its _isIndecomposable flips from false to TRUE — stop trying to refute it. Scope construction and proof as separate deliverables (the ETilde6/7 + D̃₄ pattern): the *Rep_kQ def gains an explicit (lam : F) parameter with the fourth/eigenvalue arm = starEmbedTube_F F lam m (λ•id + J, a square Jordan block — relocated into FieldGenericStar.lean, #4648), the *_not_finite_type_per_kQ consumer fixes lam = 1, and the orientation-generic _isIndecomposable proof is sorried "for every lam", deferred to a shared family-wide center-crux wall (open across D̃₄ #4674 / D̃₅–D̃₈ / Ẽ₆ etilde6Rep_kQ_isIndecomposable / Ẽ₇). The worked canonical-orientation proof starTubeRepGen_isIndecomposable (FieldGenericTube.lean) + the leaf reductions forward_leaf_subspace_eq/reversed_leaf_subspace_eq + the center lemma eigenvalue_jordan_invariant_compl_trivial_gen are the assembly pieces. So: don't re-investigate whether these are tractable as one unit, and don't refute a shape whose corrected tube already landed — check the construction's arm map first.

5. "Follows via Schur's lemma / character matching" can be circular — check the nonzero-hom prerequisite. When an issue claims a decomposition/iso "follows by Schur's lemma" from two reps being simple, remember Schur's lemma (finrank_hom_simple_simple) only gives Hom ∈ {0,1}-dim; concluding iso needs a nonzero equivariant map, which usually presupposes the very character/highest-weight match being sought. Example (#2493): identifying the abstract Schur-Weyl summand Lᵢ with SchurModule k N λ was claimed to follow from Lᵢ simple (C-3) + SchurModule simple (C-4) + Schur's lemma, but that route is circular — it needs char(Lᵢ) = schurPoly N λ (the highest-weight classification, downstream #2482/#2483) to produce the nonzero map. The character-level assembly (formalCharacter(V^⊗n) = ∑_λ dim(Sλ)·sλ) is reachable from C-1∘C-2; the concrete-module iso is not. Land the reachable character identity and route the classification gap to the downstream issue rather than forcing a circular "Schur's lemma" proof. Also: do not "rescue" such an iso with a pure finrank-equality ≃ₗ[k] — it type-checks but is mathematically vacuous (any equal-dimension spaces are k-linearly isomorphic), violating the no-vacuous-theorems principle.

6. "Vanishes pointwise" lemmas about an element already known to lie in a span are usually false — refute by direct computation. A lemma claiming an explicit element has zero coefficient at certain basis points (e.g. a residual Δ's coefficient at tabloids with no column-standard rep, Ch5 Wall 3 R2.b.i #2769) is suspicious whenever the true reason Δ sits in the target span V is global rather than pointwise. If Δ equals a single polytabloid ±ψ_τ (τ col-standard), it carries ±1 at every column-class of τ — including non-standardizable ones — so pointwise vanishing fails even though Δ ∈ V holds. Brute-force the smallest example by replicating the Lean definitional conventions exactly (toTabloid = entry→row map, ColumnSubgroup, tabloidStrictDominates, signed-polytabloid form of the construction), and validate your model reproduces a known ground truth (e.g. the design note's hand-computed values) before trusting a refutation. This refuted #2769 in minutes (progress/r2bi-counterexample-check.py, redesign tracked in #4584). A hand-checked confirmation is no safer than a hand-checked refutation — brute-force both directions. A prior meditate note (#2776, progress/r3-bis-residual-cancellation.md §3) claimed the same statement was TRUE via a cross-region involution, "validated on the running example; sign reversal verified" — the faithful brute force refuted it on that very example. When you assert a tricky combinatorial identity holds, run the script; never ship "verified by hand". And refuting the lemma does not refute the goal: the global span-membership a dead pointwise route was serving is often still true by a direct identification (here Δ = ±ψ_τ, discharged by the existing (srRank, rowInvCount') induction — see progress/r2b-redesign-direct-polytabloid.md). Also beware the inverse circularity trap: a "straightening" lemma that consumes v ∈ V as a hypothesis (e.g. tabloidSupport_straightening) cannot be the route that establishes v ∈ V; and a design note claiming a proof is "just re-packaging the internals of lemma X" is circular whenever X takes the goal as a hypothesis — check before adopting the plan. When your validation script tests a measure/ordering condition (e.g. srRank τ' < srRank σ, IH-availability, dominance), pin the measure's DIRECTION to the codebase definition before trusting PASS/FAIL. A flipped sign silently inverts the verdict: here srRank σ = #{τ : σ strictly dominates τ} counts tabloids below σ, so a tabloid dominated by σ has smaller srRank (IH-available) — an early script that counted tabloids above spuriously reported every constituent "above σ" and nearly condemned a sound route (Ch5 R2.b #4593, validated route → #4604/#4605). Re-derive one row by hand against the Lean def before reading the table.

7. Character / multiplicity identities: dimension-count both sides (evaluate at all-ones) before attempting. Any claimed formalCharacter M = ∑_λ (coeff_λ)·S_λ must match in total dimension: setting every torus variable to 1 makes each S_λ evaluate to dim V_λ = s_λ(1,…,1) and the LHS to dim M. This is a 30-second check that catches multiplicity errors instantly. It refuted #4944: polyRightDegreeFDRep_formalCharacter claimed the degree-d part A_d of k[Xᵢⱼ] had a multiplicity-one decomposition formalCharacter k N A_d = ∑_{ν : BoundedPartition N d} schurPoly N ν.parts, but for N=2, d=1, dim A_1 = 4 (the four Xᵢⱼ) while ∑_ν dim V_ν = dim V_{(1,0)} = 2 — unequal, so false. The actual right-GL_N multiplicity is dim S_ν(k^N) = s_ν(1,…,1) (the left Schur-factor of the GL×GL Cauchy bi-rep Sym^d(V⊗W) = ⊕_ν S_ν(V)⊗S_ν(W)), not one. The fix is to correct the statement to the multiplicity-bearing form ∑_ν (eval 1 (schurPoly N ν.parts)) • schurPoly N ν.parts (Cauchy at x=1^N) — and since a sorried false theorem is a landmine even unused, correct it openly (per "Definition seems wrong: don't silently work around bad definitions") rather than leaving it. Watch for "multiplicity one" / "each ν exactly once" claims about a forgetful restriction of a bi-representation: forgetting one factor of V_λ ⊠ V_λ leaves dim V_λ copies, never one (except dim V_λ = 1, i.e. powers of det). The qualitative support conclusion a consumer wants (e.g. "constituents of A/det have ν_N = 0") usually survives the multiplicity correction (the dim V_{ν-(1,…,1)} = dim V_ν factors cancel termwise), so re-spec the proof, don't abandon the consumer.

8. A character table is NOT formalized by asserting orthonormality of hand-typed rows — that is vacuous. Encoding the table as an explicit chi : Fin r → Fin r → ℂ (or Q5) and proving the rows are orthonormal + "the group has r conjugacy classes" does not pin down the table: a continuum of orthonormal r-frames satisfy it, and nothing connects the rows to actual representations — the claim "these are the irreducible characters" then lives only in the docstring. This sank Example 4.8.1's first fix (#5418 reopened → decomposed into #5428–#5431). The non-vacuous bar: build each row as the trace of an honest representation — construct V : FDRep ℂ G (from a real Representation/MonoidHom), prove V.character g equals the tabulated value at each class representative, prove V is Simple via FDRep.simple_iff_char_is_norm_one (FinGroupCharZero.lean: Simple V ↔ ∑ g, χ(g)·χ(g⁻¹) = Nat.card G, over an alg-closed char-0 field — so work over ℂ, which also carries √5 etc.), prove the rows are pairwise non-isomorphic (distinct characters / FDRep.char_orthonormal), and conclude completeness from "r distinct simples + r conjugacy classes". The same critique applies to any "tensor multiplicity" or "decomposition" table built on the orthonormality-only certificate (e.g. Example 4.9.1 uses the identical Q5 + *_orthonormal pattern and is a likely repeat flag). Also: the native_decide used to discharge those orthonormality sums and the Fintype.card (ConjClasses G) = r counts is a forbidden trust hole — evaluate character inner-product sums over G via a class-function decomposition ∑ g = ∑ class c, |c|·f(rep c), not native_decide.

9. A book formula ported verbatim into ℕ is silently FALSE at a boundary when it contains subtraction — plug in the degenerate case before proving. Truncated ℕ-subtraction makes a - b collapse to 0 (or the formula to a wrong constant) exactly where the mathematics wants a negative/zero index. Problem 2.8.11(a) #6267: the stated coefficient C(n + m - 1, m - 1) (dimension of the degree-n piece of k[x₁..x_m]) is correct for m ≥ 1 but at m = 0 becomes C(n - 1, 0) = 1 for every n, whereas k[] ≅ k is concentrated in degree 0 (dim 1 at n=0, else 0) — so both the finrank theorem and the power-series identity (1-X)^m·h = 1 are false at m=0. Fix: use the equal-for-m≥1, boundary-correct form C(n + m - 1, n) (= Nat.multichoose m n), which is exactly what Finset.card_finsuppAntidiag_nat_eq_choose (#(univ.finsuppAntidiag n) = (#s + n - 1).choose n) produces and what makes the identity hold for all m including 0. Correct the statement openly (docstring the choice) rather than adding an m ≥ 1 hypothesis that silently drops the degenerate case. Reusable API for "dim of degree-n homogeneous piece = # monomials": homogeneousSubmodule = restrictSupport {d | d.degree = n} (homogeneousSubmodule_eq_finsupp_supported), which has monomial basis MvPolynomial.basisRestrictSupport; then Module.finrank_eq_nat_card_basis + Nat.card_coe_set_eq + Set.ncard_coe_finset reduces finrank to the antidiag Finset.card. Power-series (1-X)^m·(∑ C(n+m-1,n) tⁿ) = 1: it is PowerSeries.invOneSubPow k m — use .inv_val + invOneSubPow_inv_eq_one_sub_pow + invOneSubPow_val_succ_eq_mk_add_choose, match coefficients C(d+n,d)=C(n+(d+1)-1,n) via Nat.choose_symm, and handle m=0 directly with PowerSeries.ext. Worked example: Chapter2/Problem2_8_11.lean (finrank_homogeneous_mvPolynomial, hilbertSeries_mvPolynomial).

Genuine tensor-multiplicity tables: prove the character identity, don't chase a tensor-product iso (Example 4.9.1 S₃ — DONE, #5377, Chapter4/Example4_9_1.lean). The non-vacuous form of a Clebsch-Gordan table V_i ⊗ V_j ≅ ⊕_k n_{ij}^k V_k is the character identity χ_i(g)·χ_j(g) = Σ_k n_{ij}^k χ_k(g) proved from real reps — you need neither the module iso nor CharEqIso (which lives in Ch5, unimportable from Ch4). Recipe: build the irreducibles as FDRep ℂ G and get each character as a closed-form trace (for S₃ = Equiv.Perm (Fin 3): trivial = 1, sign = (Equiv.Perm.sign g : ℂ) via charRep, standard = #fix(g) − 1 via the sum-zero subrep of the permutation rep — rebuild the sorry-free Ch5 Discussion5_11_examples permRep/stdSub/stdRep_character locally since Ch5 imports Ch4). The whole table then collapses to a polynomial identity in those closed forms, and the only group-specific input is one decidable fact ∀ g, (sign g, #fix g) ∈ {finite class values} proved by revert g; decide (do NOT state it for a fixed g — that is not decidable). Proof shape: simp only [irrep_char, Fin.sum_univ_three]; fin_cases i <;> fin_cases j <;> simp only [<matrix-cons lemmas>, Fin.isValue] <;> rcases <class-cases> g <;> rw [<sign-coe>, hs, hf]; push_cast; ring. Bridge to genuine tensor products with FDRep.char_tensor (V W) : (V ⊗ W).character = V.character * W.character + Pi.mul_apply (needs open CategoryTheory MonoidalCategory). Axiom-clean, no native_decide. S₄/A₅ follow the same pattern (#5442/#5443); A₅ additionally needs the two 3-dim icosahedral reps with golden-ratio values over ℚ(√5). A₅ DONE (#5776, PR #5846, same file): reuse the genuine catalogue Etingof.Example4_8_1.A5.irrepA5 (= ![repTriv, repC3plus, repC3minus, repC4, repC5]) + its class-rep character values irrepA5_character_book (over Q5 = ℚ(√5)) verbatim — import EtingofRepresentationTheory.Chapter4.Example4_8_1 (no cycle; 4_8_1 imports only Mathlib). Two lessons that cost real time:

• Do the golden-ratio arithmetic in Q5, NOT ℂ. A₅'s characters are class functions, so χ_i(g) = Q5toC (chiA5 i (classIdxA5 g)) (via classIdxA5_spec + FDRep.char_conj); the tensor identity then reduces to a 5·5·5 case split over the classes. Closing that split directly over ℂ with push_cast <;> (first | ring | linear_combination …·sqrt5_sq) ran 44 minutes then crashed — the first backtracking runs ring over ℂ-with-√5 under a bumped heartbeat budget, ×125. Instead prove the identity in Q5 (chiA5 i j * chiA5 i' j = Σ q5Nat(n)·chiA5 k j), where √5²=5 is baked into Q5.mul, so each case is pure rational norm_num on re/im (no √5, no ℂ); then transport to ℂ once via a hand-proved ring-hom lemma Q5toC_mul (a b) : Q5toC (a*b) = Q5toC a * Q5toC b (simp [Q5.mul_re, Q5.mul_im]; push_cast; linear_combination (-(a.im*b.im))*sqrt5_sq) plus the existing Q5toC_add. Whole file drops to ~4 min. Q5 has Mul/Add/Neg/Zero/One/OfNat but no CommRing/NatCast/AddCommMonoid — so no Finset.sum/•/map_sum over Q5; write the RHS as an explicit Fin.sum_univ_five of q5Nat n * chiA5 k j with q5Nat n := ⟨(n:ℚ),0⟩.
• FDRep.char_conj V g h : V.character (h*g*h⁻¹) = V.character g — rewrite the character argument only. To turn χ(g) into χ(classRep (classIdx g)) given hc : c * classRep (classIdx g) * c⁻¹ = g, a bare rw [← hc] also rewrites the g inside classIdx g on the RHS, corrupting the goal. Localise it: have key : χ g = χ (classRep (classIdx g)) := by rw [← FDRep.char_conj V (classRep (classIdx g)) c, hc] (the ← targets the standalone χ (classRep …), then hc collapses c*·*c⁻¹ to g).
• Kernel decide memory OOMs CI — reduce group sums to class sums BEFORE deciding, and split big files (#5852, PR #5854). A single decide of a 60×60 = 3600-term character double sum under maxHeartbeats 2000000000 cost ~12 GB of kernel memory and OOM-killed the 16 GB CI runner for two days (zEnd_cube_trace); heartbeats bound time, not memory, so a "just raise the budget" decide can pass locally and still kill CI. If you find yourself raising maxHeartbeats past ~4·10⁶ for a decide, restructure instead: (a) any conjugation-invariant summand (characters, fixCardM, tr(z·ρ(·)) for central z) collapses ∑ g : A₅ to the 5 class representatives weighted by classIdxA5_card sizes — the abstract pieces are S4.fixCardM_conj, A5.sum_fixCard_classfn, and the centrality+trace-cyclicity argument in zEnd_cube_trace; the kernel then only ever evaluates 5 (not 60, not 3600) terms. (b) Elaboration memory ratchets across a file (~13 GB cumulative for the old 2755-line Example4_8_1.lean even after (a)) — split into chained modules so each lean process peaks lower (now Example4_8_1/{Q8,S4,A5Classes,A5Reps,A5Lambda2,A5Golden}.lean + umbrella, peaks 5.6–9.7 GB; measure with ps -o rss= sampling during lake build). Chained imports also serialize the heavy modules in CI, so their peaks never stack. Micro-splitting one decide via fin_cases i <;> (revert g; decide) does NOT reduce peak (the elaborator still evaluates every column in one declaration) — don't bother.

This saved 2+ sessions in Waves 47-49 by catching false statements early, an entire D̃₄ proof attempt (#4566), a Ch5 Wall 3 R2.b.i attempt against a false pointwise-vanishing residual lemma (#2769 → #4584), and a research-level Cauchy proof attempt against a false multiplicity-one character identity (#4944).

Worked recipe for genuine small-group character tables (Example 4.8.1 family — #5428 done for Q₈, #5429 S₄, #5430 A₅ triv/ℂ⁴/ℂ⁵). The Q₈ table is sorry-free, native_decide-free, and axiom-clean (propext/Classical.choice/Quot.sound only) in Chapter4/Example4_8_1.lean (namespace Etingof.Example4_8_1.Q8). The 1-dim, sign, permutation-derived (stdRepM deleted-perm), and tensor-twist rows of Q₈/S₄/A₅ all follow the identical explicit-construction moves below — but the remaining #5431 (decomposed into #5449/#5450) does NOT, and the explicit-matrix moves are the wrong tool there:

• The two 3-dim A₅ icosahedral reps ℂ³₊/ℂ³₋ (golden-ratio χ) cannot be built as explicit-matrix MonoidHoms out of alternatingGroup (Fin 5). map_mul over 60 elements is infeasible by decide (even over the DecidableEq ring Q5 = ℚ[√5]), and the algebraic route would need PresentedGroup {a⁵,b²,(ab)³} ≃* A₅ (the (2,3,5) von Dyck group has order 60 — Todd–Coxeter), which is not in Mathlib. The only feasible rigorous route is the central-element eigenspace of Λ²(ℂ⁴): Λ²(ℂ⁴) ≅ ℂ³₊ ⊕ ℂ³₋, and z = Σ_{c∈C} ρ(c) (one 5-cycle class, 12 elts) acts as 4φ/4φ' (min poly X²−4X−16), so each rep is an eigenspace-Subrepresentation, with character via the projector (z−4φ'·id)/(4√5) and LinearMap.trace_eq_sum_trace_restrict. Heavy but uses existing infra (FDRep.char_tensor in Discussion_4_4.lean, Subrepresentation, Module.End.eigenspace, S4.fixCardM). Do not attempt explicit matrices here. Phase A landed (#5449 → PR #5454): Λ²(ℂ⁴) is now a genuine FDRep Etingof.Example4_8_1.A5.lam2 (= range asym ⊆ repC4 ⊗ repC4, asym = ½(1−β) the antisymmetriser), with lam2_char_formula : lam2.character g = ½(repC4.character g ^2 − repC4.character (g*g)) and lam2_character : … (classRepA5 j) = ![6,0,-2,1,1] j, axiom-clean (no native_decide). The remaining eigenspace split (z = Σ_{c∈C} lam2.ρ c → ℂ³₊/ℂ³₋) is #5453: consume lam2/lam2_character, do NOT rebuild the exterior square. Two reusable lessons from Phase A: (a) the swap-trace identity trace(swap ∘ map A B) = trace(A∘B) is copyable from Chapter5/FrobeniusSchurRealType.lean (trace_comm_comp_map) specialised to ℂ (Ch4 cannot import Ch5); the antisymmetric-subrep character then comes from two LinearMap.trace_eq_sum_trace_restrict over the ±1-eigenspaces of β (the β = ∓1 on range a/ker a facts close by linear_combination/module after LinearMap.smul_apply+LinearMap.sub_apply+Module.End.one_apply). (b) The idempotent-projection lemmas are in namespace LinearMap — write LinearMap.IsIdempotentElem.isCompl asym_idem / LinearMap.IsIdempotentElem.mem_range_iff asym_idem (bare asym_idem.isCompl/.mem_range_iff fail: IsIdempotentElem p unfolds to the Eq p*p=p, so dot-notation resolves to Eq.*). Feed the IsCompl (range a) (ker a) to DirectSum.isInternal_submodule_iff_isCompl ![range a, ker a] zero_ne_one huniv for the IsInternal the trace lemma needs.
• The "five simples + five conjugacy classes ⇒ complete table" certificate needs #(irreducible FDRep ℂ G) = #(ConjClasses G), which Mathlib does NOT package (RepresentationTheory/ has simple_iff_char_is_norm_one, char_orthonormal, but no ConjClasses-count bridge) — this count theorem is exactly what the rejected native_decide orthonormality stood in for, and must be proven as reusable repo infra (or replaced by a decidable IsCharacterTable predicate).
• Finiteness of the set of simple modules over a finite-dimensional algebra IS provable from Mathlib primitives — do NOT defer it as "missing infra" (#6090, landed as Etingof.finite_simpleModuleClasses in Chapter4/Exercise4_2_3.lean, sorry-free). Goal shape: Finite (SimpleModuleClasses.{u} R) (iso classes of simple R-modules) for R finite-dim over a field k. Route, all from Mathlib: (a) rad = Ring.jacobson R annihilates every simple module — IsSemisimpleModule.jacobson_le_annihilator R M (a simple module is semisimple), giving Module.IsTorsionBySet R M (Ring.jacobson R); (b) descend to the semisimple quotient A = R ⧸ Ring.jacobson R via Module.IsTorsionBySet.module (mark the descended Module A M @[implicit_reducible], else "class type must be marked reducible"), and transfer simplicity with LinearMap.isSimpleModule_iff_of_bijective applied to the identity semilinear map hM.semilinearMap (its map_smul' is rfl, so mk r • x = r • x is definitional — this makes R-linear ⇄ A-linear equiv promotion/demotion trivial { e with map_smul' := fun a x => by obtain ⟨r,rfl⟩ := Ideal.Quotient.mk_surjective a; exact e.map_smul r x }); (c) A semisimple: isArtinian_of_tower k inferInstance → IsArtinianRing R → IsSemiprimaryRing R (Mathlib instance) whose IsSemiprimaryRing.isSemisimpleRing field gives IsSemisimpleRing A (no need to import Chapter8/SemiprimaryAlgebra); (d) over semisimple A, Finite (isotypicComponents A A) is a Mathlib instance (Mathlib/RingTheory/SimpleModule/Isotypic.lean, needs IsNoetherian), every simple embeds as an ideal (IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModule), and ⟦X⟧ ↦ isotypicComponent A A (descent of X) is a choice-free, injective map into that finite type (well-defined & injective via LinearEquiv.isotypicComponent_eq + IsIsotypicOfType.isotypicComponent + isIsotypicOfType_submodule_iff). Finite.of_injective finishes — no Shrink/universe juggling. Reuse this for any Ch4/Ch9 count that first needs "finitely many simples". To lift a categorical Iso in (simpleProp _).FullSubcategory to/from a LinearEquiv: (ObjectProperty.ι _).mapIso iso |>.toLinearEquiv one way, P.fullyFaithfulι.preimageIso e.toModuleIso the other; and attribute [local instance] CategoryTheory.isIsomorphicSetoid is needed for ≈/Quotient.lift since the setoid is passed explicitly in SimpleModuleClasses.
• The minimal polynomial z²−20z−400=0 splitting Λ²(ℂ⁴) into ℂ³₊/ℂ³₋ (#5459 crux) does NOT need an explicit 16×16 matrix decide — get it from multiplicity-freeness for free (landed as lam2_hom_finrank, zEnd_trace, PR #5741). FDRep.scalar_product_char_eq_finrank_equivariant V V : ⅟(card G) • ∑_g χ(g)χ(g⁻¹) = finrank ℂ (V ⟶ V) (in RepresentationTheory/Character.lean; needs [Fintype G] [Invertible (card G : ℂ)] — supply the invertible instance by rw [show Fintype.card G = 60 from …]; exact invertibleOfNonzero (by norm_num)) turns ⟨χ_{Λ²},χ_{Λ²}⟩ = 2 into dim_ℂ End_G(Λ²) = 2. Evaluate the sum honestly by writing χ_{Λ²}(g)=½·P(g) with the integer P(g)=(fix₅(g)−1)²−(fix₅(g·g)−1) (from lam2_char_formula+repC4_char; the character is real so χ(g⁻¹)=χ(g) via fixCardM_inv and g⁻¹g⁻¹=(gg)⁻¹), factor out ¼, and ∑_g P(g)²=480 by decide (integer sum, no ℚ/native_decide). Then dim End=2 means the three endos {1, z, z²} are linearly dependent (3 vectors in a 2-dim Hom-space), forcing a degree-≤2 minimal polynomial; the two trace identities pin it exactly: tr z=60 (each ρ(g·r·g⁻¹) is conjugate to a 5-cycle so χ_{Λ²}=1, sum of 1 over 60 elts — via FDRep.char_conj+lam2_character 3; note LinearMap.trace ℂ ↥lam2Sub.toSubmodule (lam2Sub.toRepresentation x) = lam2.character x holds by rfl) and tr z²=3600, giving μ⁺+μ⁻=20, μ⁺μ⁻=−400 (μ±=10±10√5). Note the eigenvalue scaling differs from the earlier bullet: this uses z = Zamb = Σ_{g∈A₅} ρ(g·r·g⁻¹) (all 60 elts = 5·class-sum, chosen so centrality is a one-line reindex), so μ±=20φ/20φ', min poly z²−20z−400 — NOT the class-sum-only X²−4X−16. Remaining after PR #5741: package zEnd as a categorical φ : lam2 ⟶ lam2 (equivariant via zEnd_central), extract the degree-2 relation, then projector P⁺=(z−μ⁻)/(20√5) gives finrank=3; characters via the two-eigenspace LinearMap.trace_eq_sum_trace_restrict system. Trace-moment lemmas tr(zⁿ) (zEnd_sq_trace =3600, zEnd_cube_trace =96000, #5778): mirror the sibling one level up, and never rw [map_mul] on a trace(a*b*c)=… goal. map_mul sees LinearMap.trace (a →ₗ[ℂ] ℂ functional) and tries to synthesize MulHomClass for it, silently mangling the goal into trace a * trace b * trace c before failing — the tell is failed to synthesize instance … MulHomClass (… →ₗ[ℂ] ℂ). Do the map_mul/associativity rewrite inside a separate endomorphism-level have hrw : z*…*ρ(g·r·g⁻¹) = ρ g * (…) * ρ g⁻¹ (there map_mul correctly targets lam2Sub.toRepresentation), then rw [hrw, LinearMap.trace_mul_comm, ← mul_assoc, ← map_mul, inv_mul_cancel, map_one, one_mul]. For tr(zⁿ): centrality of the product zⁿ⁻¹ ((zEnd_central g).mul_right (zEnd_central g) builds Commute (ρ g) (z*z) for the cube) makes every conjugate summand's trace equal, so tr(zⁿ)=60·tr(zⁿ⁻¹·ρ(r)); unfold one more z and hit zEnd_comp_char to land on an honest ∑_h ∑_{h'} χ-style group sum by decide. That decide scales ~60× per extra z factor (cube = 3600 terms, ~4 min build, maxHeartbeats 2000000000/maxRecDepth 100000); a classIdxA5 class-index reduction (sub-issue #5) would cut it to 60 terms but fixCardM alone can't separate the two 5-cycle classes, so that fallback needs the dedicated work. When copying the sibling's key : (∑ …) = N := by decide, replicate its parenthesis nesting exactly — an extra ( around the summand leaves the outer (∑…) unclosed and the parser dies on := with "unexpected token ':='; expected ')'".
• rw gotchas hit while landing PR #5741 (both cost a rebuild): (1) rewriting a hypothesis of the form ⅟(card G) • S = … with card G = 60 fails motive is not type correct — the ⅟ carries an Invertible (card G) instance that can't be abstracted; fix by rw [invOf_eq_inv, smul_eq_mul] FIRST (drops the instance-dependence), then rewrite the cast freely. (2) A rw [… , lam2_character 3] chain can silently close the goal via its trailing rfl (the ![6,0,-2,1,1] 3 matrix index reduces to 1 definitionally), so a following norm_num/rfl throws "no goals to be solved" — either drop the trailing tactic, or make the closing step robust with simpa using lam2_character 3 (simp's Matrix.cons_val_* evaluate the index either way).
• motive is not type correct in Fin n/Nat.Partition/List-index proofs (#6076, Problem 5.16.2; two variants, each cost a rebuild). (1) With hsum : la.sortedParts.sum = n, doing rw [← hsum] to turn a goal m < n into m < …sum fails — n is the type parameter of la : n.Partition, so abstracting it breaks la's type. Fix: never rw [← hsum]; use a term (lt_of_lt_of_eq hmlt hsum : m < n) or forward rw [hsum] in a goal that mentions only …sum. (2) set r := rowOfPos … with hr before establishing a getElem fact, then rw [hr] into the index of la.sortedParts[r], fails (the r < length membership proof depends on r). Fix: state the raw haves (rowOfPos_lt_length, colOfPos_lt_getElem, pos_decomp_list) first, then set r/set c — set folds them automatically and no rw-into-getElem is needed. Also: List.sum_take_succ l i h : (l.take (i+1)).sum = (l.take i).sum + l[i] is cleaner than take_succ_eq_append_getElem + simp.
• Reusing earlier-chapter helpers that are private (#6076). Much of the Young-tableau coefficient/counting machinery (youngSymmetrizer_pq_coeff, youngSymmetrizer_support in PolytabloidBasis.lean; rowOfPos_lt_iff, rowOfPos_colOfPos_canonical, card_filter_val_lt, swap_mem_RowSubgroup, … in Lemma5_13_2.lean) is private. grep -n "private (theorem|lemma) <name>" and remove the private keyword rather than reproving — de-privatizing is a one-word, regression-free change (verified by a full lake build), far cheaper than re-deriving ~80 lines of MonoidAlgebra/positional-induction proofs.
• Extracting the golden-ratio characters χ₊/χ₋ from the eigenspace split (#5781, PR #5843, landed as repC3plus_character/repC3minus_character). Solve the 2×2 trace system χ₊+χ₋ = χ_{Λ²} and μ⁺χ₊+μ⁻χ₋ = tr(z·ρ(g)) per class j: LinearMap.trace_eq_sum_trace_restrict over the IsCompl eigenspace pair E± of zEnd gives both equations (on E±, z·ρ(g) restricts to μ±·(ρ(g)|E±) — prove via Module.End.mem_eigenspace_iff.mp (hf i x.2)), then mul_left_cancel₀ (muPlus_sub_muMinus ≠ 0) + linear_combination (±10)*sqrt5_sq. Two traps that cost ~7 rebuilds:
  • The trace-transport repC3plus.character g = tr(ρ(g)|E⁺) hits an AddCommGroup instance diamond. LinearMap.trace_conj' (needed to move the trace across the intertwiner e : E⁺ ≃ repC3plusSub.toSubmodule) requires [AddCommGroup ↥E⁺], but a doubly-nested subtype ↥E⁺ (E⁺ : Submodule ℂ ↥lam2Sub.toSubmodule) defaults to Submodule.addCommMonoid, so e records E⁺.addCommMonoid and you get "Application type mismatch: argument e … E.addCommMonoid vs AddCommGroup.toAddCommMonoid". Fix: letI : AddCommGroup (↥E) := E.addCommGroup as the first line of the proof — the local high-priority instance makes every ↥E (the equiv, both traces) resolve the AddCommGroup-derived AddCommMonoid, matching trace_conj'. Build the intertwiner with LinearEquiv.ofBijective of a corestricted (lam2Sub.subtype ∘ₗ E.subtype).codRestrict … (mirrors Theorem5_25_2.lean's evalMap); Submodule.equivMapOfInjective hits the same diamond. The whole transport lemma needs set_option synthInstance.maxHeartbeats 400000 + maxHeartbeats 800000 (the nested subtype makes defeq slow, not wrong).
  • Q5toC arithmetic: use norm_num, not simp only. simp only [Q5.ofNat_re, Q5.neg_re, …] does not reduce (3 : Q5).re/(-1 : Q5).im (leaves opaque re 3 in the goal); norm_num [Q5toC, muPlus, muMinus, chiA5, Matrix.cons_val_*, Q5.mk_re, Q5.ofNat_re, …] does, and outright closes the all-rational classes (incl. the all-zero class 1) — leaving only the two 5-cycle classes for linear_combination. Never decide on Q5 (the 1/60/ℚ-normalisation stalls the kernel).

Honest (native_decide-free) arithmetic over the Q5 = ℚ[√5] character table (#5459 deliverable 4, the retired A5_orthonormal, sorry-free axiom-clean in Chapter4/Example4_8_1.lean). Any computation over the book table chiA5 : Fin 5 → Fin 5 → Q5 (the orthonormality ip sum, and the upcoming #5468/#5469 character/norm-one sums) — kernel decide stalls, but NOT on the √5/foldr: it stalls on ℚ-normalisation, getting stuck at the Rat.num Decidable instance even after the List.ofFn/foldr is removed. This triggers on any non-integer ℚ in the entries, not only a 1/N prefactor (e.g. 1/60): a bare (chiA5 1 j + chiA5 2 j).re = … decide over the ⟨1/2, ±1/2⟩ golden-ratio entries of rows 1/2 also stalls. So do not reach for decide on anything touching the 1/2 entries; the working pattern is Q5.ext/norm_num (the Q5.*_re/_im projection set below closes .re/.im of Q5 sums directly — e.g. lam2_character_eq_sum : lam2.character (classRepA5 j) = Q5toC (chiA5 1 j) + Q5toC (chiA5 2 j), the χ_Λ² = χ₊+χ₋ identity, via ← Q5toC_add then fin_cases j <;> simp only [chiA5, cons_val…] <;> norm_num [Q5.add_re, …]):

1. A sumFin_five-style explicit-unfold lemma (sumFin f = f 0 + (f 1 + (f 2 + (f 3 + (f 4 + 0)))), proved by simp only [sumFin, List.ofFn_succ, List.ofFn_zero, List.foldr_cons, List.foldr_nil]; rfl). The bare List.ofFn/List.foldr simp lemmas reduce inconsistently in the big file vs a scratch (sometimes leaving an un-reduced Fin.foldr 5 …), so pre-unfold the fixed-arity sum into a named lemma rather than relying on List.ofFn inside the main proof.
2. Q5 projection simp lemmas mk/zero/one/add/neg/mul/ofRat _re/_im (all rfl). The OfNat ones MUST use no_index: theorem ofNat_re (n : ℕ) : (no_index (OfNat.ofNat n) : Q5).re = (OfNat.ofNat n : ℚ) := rfl — without no_index, simp's discrimination tree indexes on the literal and the lemma silently makes "no progress" on (3 : Q5).re (the custom OfNat Q5 n instance, not an AtLeastTwo one). Keep them non-@[simp] and pass explicitly: marking them @[simp] does NOT add warnings (the ~21 unusedSimpArgs in this file are pre-existing, e.g. Matrix.toLin'_apply at the Q₈ rho_apply), but explicit-only keeps the blast radius surgical.
3. One norm_num pass after fin_cases i <;> fin_cases j <;> (first | rw [if_pos rfl] | rw [if_neg (by decide)]) <;> apply Q5.ext <;> norm_num [ip, Q5.sumFin_five, sizesA5, chiA5, <all the Q5 _re/_im>, Matrix.cons_val_zero, cons_val_one, cons_val_two, cons_val_three, cons_val_four, head_cons, tail_cons]. norm_num (NOT simp only) is what reduces the OfNat literals and the 1/60 * (rational) = 0/1 arithmetic; the cons_val_two/three/four lemmas (they DO exist in this Mathlib — the existing repC4_character uses them) handle matrix indices ≥ 2 that cons_val_zero/one+head_cons miss. Probe the whole proof in a /tmp scratch (gtimeout 400 lake env lean) before the 90s file build.

Reusable pieces and the gotchas that each cost a build cycle: