1. Introduction
This is a Lean 4 mechanisation of Milner's bigraphs and bigraphical reactive systems (Milner, The Space and Motion of Communicating Agents, 2009; Jensen and Milner, Bigraphs and mobile processes (revised), UCAM-CL-TR-580, 2004), with their behavioural theory, a certified simulator and model checker, and an application. The project began from a design question, a programming language for signers whose structure borrows from the grammar of British Sign Language; the term calculus from that beginning is in the appendix. No part of that design has yet been put to BSL users; by the project's own rule, a design bet that signers have not tested is OPEN. The Lean definitions are the specification: implementation, documentation and test oracles are derived from them.