Depth-one disjoint-type guessing and Kunen's interval-hitting principle

We construct an explicit sequence of disjoint types with depth one and width k + 3 such that every ladder system guessing this sequence yields a witness to Kunen's interval-hitting principle KA: one simply takes every third point of each ladder. The proof labels the countable intervals determined by a club and encodes a gap position and a forbidden label in a colour. Published consistency results for the failure of KA, together with club guessing in the positive direction, then show that bounded-depth disjoint-type guessing is independent of ZFC, relative to its consistency. In particular, the construction gives a consistent negative answer to Question 6.1 of Lambie-Hanson and Uhrik, already for types of constant depth one. Files comprise the article PDF and complete LaTeX source. The manuscript discloses AI-generated mathematical content and its verification limits. A companion Lean 4 development verifies the central combinatorial reduction and internal consequences; external forcing and constructibility results, the cited club-guessing-to-type-guessing theorem, and the fixed-threshold observation in Remark 4.3 are outside this verification claim. Fixed formalization source and scope · Lean 4 verification record