Bridge Assumptions

The framework names the empirical and philosophical handoffs it needs instead of hiding them inside definitions.

What decision changes?

When reading a claim, ask whether it is a proof step, a counterexample, or a bridge to real systems.

The book does not try to make every hard problem disappear by definition. It names the handoffs.

A bridge assumption is a place where the argument needs the world to cooperate. For example: that boundary discovery can identify the operative controller, that value-bundle measurements track something real enough, that correction channels can be measured, or that successor checks preserve what matters.

In the formal spine, these are the MB1 to MB10 bridges. Lean can check that certain conclusions follow if the bridges hold. It does not prove that real systems satisfy the bridges. Each bridge maps to a canonical open problem the wider alignment field already argues about — see the ten cards linked in the side panel for the field crux, the Lean axiom, and what the experiment suite has (and has not) shown about it.

This distinction is useful because it marks where the open work lives and where confidence should be lower, instead of folding both into one confident-sounding claim.

What would count as evidence?

A bridge becomes stronger when a measurement procedure, governance mechanism, or field result makes the handoff reliable in a narrow deployment class.