diff --git a/boot/uefi/main.c b/boot/uefi/main.c
index 03176ca..616b939 100644
--- a/boot/uefi/main.c
+++ b/boot/uefi/main.c
@@ -41,6 +41,14 @@
 
 // Page tables are built here, exactly where mboot_entry builds them, so the
 // kernel's entry sees the state it was written for.
+//
+// **These are a contract, not this file's choice.** kernel/arch/x86_64/entry.S
+// builds its own bootstrap tables at the same two addresses and loads cr3 with
+// 0x1000 by name. Moving them here alone was tried, on the theory that
+// hardcoded low memory is a poor assumption under UEFI: the machine
+// triple-faulted one instruction after the jump, twice, for two different
+// reasons -- and would have needed the kernel's assembly to agree even once
+// both were fixed. If it ever does move, it moves in both files at once.
 #define PML4_ADDR  0x1000
 #define PDPT_ADDR  0x2000
 
@@ -1751,11 +1759,12 @@ EfiMain(EFI_HANDLE image, EFI_SYSTEM_TABLE *systab)
 
     // ---- no firmware services exist past this line ----
     //
-    // Nothing below can report anything: ConOut is gone, and ui_progress_label
-    // would be drawing into a framebuffer the firmware may no longer own. The
-    // last label on screen is therefore "Leaving the firmware", and a machine
-    // stopped on that one stopped somewhere in the handful of instructions
-    // between here and the kernel's first.
+    // ConOut is gone, but the *framebuffer* is not: it is memory, the firmware
+    // has stopped using it, and ui_progress_label() is a write to it and
+    // nothing more. That distinction is worth making rather than assuming --
+    // an earlier version of this comment claimed nothing could report from
+    // here, and that claim cost a round trip to a laptop and back to learn
+    // which of three steps a machine had stopped in.
 
     __asm__ volatile("cli");
 
@@ -1776,6 +1785,8 @@ EfiMain(EFI_HANDLE image, EFI_SYSTEM_TABLE *systab)
     for (int i = 0; i < 4; i++)                  // 4 GB in 1 GB pages
         pdpt[i] = ((UINT64)i << 30) | PTE_P | PTE_PS | PTE_W;
 
+    ui_progress_label("Starting the kernel");
+
     // RBX carries the framebuffer address into kmain, and must never be 1 --
     // that value marks an application processor in entry64high. A physical
     // MMIO address or zero, so it cannot collide.