bridge

MB5 Successor audit

Lean spine source

Declarations: MB5_ontology_shift_successor_audit, MB5Crux

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 MB5_ontology_shift_successor_audit :
  ∀ A B : System, FullTransport A B → BearerTransport B → SuccessorSafe A B

/-- MB6a: percolation-evidence-to-basin bridge. Cooperation/percolation
    evidence warrants the abstract basin-stability predicate. -/

def MB5Crux : Prop :=
  ∀ A B : System, FullTransport A B → BearerTransport B → SuccessorSafe A B