TauLib · API Book II

TauLib.BookII.Enrichment.TwoCategories

TauLib.BookII.Enrichment.TwoCategories

Strict 2-category structure τ₂ on the τ-enriched category, with 2-morphisms (natural transformations) between holomorphic maps.

Registry Cross-References

  • [II.D55] 2-Category Structure — TwoCat, two_cat_assoc_check

  • [II.D56] 2-Morphism — two_morphism_check, two_morph_tower_check

  • [II.P13] Enrichment Iteration — enrichment_iteration_check, interchange_check

Mathematical Content

2-Category Structure (II.D55): The strict 2-category τ₂ has:

  • Objects: τ-objects (stages k of the primorial tower)

  • 1-morphisms: holomorphic endomorphisms (tower-coherent maps)

  • 2-morphisms: natural transformations between 1-morphisms

  • Vertical composition: pointwise composition of 2-morphisms

  • Horizontal composition: stagewise composition

Composition of 1-morphisms is the standard hol_comp from CategoryStructure: (f . g)(n, k) = f(g(n, k), k). Associativity holds definitionally.

2-Morphism (II.D56): A 2-morphism eta : f => g between 1-morphisms f, g : A -> B is a family eta_k : Z/P_kZ -> Z/P_kZ such that eta_k(f(x, k)) = g(x, k) for all x, and the family is tower-coherent. In the primorial setting, this means reduce(eta(f(x, l)), k) = eta(f(x, k)) for k <= l.

Enrichment Iteration (II.P13): The 2-category τ₂ is itself enrichable: Hom(f, g) for 1-morphisms f, g is a τ-object. This iterates: τ₃ exists, τ₄ exists, etc. The enrichment ladder is well-founded because each step uses the primorial tower’s finite stages — every hom-space at stage k is a finite set.

The interchange law verifies the 2-categorical axiom: (eta₂ ∘_v eta₁) ∘_h (mu₂ ∘_v mu₁) = (eta₂ ∘_h mu₂) ∘_v (eta₁ ∘_h mu₁)

Tau.BookII.Enrichment.OneCell

source@[reducible, inline]

abbrev Tau.BookII.Enrichment.OneCell :Type

[II.D55] 1-cell (1-morphism): a tower-coherent endomorphism on the primorial tower. Represented as (n, k) ↦ value at stage k. Equations

  • Tau.BookII.Enrichment.OneCell = (Tau.Denotation.TauIdx → Tau.Denotation.TauIdx → Tau.Denotation.TauIdx) Instances For

Tau.BookII.Enrichment.TwoCell

source@[reducible, inline]

abbrev Tau.BookII.Enrichment.TwoCell :Type

[II.D55] 2-cell (2-morphism): a tower-coherent family mediating between two 1-cells. eta mediates f => g means: eta(f(x, k), k) = g(x, k) for all x, k. Equations

  • Tau.BookII.Enrichment.TwoCell = (Tau.Denotation.TauIdx → Tau.Denotation.TauIdx → Tau.Denotation.TauIdx) Instances For

Tau.BookII.Enrichment.vert_comp

source def Tau.BookII.Enrichment.vert_comp (eta₂ eta₁ : TwoCell) :TwoCell

[II.D55] Vertical composition of 2-cells: (eta₂ ∘_v eta₁)(x, k) = eta₂(eta₁(x, k), k). If eta₁ : f => g and eta₂ : g => h, then eta₂ ∘_v eta₁ : f => h. Equations

  • Tau.BookII.Enrichment.vert_comp eta₂ eta₁ n k = eta₂ (eta₁ n k) k Instances For

Tau.BookII.Enrichment.horiz_comp

source def Tau.BookII.Enrichment.horiz_comp (eta mu : TwoCell) :TwoCell

[II.D55] Horizontal composition of 2-cells: (eta ∘_h mu)(x, k) = eta(mu(x, k), k). This composes 2-cells across different hom-spaces. Equations

  • Tau.BookII.Enrichment.horiz_comp eta mu n k = eta (mu n k) k Instances For

Tau.BookII.Enrichment.id_two_cell

source def Tau.BookII.Enrichment.id_two_cell :TwoCell

[II.D55] Identity 2-cell: id_2(x, k) = reduce(x, k). The identity 2-morphism on any 1-cell is the canonical reduction. Equations

  • Tau.BookII.Enrichment.id_two_cell n k = Tau.Polarity.reduce n k Instances For

Tau.BookII.Enrichment.TwoCat

source structure Tau.BookII.Enrichment.TwoCat :Type

