bridge

MB2 Bundle identifiability

Lean spine source

Declarations: MB2_bundle_identifiability

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

axiom MB2_bundle_identifiability :
  ∀ A B : System, BundleGradientEquivalent A B → BundleAligned A B

/-- MB3: bearer import. Preserved bearer maps under a substrate translation make
    value-bundle transport more than merely semantic. -/