Actual-index certificate assembly for a genuine right ladder

This file combines the pure Fin.rev adapter with the abstract reversed-rung propagation. It remains entirely categorical.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.familyArrowIso {C : Type u} [CategoryTheory.Category.{v, u} C] (Z Y : ℕ → C) (b : (k : ℕ) → Z k ⟶ Y k) {m n : ℕ} (e : m = n) : CategoryTheory.Arrow.mk (b m) ≅ CategoryTheory.Arrow.mk (b n)

Pointwise arrows at equal indices are isomorphic in the arrow category. Writing this by equality elimination avoids exposing dependent transports in later statements.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.familyShortComplexIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (S : ℕ → CategoryTheory.ShortComplex C) {m n : ℕ} (e : m = n) : S m ≅ S n

A family of short complexes takes equal indices to isomorphic complexes.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.genuineRightStep {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} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (i : ℕ) : CategoryTheory.ShortComplex C

The genuine displayed right-ladder step at a natural-number index.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ofInfiniteSpecialRightLadder_essentialArrowIso_at {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} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (j : Fin (n + 1)) : CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).b j) ≅ CategoryTheory.Arrow.mk (R.b ↑j.rev)

Forgetting the reversed-prefix wrapper at one index changes no arrow.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ofInfiniteSpecialRightLadder_paddedArrowIso_at {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} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (j : Fin (n + 1)) : CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow j) ≅ CategoryTheory.Arrow.mk (RightLadder.Comparison.paddedArrow R ↑j.rev)

The same pointwise identification for zero-padded arrows.

def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ofInfiniteSpecialRightLadder_essentialArrowIso_last {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} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) : CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).b (Fin.last n)) ≅ CategoryTheory.Arrow.mk (R.b 0)

The last arrow of a reversed finite window is the original arrow at index zero.

noncomputable def QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.ofInfiniteSpecialRightLadder_paddedArrowIso_last {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} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) : CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)) ≅ CategoryTheory.Arrow.mk (RightLadder.Comparison.paddedArrow R 0)

At the last reversed index, the aligned padded arrow is literally the initial padded arrow of the genuine right ladder.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.terminalIso_to_reversedInitialPadding {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} {X₀ Y₀ U₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (hterminal : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk a₀)) : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)))

An isomorphism from the terminal essential left arrow to the genuine initial arrow closes the reversed comparison at its final index.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.initialPreviousCancellation_of_terminalEssentialIso {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} {X₀ Y₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R (n + 1)).U 0) (n + 1)) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hterminal : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last (n + 1))) ≅ CategoryTheory.Arrow.mk a₀)) : Nonempty (RightLadder.Comparison.PreviousCancellation R 0)

The terminal four-cycle of a nonempty reversed window cancels the zero summand in the genuine initial right arrow. This is the first PreviousCancellation datum required by the finite comparison certificate.

The direct-finiteness argument is a parameter here; for a finite tau-category it is discharged by FiniteTauCategoryData.isIso_of_isSplitMono_end.

Actual-index certificate data

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.actualPreviousCancellationIso_all_of_boundaryEmbedding {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} {X₀ Y₀ U₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding (ReversedRightPrefix.ofInfiniteSpecialRightLadder R n) U₀) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)))) (i : Fin n) : Nonempty (CategoryTheory.Arrow.mk (RightLadder.Comparison.paddedArrow R ↑i) ≅ CategoryTheory.Arrow.mk (R.b ↑i))

Reindex every aligned cancellation isomorphism back to the corresponding natural-number step of the genuine right ladder.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.actualReversedStepIso_all_of_boundaryEmbedding {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} {X₀ Y₀ U₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding (ReversedRightPrefix.ofInfiniteSpecialRightLadder R n) U₀) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)))) (i : Fin n) : Nonempty (LeftLadder.stepComplex (L.b i.rev.castSucc) (L.b i.rev.succ) (L.f i.rev) (L.g i.rev) (L.h i.rev) ⋯ ⋯ ≅ genuineRightStep R ↑i)

Reindex every aligned cross-mesh isomorphism back to the corresponding genuine right-ladder step.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.exists_actualCertificateStep_of_boundaryEmbedding {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} {X₀ Y₀ U₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding (ReversedRightPrefix.ofInfiniteSpecialRightLadder R n) U₀) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)))) (i : Fin n) : ∃ (p : RightLadder.Comparison.PreviousCancellation R ↑i), Nonempty (T.leftMesh (R.Z (↑i + 1) ⊞ R.U (↑i + 1)) ≅ RightLadder.Comparison.squareComplex R (↑i) p)

One actual-index package containing exactly the two dependent fields of RightLadder.Comparison.Certificate: cancellation of the previous padded arrow and identification of the next-source left mesh with the common square complex.

theorem QuotientSubmoduleEquidistribution.Iyama.TauSequenceComparison.nonempty_certificate_to_leftZeroBoundary_of_boundaryEmbedding {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} {X₀ Y₀ U₀ : C} {a₀ : X₀ ⟶ Y₀} (R : RightLadder.InfiniteSpecialRightLadder T.toFiniteRightTauCategoryData a₀) (n : ℕ) (L : LeftLadder.FiniteSpecialLeftLadderFromZero T U₀ n) (E : BoundaryEmbedding (ReversedRightPrefix.ofInfiniteSpecialRightLadder R n) U₀) (hfinite : ∀ (X : C) (e : X ⟶ X), CategoryTheory.IsSplitMono e → CategoryTheory.IsIso e) (hlast : Nonempty (CategoryTheory.Arrow.mk (L.b (Fin.last n)) ≅ CategoryTheory.Arrow.mk ((ReversedRightPrefix.ofInfiniteSpecialRightLadder R n).paddedArrow (Fin.last n)))) : Nonempty (RightLadder.Comparison.Certificate R n (L.b 0))

Full finite comparison certificate, ending at the chosen left zero-boundary arrow. This is the production-facing assembly theorem: all dependent PreviousCancellation and leftSquareIso fields are constructed from the closed reversed comparison.