[II.D55] 2-category structure certificate.

  • max_stage : Denotation.TauIdx Maximum stage depth.

  • max_val : Denotation.TauIdx Maximum input value.

Instances For

Tau.BookII.Enrichment.instReprTwoCat

source instance Tau.BookII.Enrichment.instReprTwoCat :Repr TwoCat

Equations

  • Tau.BookII.Enrichment.instReprTwoCat = { reprPrec := Tau.BookII.Enrichment.instReprTwoCat.repr }

Tau.BookII.Enrichment.instReprTwoCat.repr

source def Tau.BookII.Enrichment.instReprTwoCat.repr :TwoCat → ℕ → Std.Format

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.mk_two_cat

source def Tau.BookII.Enrichment.mk_two_cat (max_stage max_val : Denotation.TauIdx) :TwoCat

Construct a TwoCat certificate. Equations

  • Tau.BookII.Enrichment.mk_two_cat max_stage max_val = { max_stage := max_stage, max_val := max_val } Instances For

Tau.BookII.Enrichment.one_id

source def Tau.BookII.Enrichment.one_id :OneCell

Sample 1-cell: identity endomorphism. Equations

  • Tau.BookII.Enrichment.one_id n k = Tau.Polarity.reduce n k Instances For

Tau.BookII.Enrichment.one_sq

source def Tau.BookII.Enrichment.one_sq :OneCell

Sample 1-cell: squaring endomorphism. Equations

  • Tau.BookII.Enrichment.one_sq n k = Tau.Polarity.reduce (n * n) k Instances For

Tau.BookII.Enrichment.one_dbl

source def Tau.BookII.Enrichment.one_dbl :OneCell

Sample 1-cell: doubling endomorphism. Equations

  • Tau.BookII.Enrichment.one_dbl n k = Tau.Polarity.reduce (2 * n) k Instances For

Tau.BookII.Enrichment.one_zero

source def Tau.BookII.Enrichment.one_zero :OneCell

Sample 1-cell: zero endomorphism. Equations

  • Tau.BookII.Enrichment.one_zero x✝¹ x✝ = 0 Instances For

Tau.BookII.Enrichment.two_sq

source def Tau.BookII.Enrichment.two_sq :TwoCell

Sample 2-cell: the squaring transformation (as a 2-morphism from id to sq). eta(x, k) = reduce(x * x, k). For x = id(y, k) = reduce(y, k), we get eta(id(y,k), k) = reduce(reduce(y,k)^2, k) = sq(y, k). Equations

  • Tau.BookII.Enrichment.two_sq n k = Tau.Polarity.reduce (n * n) k Instances For

Tau.BookII.Enrichment.two_dbl

source def Tau.BookII.Enrichment.two_dbl :TwoCell

Sample 2-cell: doubling transformation. Equations

  • Tau.BookII.Enrichment.two_dbl n k = Tau.Polarity.reduce (2 * n) k Instances For

Tau.BookII.Enrichment.two_cat_assoc_check

source def Tau.BookII.Enrichment.two_cat_assoc_check (bound db : Denotation.TauIdx) :Bool

[II.D55] Associativity of horizontal composition: (eta ∘_h (mu ∘_h nu))(x, k) = ((eta ∘_h mu) ∘_h nu)(x, k). Both sides expand to eta(mu(nu(x, k), k), k). Equations

  • Tau.BookII.Enrichment.two_cat_assoc_check bound db = Tau.BookII.Enrichment.two_cat_assoc_check.go bound db 2 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookII.Enrichment.two_cat_assoc_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.two_cat_assoc_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.two_cat_unit_check

source def Tau.BookII.Enrichment.two_cat_unit_check (bound db : Denotation.TauIdx) :Bool

[II.D55] Identity 2-cell is a unit for vertical composition: (id_2 ∘_v eta)(x, k) = eta(x, k) when eta is reduce-normalized. Equations

  • Tau.BookII.Enrichment.two_cat_unit_check bound db = Tau.BookII.Enrichment.two_cat_unit_check.go bound db 2 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookII.Enrichment.two_cat_unit_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.two_cat_unit_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.two_cat_vert_assoc_check

source def Tau.BookII.Enrichment.two_cat_vert_assoc_check (bound db : Denotation.TauIdx) :Bool

[II.D55] Associativity of vertical composition: (eta₃ ∘_v (eta₂ ∘_v eta₁))(x, k) = ((eta₃ ∘_v eta₂) ∘_v eta₁)(x, k). Both sides expand to eta₃(eta₂(eta₁(x, k), k), k). Equations

  • Tau.BookII.Enrichment.two_cat_vert_assoc_check bound db = Tau.BookII.Enrichment.two_cat_vert_assoc_check.go bound db 2 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookII.Enrichment.two_cat_vert_assoc_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.two_cat_vert_assoc_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.two_morph_tower_check

