Infinite and finite special left ladders from a zero boundary

This file combines target conormalization and complementary-successor specialness into an unconditional dependent left-ladder construction. It then exposes flat infinite families and exact finite prefixes for Iyama, Tau-categories I, Lemma 6.4.1(1)(ii). The construction is entirely categorical and uses no concrete algebra or module classification.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.specialLeftLadderBuilder {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) : SpecialLeftLadderBuilder T

The unconditional categorical builder supplied by target normalization and dual successor specialness.

@[reducible, inline]

abbrev QuotientSubmoduleEquidistribution.Iyama.LeftLadder.PackedSpecialCosplitState {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) : Type (max u u v)

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.nextConormalization {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) {Y : C} (s : SpecialCosplitState T Y) : SpecialConormalization T s.rawSuccessor

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.nextPackedCosplitState {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) (p : PackedSpecialCosplitState T) : PackedSpecialCosplitState T

structure QuotientSubmoduleEquidistribution.Iyama.LeftLadder.SpecialLeftLadderRung {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) (p : PackedSpecialCosplitState T) : Type v

• f : p.fst ⟶ (nextPackedCosplitState T B p).fst
• g : p.snd.Z ⟶ (nextPackedCosplitState T B p).snd.Z
• h : p.snd.Z ⟶ (nextPackedCosplitState T B p).snd.U
• comm : CategoryTheory.CategoryStruct.comp self.f (nextPackedCosplitState T B p).snd.b = CategoryTheory.CategoryStruct.comp p.snd.b self.g
• hzero : CategoryTheory.CategoryStruct.comp p.snd.b self.h = 0
• meshIso : Nonempty (T.leftMesh p.fst ≅ stepComplex p.snd.b (nextPackedCosplitState T B p).snd.b self.f self.g self.h ⋯ ⋯)

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.nonempty_specialLeftLadderRung {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) (p : PackedSpecialCosplitState T) : Nonempty (SpecialLeftLadderRung T B p)

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.chooseSpecialLeftLadderRung {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) (p : PackedSpecialCosplitState T) : SpecialLeftLadderRung T B p

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.isSpecial_of_isZero_target {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (R : CategoricalRadical.NilpotentRadicalData C) {X Z : C} (hZ : CategoryTheory.Limits.IsZero Z) (a : X ⟶ Z) : IsSpecial R a

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.zeroInitialCosplitState {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (U₀ : C) : SpecialCosplitState T U₀

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.zeroInitialPackedCosplitState {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (U₀ : C) : PackedSpecialCosplitState T

def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.iteratePackedCosplitState {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) (p₀ : PackedSpecialCosplitState T) : ℕ → PackedSpecialCosplitState T

Flat infinite ladder and exact finite prefixes

structure QuotientSubmoduleEquidistribution.Iyama.LeftLadder.InfiniteSpecialLeftLadderFromZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (U₀ : C) : Type (max u v)

• Y : ℕ → C
• Z : ℕ → C
• U : ℕ → C
• b (n : ℕ) : self.Y n ⟶ self.Z n
• b_special (n : ℕ) : IsSpecial T.radical (self.b n)
• initialSourceIso : U₀ ≅ self.Y 0
• initialTargetZero : CategoryTheory.Limits.IsZero (self.Z 0)
• b_zero : self.b 0 = 0
• f (n : ℕ) : self.Y n ⟶ self.Y (n + 1)
• g (n : ℕ) : self.Z n ⟶ self.Z (n + 1)
• h (n : ℕ) : self.Z n ⟶ self.U (n + 1)
• comm (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.f n) (self.b (n + 1)) = CategoryTheory.CategoryStruct.comp (self.b n) (self.g n)
• hzero (n : ℕ) : CategoryTheory.CategoryStruct.comp (self.b n) (self.h n) = 0
• meshIso (n : ℕ) : Nonempty (T.leftMesh (self.Y n) ≅ stepComplex (self.b n) (self.b (n + 1)) (self.f n) (self.g n) (self.h n) ⋯ ⋯)

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.infiniteSpecialLeftLadderFromZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) (U₀ : C) : InfiniteSpecialLeftLadderFromZero T U₀

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.chosenInfiniteSpecialLeftLadderFromZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (U₀ : C) : InfiniteSpecialLeftLadderFromZero T U₀

The unconditional chosen infinite left ladder, with both dual-special operations supplied by the categorical construction in this package.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.InfiniteSpecialLeftLadderFromZero.terminalDomain_not_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} (L : InfiniteSpecialLeftLadderFromZero T U₀) (n : ℕ) {W : C} (q : U₀ ⟶ W) (hq : q ∈ (T.radical.ideal.pow n).hom U₀ W) (hqne : q ≠ 0) : ¬CategoryTheory.Limits.IsZero (L.Y n)

The compiled dual radical layer applies directly to the flat ladder. A nonzero degree-n morphism out of the original boundary object forces the domain of the nth left-ladder arrow to be nonzero.

structure QuotientSubmoduleEquidistribution.Iyama.LeftLadder.FiniteSpecialLeftLadderFromZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (U₀ : C) (n : ℕ) : Type (max u v)

• Y : Fin (n + 1) → C
• Z : Fin (n + 1) → C
• U : Fin (n + 1) → C
• b (i : Fin (n + 1)) : self.Y i ⟶ self.Z i
• b_special (i : Fin (n + 1)) : IsSpecial T.radical (self.b i)
• initialSourceIso : U₀ ≅ self.Y 0
• initialTargetZero : CategoryTheory.Limits.IsZero (self.Z 0)
• b_zero : self.b 0 = 0
• f (i : Fin n) : self.Y i.castSucc ⟶ self.Y i.succ
• g (i : Fin n) : self.Z i.castSucc ⟶ self.Z i.succ
• h (i : Fin n) : self.Z i.castSucc ⟶ self.U i.succ
• comm (i : Fin n) : CategoryTheory.CategoryStruct.comp (self.f i) (self.b i.succ) = CategoryTheory.CategoryStruct.comp (self.b i.castSucc) (self.g i)
• hzero (i : Fin n) : CategoryTheory.CategoryStruct.comp (self.b i.castSucc) (self.h i) = 0
• meshIso (i : Fin n) : Nonempty (T.leftMesh (self.Y i.castSucc) ≅ stepComplex (self.b i.castSucc) (self.b i.succ) (self.f i) (self.g i) (self.h i) ⋯ ⋯)

def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.InfiniteSpecialLeftLadderFromZero.prefix {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} (L : InfiniteSpecialLeftLadderFromZero T U₀) (n : ℕ) : FiniteSpecialLeftLadderFromZero T U₀ n

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.finiteSpecialLeftLadderFromZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (B : SpecialLeftLadderBuilder T) (U₀ : C) (n : ℕ) : FiniteSpecialLeftLadderFromZero T U₀ n

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.chosenFiniteSpecialLeftLadderFromZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (U₀ : C) (n : ℕ) : FiniteSpecialLeftLadderFromZero T U₀ n

The unconditional chosen finite prefix of a zero-initial special left ladder.

theorem QuotientSubmoduleEquidistribution.Iyama.LeftLadder.chosenFiniteSpecialLeftLadderFromZero_terminalDomain_not_isZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : FiniteTauCategoryData C Ind) (U₀ : C) (n : ℕ) {W : C} (q : U₀ ⟶ W) (hq : q ∈ (T.radical.ideal.pow n).hom U₀ W) (hqne : q ≠ 0) : ¬CategoryTheory.Limits.IsZero ((chosenFiniteSpecialLeftLadderFromZero T U₀ n).Y (Fin.last n))

The dual radical-layer conclusion on the literal terminal object of the chosen finite prefix.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.LeftLadder.FiniteSpecialLeftLadderFromZero.paddedArrow {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] {T : FiniteTauCategoryData C Ind} {U₀ : C} {n : ℕ} (L : FiniteSpecialLeftLadderFromZero T U₀ n) (i : Fin (n + 1)) : L.Y i ⟶ L.Z i ⊞ L.U i