Compact Quasi-Metric Spaces Are Expand-Contract Plastic

On a totally bounded metric space, every non-contractive self-map is an isometry (Freudenthal–Hurewicz; Naimpally–Piotrowski–Wingler). For quasi-metric spaces, taken T1 throughout, this fails: Zavarzina gave a hereditarily precompact counterexample (Carpathian Math. Publ. 15(2), 2023), and the toll spiral (doi:10.5281/zenodo.22801325) shows that bijectivity does not restore rigidity. This paper shows that compactness does, with no precompactness hypothesis: every compact, or countably compact, quasi-metric space is expand-contract plastic, as is every quasi-metric space whose conjugate topology is compact. Under hereditary precompactness, upper limits of left K-Cauchy sequences, and the R0 axiom, every non-contractive self-map, bijective or not, is an isometry; in particular in hereditarily precompact, sequentially Yoneda complete quasi-metric spaces. When both topologies are compact, the statement reduces to the symmetrized case, which falls under Zavarzina's two-sided theorem; the one-sided theorems do not. No hypothesis can be dropped: a three-layer toll space with a fee vanishing toward the deep end (T0, Yoneda complete, compact in both topologies, with a left K-Cauchy subsequence in every sequence, carrying a bijective non-contractive non-isometry) shows the R0 axiom cannot; one distance on the natural numbers and its conjugate settle bijectivity and the two sequential hypotheses; the toll spiral settles compactness. Plasticity does not pass to the symmetrization, even for compact spaces: with Proposition 5.1 of Agyingi (arXiv:2610.10077v1), this shows that plasticity of a quasi-metric and of its symmetrization are independent (compare his Problem 5.4). The paper answers Questions 7.1 and 7.5 of the toll-spiral paper. Machine verification: the two rigidity theorems and the counterexamples are verified in Lean 4 over mathlib (pins in lean-toolchain, lakefile.toml, lake-manifest.json), in six modules, sorry-free. The statements not mechanized are listed in the paper's Data availability section; most concern the passage from sequential to topological compactness. The build prints sixty-three #print axioms lines, each depending only on axioms among propext, Classical.choice and Quot.sound. SHA-256 of ArtifactHashes.txt (the manifest of the six modules and the three pins, as printed in the paper's Data availability): e2942f65114e6ca497ff154e78c7f827527792788f2b966ba47732ad4836cccb Verify integrity with sha256sum -c SHA256SUMS (macOS: shasum -a 256 -c SHA256SUMS), which covers the other thirteen files. Build with lake exe cache get && lake build (requires elan). See README.md in this record. 2020 MSC: 54E35 (primary); 54D30, 54E40, 54E50, 54E15, 68V20.