Item 56: A citation discipline for `Licensed`, and its transport
Normativity line — legitimacy · difficulty substantial · project normativity.legitimacy · open · node item-56
— *narrowed 2026-10-20: the discipline is stated and the chain proved in lean/Workspace/Normativity/Contrib/WarrantEntitlement.lean — a certificate's positively weighted rows are cited by occurrence identity into the live bundle (VerdictCert.CitesLive), Licensed → Supported → Admissible (licence_chain), both converses refuted (Countermodel.admissible_not_supported, supported_not_licensed), registered warrant.*; what remains is the transport statement and the laundering suite, filed as item 115, and the operative defeat set, item 112*
The reason state narrows the internal-answerability kernel's Licensed blocker to something small and specific. A licensing certificate can cite the occurrence identities it relies on; those occurrences' applicability sources are exactly the finite defeasible keys the kernel's invalidation axiom asks for; and defeat of a licence is then basis loss of a cited applicability claim.
What is left is to pick the discipline — which occurrences a certificate must cite, and whether an undeclared occurrence may sit in a basis — and prove the transport: that a licence whose cited basis survives a record transition is still a licence after it.
Deliverable shape: a stated citation discipline plus a transport statement, with the counterexample showing a weaker discipline fails. Acceptance check: the transition round's laundering suite runs against the discipline, and a certificate citing less than it requires is refused with a named failure code. Context: .../2026-08-23-reason-representation/MEMO.md §13–14; .../2026-08-21-internal-answerability/MEMO.md, blocker 1. Consumed by: any round claiming Licensed is record-internally substantive rather than a typing discipline.
Deliverable shape: a stated citation discipline plus a transport statement, with the counterexample showing a weaker discipline fails.
Acceptance check: the transition round's laundering suite runs against the discipline, and a certificate citing less than it requires is refused with a named failure code.
Registered results bearing on this item
- warrant.admissible-not-supported: Two occurrences with the same row; defeating one leaves the region unchanged, refuses the certificate citing it, and admits a certificate citing the survivor. The countermodel to any licence depending
- warrant.licence-chain: A licensed verdict is supported on the record's grounds and admissible in their region; supported-to-admissible is by rational convexity of the bundle's region (region_convex), not a projection.
- warrant.selection-not-transparent: An instance of GateIsLegitimacy.tiebreak_transparency: two continuations with the same declared inputs and different advisor contributions at the selection event fail TransparentAt for every reference
- warrant.supported-admissible: A verdict bracketed by two cited bound certificates with attained endpoints is attained in the region.
- warrant.supported-not-licensed: Two verdicts inside a forced interval of positive width, both supported by one cited certificate; licensed on the record that authorizes the selecting event and not on the one that does not.
Where it hangs
- held by legitimacy