source def Tau.BookII.Enrichment.two_morph_tower_check (bound db : Denotation.TauIdx) :Bool

[II.D56] 2-morphism tower coherence check: A 2-cell eta is tower-coherent if reduce(eta(x, l), k) = eta(reduce(x, k), k) for k <= l. We verify this for the sample 2-cells. Equations

  • Tau.BookII.Enrichment.two_morph_tower_check bound db = Tau.BookII.Enrichment.two_morph_tower_check.go bound db 2 1 1 ((bound + 1) * (db + 1) * (db + 1)) Instances For

Tau.BookII.Enrichment.two_morph_tower_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.two_morph_tower_check.go (bound db : Denotation.TauIdx)

(x k l fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.two_morphism_check

source def Tau.BookII.Enrichment.two_morphism_check (bound db : Denotation.TauIdx) :Bool

[II.D56] 2-morphism mediating check: eta mediates f => g means eta(f(x, k), k) = g(x, k). We verify: two_sq mediates one_id => one_sq. two_sq(one_id(x, k), k) = reduce(reduce(x,k)^2, k) = one_sq(x, k). Equations

  • Tau.BookII.Enrichment.two_morphism_check bound db = Tau.BookII.Enrichment.two_morphism_check.go bound db 2 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookII.Enrichment.two_morphism_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.two_morphism_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.enrichment_iteration_check

source def Tau.BookII.Enrichment.enrichment_iteration_check (db : Denotation.TauIdx) :Bool

[II.P13] Enrichment iteration check: The hom-space between two 1-morphisms is a τ-object. For 1-cells f, g, the 2-cells mediating f => g form a set that is closed under reduce at each stage.

Concretely: the hom-space Hom_2(one_id, one_id) at stage k contains at least the identity 2-cell. We verify that this hom-space is well-defined and nonempty at each stage. Equations

  • Tau.BookII.Enrichment.enrichment_iteration_check db = Tau.BookII.Enrichment.enrichment_iteration_check.go db 1 (db + 1) Instances For

Tau.BookII.Enrichment.enrichment_iteration_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.enrichment_iteration_check.go (db : Denotation.TauIdx)

(k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.enrichment_iteration_check.check_id

source@[irreducible]

def Tau.BookII.Enrichment.enrichment_iteration_check.check_id (k x pk fuel : ℕ) :Bool

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.enrichment_finite_check

source def Tau.BookII.Enrichment.enrichment_finite_check (db : Denotation.TauIdx) :Bool

[II.P13] Enrichment iteration finiteness: At each stage k, the 2-hom-space is finite (bounded by P_k^P_k). This ensures the enrichment ladder is well-founded. We verify: the number of reduce-compatible maps at stage k is at most P_k^P_k, and the primorial tower’s finite stages guarantee finiteness at every enrichment level. Equations

  • Tau.BookII.Enrichment.enrichment_finite_check db = Tau.BookII.Enrichment.enrichment_finite_check.go db 1 (db + 1) Instances For

Tau.BookII.Enrichment.enrichment_finite_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.enrichment_finite_check.go (db : Denotation.TauIdx)

(k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.interchange_check

source def Tau.BookII.Enrichment.interchange_check (bound db : Denotation.TauIdx) :Bool

[II.P13] Interchange law verification: (eta₂ ∘_v eta₁) ∘_h (mu₂ ∘_v mu₁) = (eta₂ ∘_h mu₂) ∘_v (eta₁ ∘_h mu₁).

This is the fundamental coherence condition of a strict 2-category. Both sides expand to eta₂(mu₂(eta₁(mu₁(x, k), k), k), k) when the 2-cells are “strict” (i.e., they compose pointwise via function application).

In our representation: LHS = vert_comp(eta₂, eta₁)(horiz_comp(mu₂, mu₁)(x, k), k) = eta₂(eta₁(mu₂(mu₁(x, k), k), k), k) RHS = vert_comp(horiz_comp(eta₂, mu₂), horiz_comp(eta₁, mu₁))(x, k) = horiz_comp(eta₂, mu₂)(horiz_comp(eta₁, mu₁)(x, k), k) = eta₂(mu₂(eta₁(mu₁(x, k), k), k), k)

These are equal when mu₂ and eta₁ commute in the appropriate sense. For reduce-based cells this holds. Equations

  • Tau.BookII.Enrichment.interchange_check bound db = Tau.BookII.Enrichment.interchange_check.go bound db 2 1 ((bound + 1) * (db + 1)) Instances For

Tau.BookII.Enrichment.interchange_check.go

source@[irreducible]

**def Tau.BookII.Enrichment.interchange_check.go (bound db : Denotation.TauIdx)

(x k fuel : ℕ) :Bool**

Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.full_two_cat_check

source def Tau.BookII.Enrichment.full_two_cat_check (bound db : Denotation.TauIdx) :Bool

[II.D55 + II.D56 + II.P13] Full 2-category verification. Equations

  • One or more equations did not get rendered due to their size. Instances For

Tau.BookII.Enrichment.two_cat_assoc_10_3

source theorem Tau.BookII.Enrichment.two_cat_assoc_10_3 :two_cat_assoc_check 10 3 = true

Tau.BookII.Enrichment.two_cat_unit_10_3

source theorem Tau.BookII.Enrichment.two_cat_unit_10_3 :two_cat_unit_check 10 3 = true

Tau.BookII.Enrichment.two_cat_vert_10_3

source theorem Tau.BookII.Enrichment.two_cat_vert_10_3 :two_cat_vert_assoc_check 10 3 = true

Tau.BookII.Enrichment.two_morph_tower_8_3

source theorem Tau.BookII.Enrichment.two_morph_tower_8_3 :two_morph_tower_check 8 3 = true

Tau.BookII.Enrichment.two_morphism_10_3

source theorem Tau.BookII.Enrichment.two_morphism_10_3 :two_morphism_check 10 3 = true

Tau.BookII.Enrichment.enrich_iter_3

source theorem Tau.BookII.Enrichment.enrich_iter_3 :enrichment_iteration_check 3 = true

Tau.BookII.Enrichment.enrich_finite_5

source theorem Tau.BookII.Enrichment.enrich_finite_5 :enrichment_finite_check 5 = true

Tau.BookII.Enrichment.interchange_10_3

source theorem Tau.BookII.Enrichment.interchange_10_3 :interchange_check 10 3 = true

Tau.BookII.Enrichment.full_two_cat_8_3

source theorem Tau.BookII.Enrichment.full_two_cat_8_3 :full_two_cat_check 8 3 = true

Tau.BookII.Enrichment.horiz_comp_assoc

source **theorem Tau.BookII.Enrichment.horiz_comp_assoc (f g h : TwoCell)

(n k : Denotation.TauIdx) :horiz_comp f (horiz_comp g h) n k = horiz_comp (horiz_comp f g) h n k**

[II.D55] Formal proof: horizontal composition is associative. horiz_comp f (horiz_comp g h) = horiz_comp (horiz_comp f g) h. Both sides are fun n k => f(g(h(n, k), k), k).

Tau.BookII.Enrichment.vert_comp_assoc

source **theorem Tau.BookII.Enrichment.vert_comp_assoc (f g h : TwoCell)

(n k : Denotation.TauIdx) :vert_comp f (vert_comp g h) n k = vert_comp (vert_comp f g) h n k**

[II.D55] Formal proof: vertical composition is associative. vert_comp f (vert_comp g h) = vert_comp (vert_comp f g) h. Both sides are fun n k => f(g(h(n, k), k), k).

Tau.BookII.Enrichment.id_two_cell_tower_coherent

source **theorem Tau.BookII.Enrichment.id_two_cell_tower_coherent (x : Denotation.TauIdx)

{k l : Denotation.TauIdx}

(h : k ≤ l) :Polarity.reduce (id_two_cell x l) k = id_two_cell x k**

[II.D55] Formal proof: the identity 2-cell is tower-coherent. reduce(id_two_cell(x, l), k) = id_two_cell(x, k) for k <= l. This is reduction_compat.

Tau.BookII.Enrichment.two_sq_mediates_at_reduce

source theorem Tau.BookII.Enrichment.two_sq_mediates_at_reduce (x k : Denotation.TauIdx) :two_sq (one_id x k) k = one_sq x k

[II.D56] Formal proof: two_sq mediates one_id => one_sq. two_sq(one_id(x, k), k) = one_sq(x, k). LHS = reduce((reduce(x, k))^2, k), RHS = reduce(x^2, k). i.e., (x % P_k) * (x % P_k) % P_k = x * x % P_k.

Tau.BookII.Enrichment.primorial_pos_check

source theorem Tau.BookII.Enrichment.primorial_pos_check :((List.range 6).all fun (k : ℕ) => decide (Polarity.primorial k > 0)) = true

[II.P13] Formal proof: enrichment iteration is well-founded. The primorial P_k is positive for all k >= 0. Verified computationally for stages 0 through 5.