bridge

MB3 Bearer import

Lean spine source

Declarations: MB3_bearer_import, MB3Crux

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.

axiom MB3_bearer_import :
  ∀ A B : System, BundleTransport A → SameBearerMap A B → BearerTransport B

/-- **MB4** (correction integrity). Correction-channel integrity requires that
    the system's future behaviour tracks the correction operator — uptake and
    persistence, not merely reference legitimacy (MB4a). -/

def MB3Crux : Prop :=
  ∀ A B : System, BundleTransport A → SameBearerMap A B → BearerTransport B
-- Bearer *admission* (unfamiliar-process → value relevance; ch18
-- `ConservativeExclusion`) is an open sub-obligation of MB3, not part of this
-- transport crux and not a `BridgeAssumptions` field. See `Bundles.lean`.