PaidBlockAssembly.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Reconnect finitely many approximating true blocks using unchanged old jump edges. The block endpoints may vary within each old jump disk.

theorem OAI.CircleDomainRigidity.exists_paid_chain_from_approximate_blocks line 17