10. The pricing
This page proves the pricing: for a law with connected support, the setup, the ledger, the race, the cap and the mismatch
payment combine linearly into T(p)\le C\tau(p) with C=\max\{C_M,C_B\} (Lemma M5.1), and at the parameters
(a,u,\beta,\gamma)=(211/45,3941/20000,23/250,7/60) the stated constant 13999/2000
dominates both coefficients (Lemma M5.4). Both conclusions are for laws with connected support only. This is the assembly
itself: Lemma M5.4 is the Lean theorem NaturalLatents.General.T_le_of_connected (NaturalLatents/General/Pricing.lean),
step 8 of the route. Notation follows section 0 of the contact page.