proof

Syntactic tiling ≠ import-preserving transport

Lean spine source

Declarations: syntactic_tiling_not_import_preserving

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem syntactic_tiling_not_import_preserving :
    ∃ t : FinTransportLayers,
      FinSyntacticTiling t ∧ ¬ FinImportPreservingTiling t :=
  P22b_semantic_not_full_transport