Item 124: Certified bounds at the displayed price: the licence–force bridge

A licence certifies a bracket on a coordinate by rows of the compiled bundle; the enforcer holds those rows at a tolerance. What does the licence entitle one to say about the displayed price? Answer: a certificate's multiplier sum is the Lipschitz constant of its bound in the rows' excesses (WarrantForce.FunctionalCert.le_of_excess), so a verdict supported on the day's bundle has its bracket at the displayed price widened by mass · tol on each side (bracket_at_market), and any functional certificate cited into the bundle holds there within mass · tol (functional_at_market). This is the only conversion from the force layer's rowwise guarantee to a coordinate bound that the repository has; it is what the adapter reads.

Deliverable shape: lean-proved, landed. Acceptance check: the Lean audit clean. Context: projects/normativity/rounds/2026-10-22-normative-inductor-integration/THEOREM_STORY.md §C.