Empirical Foundations of Pat: Transformer OOD Observations, Structural Laws, and Machine-Checked Continuum Theorems

We record the empirical route by which the Pat framework is grounded: starting from controlled transformer training observations, extracting structural laws, and ending in machine-checked theorems. The starting observation is a two-pole out-of-distribution (OOD) dichotomy, reproduced in 45 training runs: a low-epoch transformer reaches training accuracy 1.000 on successor-notation arithmetic, yet OOD accuracy is 32/32 on length extrapolation in the trained notation and 0/32 on the same structure written in an untrained notation of the same basepoint; adding explicit equivalence statements bridges the two notations (0/32 -> 32/32). From this and supporting experiments we extract five structural laws (anchor binding, notation translatability, shift invariance, structure-bearing representation, definition-layer invisibility). The laws map, as an observational correspondence, to the Pat framework's paired-direction declaration, phase-relation locking, and phase-magnitude interlock. The framework chain is formalized in Lean 4 / mathlib: twenty-two theorems with zero errors and zero sorry, from the interlock matrix (determinant theta*(r + 1/r) != 0) through the four-phase interlock, the countable pat grid, and the density theorem, to the continuum closure theorems. The honest boundary is stated exactly: the empirical-to-framework mapping is an observational correspondence, not a deductive implication, and the training results are reproducible from the artifact (one command, Python + PyTorch).