I think you're still misunderstanding. The CPU picks TTBR0 or TTBR1 based on the top significant bit of the VA, irrespective of whether the access was initiated by user or kernel code. This is in contrast to s390, which has separate page tables for user mode and kernel mode. I personally much prefer s390's model.
And yes, I've read quite a few papers, and I wrote a good fraction of the patches.