P22b Semantic ≠ full transport

Declarations: P22b_semantic_not_full_transport

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 P22b_semantic_not_full_transport :
    ∃ t : FinTransportLayers,
      FinSemanticTransport t ∧ ¬ FinFullTransport t :=
  ⟨finTransportSemanticOnly, fin_semantic_only, fin_not_full_transport⟩