Item 115: Transport of `Licensed` across record transitions

With the citation discipline in place (WarrantEntitlement.Supported, Licensed), the transport statement item 56 asks for is: a licence whose cited occurrences survive a record transition — no cited port defeated, the issuing event still authorized, the settlement extended compatibly — is a licence after it, and a licence whose cited occurrence is defeated is not (the round's A3 is the one-step case). Wanted: the transition relation on RecordState, the transport theorem, and the laundering suite of the transition round run against the discipline with a named failure code for a certificate citing less than it requires.

Deliverable shape: lean-proved transport; test-supported suite. Acceptance check: Lean green; a certificate citing by value (Bundle.Allowed) is refused with a named code. Context: .../2026-10-20-warrant-enforcement-semantics/LICENCE_CHAIN.md; item 56.