Item 128: Admission from the accounted state

WarrantInductor.Entitlement O G Expresses types the admission of a warrant occurrence to the market as four conditions on its origin in the accounted obligation state. Two of them are the protocol's and the application's and are not derived: Protocol.Admitted, which the fixture's trivial protocol makes True, and Expresses, which the fixture makes total. Wanted: (a) a nontrivial protocol whose Admitted and Expresses carry content, with an entitlement at it — the first fixture in which entitlement can fail for a reason other than a dead account; (b) the relation between the record's authorized set (verdict licensing) and the account's receipts, which the construction keeps apart and does not relate; (c) whether entitlement should follow an open Integrity segment rather than one accounted state, so that a warrant's standing is a property of the evolution that incurred its obligation.

Deliverable shape: lean-proved; the protocol and its entitlement as a fixture; a theorem relating authorized to the account, or a stated reason none should exist. Acceptance check: the Lean audit clean; WarrantInductorWitness.entitlement and answered_not_entitled recovered. Context: .../2026-10-22-normative-inductor-integration/HANDOFFS.md (the first arrow); OpenIntegrityEvolution.ObligationState; wiki/Legitimacy.md. Consumed by: the legitimacy ↔ warrant handoff; item 115.