REVIEW 4 major objections 5 minor 11 references
A combinatorial characterization of Kim's lemma for pairs of bi-invariant types
T0 review · 4 major / 5 minor · reviewed 2026-08-06 · deepseek-v4-flash
Pith's one-line read A single weave configuration pinpoints when Kim’s lemma fails.
desk verdict A serious, genuinely new characterization of Kim's lemma failures via (k,1,1)-weaves, but the strongest version rests on an unpublished companion paper and omitted 'mutatis mutandis' proofs. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The central object is the (k,1,1)-weave of depth ω: a family of parameter tuples indexed by the full binary tree of height ω, with each node labelled by a pair from {0,1}², such that any finite up-1-comb (two branches splitting vertically) is k-inconsistent while any finite right-1-comb (two branches splitting horizontally) is consistent. The argument is carried by two mechanisms: an inductive cloning construction that turns a Morley sequence in a bi-invariant type into the vertical or horizontal consistency pattern of a weave, and a forcing-plus-compactness framework that builds a generic filter on dense subsets of an unbounded weave model, producing heir-coheir types whose dividing behaviour is read off from the weave combinatorics.
What would settle it
Construct a complete theory T and k < ω that has a (k,1,1)-weave of depth ω yet still satisfies (k, bi-invariant, bi-invariant)-Kim’s lemma; or exhibit an invariance base A and a type over A admitting no semi-reliably invariant extension, disproving the imported existence result that carries the ‘semi-reliably invariant’ version.
Extended reading notes
Core claim
The main theorem states an exact equivalence: a theory T has a (k,1,1)-weave of depth ω if and only if T fails (k, bi-invariant or semi-reliably invariant, bi-invariant or semi-reliably invariant)-Kim’s lemma, if and only if it fails (k, bi-invariant, bi-invariant)-Kim’s lemma, if and only if it fails (k, heir-coheir, heir-coheir)-Kim’s lemma over models. Here a formula k-divides along a type when some Morley sequence of that type makes any k of its instances jointly inconsistent. The forward direction converts the failure of Kim’s lemma into a weave by building Morley sequences along the two types and cloning them into a tree of parameters; the reverse direction uses a forcing-plus-compactness construction to turn a weave into two heir-coheirs that separate dividing from non-dividing. This gives, for the first time, a combinatorial object equivalent to the failure of a pair-of-invariant-types form of Kim’s lemma rather than merely a consequence of it.
Load-bearing premise
The whole equivalence leans on a companion result asserting that any type over an invariance base extends to a semi-reliably invariant type and any type over a model extends to a semi-reliable coheir; if that external existence result fails, the semi-reliably invariant clause in the main equivalence is unsupported and the characterization may reduce to ordinary bi-invariant types.
Editorial extensions
If this is right
- The class of theories with no (k,1,1)-weave of depth ω is now a genuine dividing line, characterized by a positive Kim’s-lemma property for bi-invariant and heir-coheir types.
- Over arbitrary invariance bases, version (1) of the main theorem gives a non-vacuous Kim’s lemma statement, removing the need to pass to models.
- In theories with no weaves, if a formula implies a finite disjunction where each disjunct divides along a bi-invariant or semi-reliably invariant type, then the formula itself divides along a reliably invariant type (Corollary 3.12).
- For k=2, failure of (2, bi-invariant or semi-reliably invariant, strongly bi-invariant)-Kim’s lemma implies that the theory admits arbitrary cograph consistency-inconsistency patterns, giving a clean graph-theoretic witness.
- An infinite k-grid implies failures of (k, coheir, strong heir-coheir)-Kim’s lemma over models and, assuming GCH, a failure of generic stationary local character.
Reading between the lines
- Because the proof is uniform in k, it leaves open whether existence of a (k,1,1)-weave for one k collapses the hierarchy across all k; if true, the family of Kim’s-lemma variants would be a single k-independent dividing line.
- The cograph characterization for k=2 suggests that the no-weave condition might be connected to the random-graph consistency-inconsistency pattern and hence to NPM(2), a relationship the paper leaves as questions rather than theorems.
- The GCH assumption in the grid-to-stationary-local-character step is likely removable or replaceable by a weaker cardinal hypothesis, since the construction itself is purely combinatorial and the set-theoretic assumption is used only to make a chain of elementary submodels cover the saturated model.
- A concrete testable extension would be to check whether a known theory, such as the triangle-free random graph, admits (k,1,1)-weaves of depth ω; the paper’s final example shows that even definable-type Kim’s lemma failures can coexist with no such weave in that setting.
Formalized claims in Lean
-
Claim #1: For bi-invariant types, Kim's lemma fails exactly when a (k,1,1)-weave of depth ω exists.
/-- @claim 1 For bi-invariant types, Kim's lemma fails exactly when a (k,1,1)-weave of depth ω exists. -/ def claim_weave_characterizes_kim_failure : Prop :=
-
Claim #2: The cloning construction turns any Morley sequence in a bi-invariant type into the consistency patterns of a (k,1,1)-weave.
/-- @claim 2 The cloning construction turns any Morley sequence in a bi-invariant type into the consistency patterns of a (k,1,1)-weave. -/ def claim_cloning_produces_weave_patterns : Prop :=
-
Claim #3: The forcing-plus-compactness framework builds a generic filter on dense subsets of an unbounded weave model, producing heir-coheir types.
/-- @claim 3 The forcing-plus-compactness framework builds a generic filter on dense subsets of an unbounded weave model, producing heir-coheir types. -/ def claim_forcing_builds_heir_coheir : Prop :=
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper introduces two families of combinatorial consistency-inconsistency configurations, (k,m,n)-weaves and k-grids, and proves implications between these configurations and failures of several variants of Kim's lemma for invariant types. The main result, Theorem 3.10, asserts that for a complete theory T and k<ω the absence of a (k,1,1)-weave of depth ω is equivalent to (k, bi-invariant or semi-reliably invariant, bi-invariant or semi-reliably invariant)-Kim's lemma, to (k, bi-invariant, bi-invariant)-Kim's lemma, and to (k, heir-coheir, heir-coheir)-Kim's lemma over models. The forward direction is proved via an induction building weaves from a failure of Kim's lemma (Theorem 2.6), and the converse uses a forcing-plus-compactness construction (Proposition 3.9). The paper also shows that arbitrary cograph consistency-inconsistency patterns are equivalent to certain weaves, that infinite k-grids entail failures of Kim's lemma variants and, under GCH, failure of generic stationary local character, and that the triangle-free random graph satisfies none of the relevant stronger statements.
Significance. If the central equivalence is correct, it gives the first combinatorial configuration known to be equivalent to a Kim's lemma statement for pairs of bi-invariant types, and the use of semi-reliably invariant types is a genuine attempt to make the statement non-vacuous over arbitrary invariance bases. The weave and grid definitions are independent, parameter-free objects, and the main equivalence is not true by definition but is proved in a genuine cycle of implications. The cograph characterization in Section 4 and the k-grid consequences in Section 5 are elegant and will likely be of independent interest to model theorists working on NTP2/NSOP1-type dividing lines. However, the manuscript depends heavily on the author's unpublished preprint [7] and on several proof steps that are omitted or only sketched, so the advertised results are not yet fully verified in the text.
major comments (4)
- [Section 2, Theorem 2.6(3)-(4)] The proofs of parts (3) and (4) are dismissed with 'mutatis mutandis' after part (2). These cases are load-bearing for Theorem 3.10(1), because the 'bi-invariant or semi-reliably invariant' disjunction in condition (1) requires the semi-reliably invariant class on the left-hand side and on both sides, not only on the right-hand side as proved in (2). The semi-reliable extension machinery is delicate: it requires the constructed type q_d to restrict to q on each coordinate and the relevant two-tuples to be invariant sequences. Please write out the inductions for parts (3) and (4) explicitly.
- [Section 1, Lemma 1.8] The claimed canonical identification of W with a subset of (2^2)^L is impossible as stated: W is the sort for (2^2)^≤L, and elements of W_<L are partial functions of finite height, so the map iota(a) = (i mapsto eval(a,i)) is not a total function on L. This lemma is used in Proposition 1.11 to pass from finite-depth weaves to depth ω. The statement should be reformulated for Wtop (or the evaluation function should be extended in a definable way), and the asserted first-order definability of the comb predicates and the axiomatizability of partial weaves should be proved rather than asserted with 'it is not difficult to show'.
- [Definition 2.3 and Fact 2.4] The advertised non-triviality of Theorem 3.10(1) over arbitrary invariance bases depends on Fact 2.4, quoted as [7, Thm. 2.14], which asserts that every type over an invariance base extends to a semi-reliably invariant type and every type over a model extends to a semi-reliable coheir. Since [7] is an unpublished preprint and no proof is included in the present paper, the reader cannot verify this dependence. If Fact 2.4 fails, the 'semi-reliably invariant' disjunct in Theorem 3.10(1) may be spurious. Please include a proof of Fact 2.4 or state Theorem 3.10 conditionally on it.
- [Section 3, Proposition 3.9, final paragraph] The final step asserts that the displayed up-1-comb statements imply that φ(x,y) k-divides along p(y). This is not immediate, because the Morley sequence (b_i) is generated by p, a coheir coming from the ultrafilter UR, while the displayed up-comb statements involve elements of U, which belong to the UU-side. In particular, when m=0 the displayed set reduces to the b_i's themselves, and the text does not spell out why those form an up-1-comb. Please give the explicit finite-inconsistency and compactness argument justifying the conclusion.
minor comments (5)
- [Proposition 2.2] The proof has a typographical swap: it says 'φ(x,b) k-divides along q' and 'since (A,q)∈X', but the hypothesis is (A,p)∈X and (A,q)∈Y, and the assumption should be that φ(x,b) k-divides along p. Please correct this.
- [Theorem 2.6, proof of (1)] Near the end, the text says 'an up-n-comb in (2^2)^{d+1}' but the property being verified is (U), which concerns up-m-combs. This is a typo and should be fixed.
- [Definition 2.3] The definition of 'semi-reliably in I' refers to the largest class R satisfying a certain closure property; the existence of such a largest class is not justified. Since the property is preserved under unions of chains, the fix is routine, but it should be stated.
- [Definition 1.1] The phrase 'common first-order theory of ordinals' is not a definition. The properties needed later (least element, successor of every non-maximal element, and initial segments) should be made explicit.
- [Proposition 3.9] The notation (1)_N and (2)_{N,ψ} for the sets of morphisms collides with the numbered item labels in the same sentence; please use a more distinctive notation.
Circularity Check
No circularity: Theorem 3.10 is a genuine equivalence cycle over independently defined weaves; reliance on the author's earlier [7] is auxiliary, not definitional.
full rationale
No circular steps are present. The central theorem (3.10) is proved by a genuine cycle of implications: (1)=>(2) and (2)=>(3) are inclusions of type classes (bi-invariant types are contained in 'bi-invariant or semi-reliably invariant', and heir-coheirs are bi-invariant) via the monotonicity Proposition 2.2; (4)=>(1) uses Corollary 2.7, whose proof reduces to the four cases of Theorem 2.6; and (3)=>(4) uses Proposition 3.9, which constructs heir-coheirs from a weave by the forcing-plus-compactness argument. The weave and grid configurations (Definitions 1.4 and 5.2) are defined independently of the Kim-lemma statements, and no parameter is fitted to data, so the equivalences are not true by construction. The semi-reliably invariant extension property used in Theorem 2.6 is applied directly from Definition 2.3, not imported as the conclusion of the theorem. The paper does lean on the author's earlier preprint [7] for Fact 2.4 (existence of semi-reliably invariant types over invariance bases) and for proof templates; this is self-citation, but it is not a circular derivation because [7]'s theorem has its own stated assumptions and does not include the target equivalence. If Fact 2.4 or the 'mutatis mutandis' proofs of Theorem 2.6(3)-(4) were to fail, the advertised non-vacuity over arbitrary invariance bases would be weakened, but the bi-invariant-only characterization in Theorem 3.10(2) and the main equivalence cycle would remain intact. Those are verification risks, not circularity.
Assumptions & free parameters
assumptions (5)
- standard math Standard first-order model theory framework: monster model, compactness, saturation, Morley sequences.
- domain assumption Fact 2.4 ([7, Thm. 2.14]): every type over an invariance base extends to a semi-reliably A-invariant type, and every type over a model extends to a semi-reliable M-coheir.
- domain assumption GCH for Theorem 5.10(5).
- standard math Cographs are exactly finite P4-free graphs ([6, Thm. 2]).
- domain assumption Results from [7]: Prop 1.5/3.1 template for forcing-plus-compactness; Prop 1.7 for ATP equivalence.
invented entities (3)
-
(k,m,n)-weave of depth L
-
k-grid indexed by L
-
augmented (k,1,1)-weave model
Cite this review
Pith. "Pith review of A combinatorial characterization of Kim's lemma for pairs of bi-invariant types." pith.science (2026). https://pith.science/paper/GCQTTUQX
@misc{pith2026250721366,
author = {Pith},
title = {Pith review of: A combinatorial characterization of Kim's lemma for pairs of bi-invariant types},
year = {2026},
howpublished = {\url{https://pith.science/paper/GCQTTUQX}},
note = {Machine review of arXiv:2507.21366}
}
abstract
We give a combinatorial consistency-inconsistency configuration that is equivalent to the failure of the following form of Kim's lemma for a given $k$: $(\star)$ For any set of parameters $A$, formula $\varphi(x,b)$, and $A$-bi-invariant types $p$ and $q$ extending $\mathrm{tp}(b/A)$, if $\varphi(x,b)$ $k$-divides along $p$, then it divides along $q$. We then give an equivalent technical variant of $(\star)$ that is non-trivial over arbitrary invariance bases. We also show that the failure of weaker versions of $(\star)$ entails the existence of stronger combinatorial configurations, the strongest of which can be phrased in terms of families of parameters indexed by arbitrary cographs (i.e., $P_4$-free graphs). Finally, we show that if there is an array $(b_{i,j} : i,j < \omega)$ of parameters such that $\{\varphi(x,b_{i,j}) : (i,j) \in C\}$ is consistent whenever $C \subseteq \omega^2$ is a chain (in the product partial order) and $k$-inconsistent whenever $C$ is an antichain, then there is a model $M$, parameter $b$, and $M$-coheirs $p,q \supset \mathrm{tp}(b/M)$ such that $q^{\otimes \omega}$ is an $M$-heir-coheir and $\varphi(x,b)$ $k$-divides along $p$ but does not divide along $q$. In doing so, we also show that this configuration entails the failure of generic stationary local character under the assumption of $\mathsf{GCH}$.
Figures
Figures from the paper (5 more)
Reference graph
Works this paper leans on
-
[7]
James E. Hanson. Bi-invariant types, reliably invariant types, and the comb tree property. arXiv e-prints , page arXiv:2306.08239, June 2023
work page Pith review arXiv 2023
-
[1]
SOP 1, SOP2, and antichain tree property
JinHoo Ahn and Joonhee Kim. SOP 1, SOP2, and antichain tree property. Annals of Pure and Applied Logic , 175(3):103402, March 2024
work page 2024
-
[2]
On the antichain tree property
JinHoo Ahn, Joonhee Kim, and Junguk Lee. On the antichain tree property. Journal of Mathematical Logic , 23(02), December 2022
work page 2022
-
[3]
A Walk on the Wild Side: Notions of maximality in first-order theories
Michele Bailetti. A Walk on the Wild Side: Notions of maximality in first-order theories. arXiv e-prints , page arXiv:2409.19236, September 2024
arXiv 2024
-
[4]
Remarks on generic stability in independent theories
Gabriel Conant and Kyle Gannon. Remarks on generic stability in independent theories. Annals of Pure and Applied Logic , 171(2):102736, February 2020
work page 2020
-
[5]
Gabriel Conant, Kyle Gannon, and James Hanson. Keisler measures in the wild. Model Theory, 2(1):1–67, June 2023
work page 2023
-
[6]
D. G. Corneil, H. Lerchs, and L. Stewart Burlingham. Complement reducible graphs. Discrete Applied Mathematics , 3(3):163–174, July 1981
work page 1981
-
[8]
Generic stability independence and treeless theories.Forum of Mathematics, Sigma, 12, 2024
Itay Kaplan, Nicholas Ramsey, and Pierre Simon. Generic stability independence and treeless theories.Forum of Mathematics, Sigma, 12, 2024
work page 2024
Show all 11 references
-
[9]
Some Remarks on Kim-dividing in NATP Theories
Joonhee Kim and Hyoyoon Lee. Some Remarks on Kim-dividing in NATP Theories. arXiv e-prints , page arXiv:2211.04213, November 2022
2022
-
[10]
A New Kim’s Lemma
Alex Kruckman and Nicholas Ramsey. A New Kim’s Lemma. Model Theory, 3(3):825–860, Aug 2024
2024
-
[11]
On NSOP 2 Theories
Scott Mutchnik. On NSOP 2 Theories. arXiv e-prints , page arXiv:2206.08512, June 2022. Department of Mathematics, Iowa State University, 396 Carver Hall, 411 Morrill Road, Ames, IA 50011, USA Email address : jameseh@iastate.edu 25
2022 arXiv
Reviewed August 6, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.