SPTM: MTE SK tag-page check is a PA-range gate; alias mapping does not bypass it

docs/SPTM-MIE-27.2.md

@@ -98,6 +98,25 @@ The dangling-tag check is a real state machine: a previous tag-storage mapping
 attempt can leave a reference that SPTM detects later. It exists in both builds,
 so it is not a 27.2 fix; it is an audit target.
 
+### MTE check semantics (27.2, `0xfffffff0270d7028`)
+
+The 210-instruction function is a PA-range gate, not a tag-value check:
+
+```
+x19 = page PA
+if (x19 - [0xfffffff0270ae218] < ([0xfffffff0270ae220] - [0xfffffff0270ae218])) {
+    ... state bit test ...
+    if (state bit) panic("%s: MTE tag page containing SK tags is mapped %#lx", x19)
+}
+```
+
+The comparison is on the physical address. An alias that maps the same physical tag
+page at a different virtual address does not move the PA, so it does not avoid the
+check. A bypass would need to make SPTM see a different PA for the same tag memory
+(a page-table/IOMMU bug), or to corrupt the range globals / state bit — none of
+which is present in the 27.2 diff. This is why the MTE line remains a hypothesis,
+not a finding.
+
 ## Why Titan does not transfer
 
 Titan (iOS 16.1–17.4b3, A14–A17) is not an SPTM logic bug. It uses: