2026-10-20-warrant-enforcement-semantics

Prompt — what entitles a market to enforce a warrant (2026-10-20)

You are working in the alignment-workspace repository, on main after the merge of PR #128. Do not stack this round on an unmerged branch. One unmerged branch is a source for this round (Part 0); it is not a base.

The round directory is projects/normativity/rounds/2026-10-20-warrant-enforcement-semantics/. The prompt goes verbatim in prompts/2026-10-20-warrant-enforcement-semantics/PROMPT.md. New priority items start at 112.

What this round is for

Item 39 asks whether normative statics produce a credal constraint or only a price demand, and says in its own text that producing the region is half the item: the source must also supply a certificate that cumulative enforcement liability over the assessed worlds is bounded. The geometric half now exists (a warrant compiles to rows; rows force a region). The liability half has never been attempted for a genuinely normative row. This round attempts it, as a fork over what the enforced security settles against, and reports which readings of "a reason" the market can afford. The deliverable is a finding, not a design.

Be skeptical. The three semantics below and the licence chain were worked out in conversation and checked on no example. Treat each as a conjecture. A part that fails ships its exact obstruction with a fixture.

Every declaration named below was read from main at #128 or from the named branch. Confirm each exists before relying on it, and correct this prompt in the report where it is wrong.

Maintainer rulings

Record each as a dated DECISIONS.md entry as the round's first commit. Where the maintainer has struck one, omit it.

M1. [MAINTAINER: confirm, amend, or strike.] Normative content enters the market in two forms: obligations as credal constraints on priced sentences; values as securities traded directly. (Stated in conversation on 2026-08-23; not in DECISIONS.md. If struck, Part B's semantics (iii) is the only one that survives as a reading of obligations, and the round says so.)

M2. The question of what a warrant's security settles against is not ruled. This round runs it as a fork (Part B) and reports; the maintainer rules on the result.

M3. Nothing in this round redefines legitimacy, the Normative Inductor architecture, or the force layer. Those are consumed, not revised.

Proposals from the prompt's author

Not ruled on. Where the mathematics supports one, adopt it as agent-decided, reversible, naming the rejected alternative.

P1. Licence is three-level, with no converses. For a verdict v, a certificate c, grounds G and a record R:

• Admissible(v, G): the region compiled from G contains v;
• Supported(v, c, G): c certifies v from admitted grounds — its positive multipliers name occurrences in G;
• Licensed(v, c, R): every occurrence c cites is live in R at the step, and the event that issued and selected c is itself an authorized record event.

Conjecture: Licensed ⇒ Supported ⇒ Admissible, and both converses fail. The compiler decides the first two; the record decides the third. This is the shape proposed for item 56; this round proves the chain and the two countermodels and files the rest of 56 against it.

P2. The conclusion of enforcement is defect, not membership. What affordable enforcement delivers is a bounded public defect d_s = dist_∞(b_s, K_s) at a declared tolerance, never P_t ∈ K_t. State every result in that form.

P3. The record of a market run is an additional object. Price history is not reason history. Part C defines the minimum such object and shows it is neither over-rich nor under-rich in the sense of ReasonMediatedAuthorship.

P4. Names, provisional: settlement semantics for the fork's parameter; bankroll schedule for the constructed B; entitlement for "the row may be enforced at bounded liability".

Part 0 — port the seed statics (bounded)

Branch round/2026-09-16-seed-statics holds lean/Workspace/Normativity/Contrib/SeedStatics.lean, 96 commits behind main. Port onto this round's branch the declarations this round consumes — Form, Form.row, Settlement, SubItem, StrItem, Seed, DocketState, forcedBundle, forcedRegion, IsForcedInterval, BoundCert, defeat_widens — against current main (Bundle.Region and FarkasCert in NormativeInductorComposition.lean are the targets they compile to). Do not merge the branch; do not port the convergence branch; do not port the fixtures or the criterion material. If the port does not build within a bounded effort, port only Form/Form.row/BoundCert and file the rest as an item. Say in the report what was ported and what was left.

Part A — the warrant as a provenance-carrying market object

A1. The typed warrant. A warrant occurrence is a Form together with: an occurrence identity; the applicability claim it cites (an occurrence, or a settled sentence); a source (a party or a settlement event); and a defeat condition (which occurrences, if live, undercut it). The three forms stay as on the branch: premise X c, applicability X XA c, strength XA XAY c, each compiling by Form.row.

A2. The chain. Lean. State Admissible, Supported, Licensed per P1, with Supported carried by a BoundCert whose positive-multiplier rows are indexed by occurrences. Prove Licensed → Supported → Admissible.

**A3. Countermodel to Admissible → Supported, and to transport.** Two occurrences r₁, r₂, distinct, each independently supporting the same bound on φ. A certificate citing r₁. Defeat r₁; r₂ stays live. Show: the forced region is unchanged; the certificate no longer satisfies Supported; a fresh certificate citing r₂ does. Exact fixture, and Lean if cheap. This is the countermodel to any licence that depends only on the region.

**A4. Countermodel to Supported → Licensed.** A region [a, b] with a < b on φ, two licensed verdicts inside it, and a selection by a non-principal party that lands on one. Admissible and supported; whether it is licensed is a transparency question on the record. Do not re-prove tiebreak_transparency (GateIsLegitimacy); cite it and show the fixture is an instance.

Part B — the fork: what the security settles against

The hypothesis to discharge is liability in conditional_normative_inductor (NormativeInductionInterface.lean): for every n and every live world v, −B ≤ (realizedEnforcer L enforcer).netWorth (history L enforcer) v n. The enforcer is the force layer's compiled position (TRADERIZED_FORCE_INTERFACE.md); the assessment process is Assessment (AssessmentProcess.lean).

The fixture, used throughout B. A fragment of four sentences X, X∧A, X∧A∧Y, Y; one warrant occurrence with strengths c_P, c_A, c_S all strictly between 0 and 1; one defeater of its applicability claim that arrives at a known date n₀; a deductive process that settles X true at some n₁. Exact rationals.

For each of the three settlement semantics, either construct a bankroll schedule B (as a function of the fixture's declared quantities) under which the liability hypothesis holds, or exhibit an efficiently computable trader that drives the enforcer's net worth below every bound. Both outcomes are results.

B(i) — deductive settlement. The rows are admissible in every plausible world (the hypothesis of deductive_end_to_end, DeductiveEffective.lean). Expected: zero liability, and the warrant was a logical fact wearing a strength. Confirm, and state exactly which hypothesis of deductive_end_to_end a genuine warrant fails — that is the boundary of the deductive case.

B(ii) — evaluation settlement. The sentence Y is settled by a later legitimate evaluation: Y's payoff in a live world is that world's evaluation at a declared date, and the evaluation is a typed input of the fixture. Liability is then the enforcer's exposure on the event that the evaluation disagrees with the warrant. Construct B as a function of the declared disagreement mass if one exists; show it is unbounded if the evaluation is unconstrained by the warrant. This is the reading under which enforcement "assumes the normative conclusion" — say precisely whether it does, i.e. whether the only B that works presupposes the evaluation satisfies the row.

B(iii) — pegged, no settlement. Y has no payoff event; the row is held by the enforcer against its own account and the enforcer is settled on nothing. Determine which of the criterion's clauses survive: is the augmented market still a logical inductor relative to Assessment when one trader's securities never settle? If yes, with what B; if no, which clause fails and on which trader.

B(iv) — the defeater. For whichever semantics admit a B, show what happens at n₀ when the applicability claim is undercut: the row leaves the region (defeat_widens), the enforcer's position unwinds, and the liability incurred between the warrant's entry and n₀ is either recovered, absorbed by B, or not — state which, exactly.

B(v) — answer item 39 in its own terms. Strong (a semantic credal constraint C_t with live worlds following) or weak (a price demand K_t only), per semantics. If weak for all three, exhibit the two credal sets with the same projection and different live worlds that the item asks for.

Part C — the record of a market run (bounded)

Define trace : MarketRun → Record where the record carries, per date: warrant occurrences entered (with A1's provenance), certificates issued and selected, docket transitions (entry, defeat, withdrawal), and the enforcer's position. Prices are not in the record. Prove on the Part B fixture that the record is neither injective in the market run (the over-rich end, reasonMediated_of_injOn) nor constant (the under-rich end, reasonMediated_const_iff), and that Licensed from A2 is decidable from the record alone. Stop there: do not attempt authorship, transparency, or the inductor-as- principal question; file what Part C makes visible as items.

What this round is told not to do

• No architecture pass over legitimacy or the Normative Inductor.
• Do not define the baseline B of the thin specification (item 110) — a different B.
• Do not merge or port the convergence branch.
• Do not touch the deference line's Lean except to cite it.
• Do not cite any ruling not in DECISIONS.md; M1 is the only chat-sourced position here and it is marked for the maintainer.
• Do not register any Part B result above test-supported unless the construction is in Lean against conditional_normative_inductor's actual signature.

Lean / formalization target

lean/Workspace/Normativity/Contrib/WarrantEntitlement.lean (name provisional): the ported seed declarations, A1–A2, A3 if cheap, the B constructions that go through, and the Part C record with its two non-vacuity lemmas. Sorry-free, three allowed axioms, nonvacuity witnesses for every structure. #print axioms on every declaration.

Output

In the round directory: REPORT.md; LICENCE_CHAIN.md (Part A); SETTLEMENT_FORK.md (Part B, one section per semantics, with the fixture's numbers); RECORD.md (Part C); COUNTERMODELS.md; src/ with the exact-rational fixture and the trader-exploitation search for any semantics that failed; PROVENANCE.md. Items filed from 112. Candidate registrations listed, not registered, except Lean-proved chain lemmas against item 56.

Final questions the report must answer

1. Under which settlement semantics does a bankroll schedule exist for one defeasible warrant, and as a function of what?
2. Under evaluation settlement, does the only working B presuppose the evaluation satisfies the row? Yes or no, with the construction.
3. Is item 39 strong or weak, per semantics?
4. What does Licensed need from the record that the region cannot supply? State it as the content of item 56.
5. Which of M1's two forms (constraint, security) does each semantics realize, and is there a semantics under which "obligation to respond" is the only coherent reading?
6. What is reserved to the maintainer.

Report — 2026-10-20-warrant-enforcement-semantics

Prompt author	the maintainer (prompts/2026-10-20-warrant-enforcement-semantics/PROMPT.md, verbatim)
Executor	Claude Fable 5.1 (Anthropic), in Claude Code
Lean	lean/Workspace/Normativity/Contrib/WarrantEntitlement.lean (one file, 255 declarations audited, three allowed axioms, no sorry)
Fixture	src/fixture.py, src/licence.py, src/record.py; tests/run.py (37 checks, exact rationals)
Registrations	warrant.* in projects/normativity/CLAIMS.md, the chain lemmas against item 56
Filed	PRIORITIES.md items 112–116; item 56 narrowed
Base	main at the merge of PR #128 (2b7a1453)
Date	2026-10-20

Verdict. ONE-DEFEASIBLE-WARRANT-IS-ENTITLED-AT-THE-ODDS-UNDER-EVERY-SETTLEMENT-SEMANTICS-WHILE-A-SLACK-WORLD-IS-LIVE-THE-FORK-COLLAPSES-IN-THE-ACCOUNT-THE-ORPHANED-STRENGTH-ROW-IS-THE-ONE-UNAFFORDABLE-CASE-ITEM-39-IS-WEAK-AND-THE-LICENCE-CHAIN-HOLDS-WITH-BOTH-CONVERSES-FAILING. The gloss is in README.md.

Depends on 2026-08-16-traderized-enforcement (the force algebra and the enforcement-preservation composition), 2026-09-07-final-pressure-pass (the conditional Normative Inductor theorem), and the unmerged round/2026-09-16-seed-statics as a source (Part 0; not a base, not merged).

Superseded by the rebuttal round (2026-10-21)

The round 2026-10-21-rebuttal-and-end-to-end (projects/normativity/rounds/2026-10-21-rebuttal-and-end-to-end/, shipped in the same pull request) lands the maintainer's repair of this round's one refutation and supersedes three readings below, which are left in place as this round made them:

• **Fixture.disagree_region_empty** is true of the port-only region and is no longer the operative statement: under rebuttal by settlement (settleForm) the strength row leaves at n_E, the region is nonempty (Fixture.rebutted_region_nonempty) and force is not withheld; Fixture.liability_disagree describes a superseded schedule (schedWithheld).
• "The premise row guards the chain" (B(ii), (iv); COUNTERMODELS.md §3) is retracted as a design reading: the guard also emptied the joint region on unrelated warrants when the premise was refuted (Fixture2.old_rule_empty); under M2 a refuted premise retires its occurrence and the other warrants stay enforced (Fixture2.retired_region).
• The orphan pin (orphan_region_nonempty, orphan_no_slack, harmonic_buyer_run) is kept as the countermodel to the port-only rule; under settleForm it cannot form (Fixture.no_strength_after). The bankroll across the rebuttal is 3ρ(2 + ρ), not 3ρ (REBUTTAL.md A2 of that round).

The finding in one paragraph

A warrant with strengths strictly inside (0, 1) excludes live worlds as points of its region — that is what makes it normative rather than logical — and the enforcer that holds it is exposed at exactly those worlds. The round's result is that this exposure is bounded by the odds of the warrant, not by its intensity, its tolerance or how long it is held: the enforcer's assessed net worth at any live world is at least −(1 + 2) · ρ, where 1 is the market maker's constant, 2 the trading firm's budget floor, and ρ dominates, row by row, every live world's deficit by some live world's surplus (netWorth_ge_neg_odds). For the fixture's three rows the least such ρ is max_j c_j/(1 − c_j), the largest odds the warrant states. The argument follows one world across dates (the item-40 shape), where the force interface's own certificate Σ_t (ε_t + C_t) D_t/δ_t maximizes date by date; that is why the one is a constant and the other a sum. The three settlement semantics of the dispatch are three live-set schedules of one assessment process, and the bankroll is the same under all three as long as a slack world is live. When the slack world dies, two things can happen: the region empties and force is withheld (the premise row guards the chain), or — after the applicability port has been defeated — the region stays nonempty with no slack world, the strength row contraposes, and an efficiently computable buyer drives the enforcer's net worth to −∞ on a convergent budget. That last case is the round's one refutation, and it is a fact about per-row defeat and linear strength rows, not about any settlement semantics.

Corrections to the prompt (AGENTS.md §8)

1. GateIsLegitimacy and ReasonMediatedAuthorship are in lean/Workspace/Deference/Contrib/, not under Normativity. They are imported and cited only; the deference line's Lean is untouched.
2. deductive_end_to_end (DeductiveEffective.lean) has no row or region hypothesis: its region is DeductiveRegion.deductiveRegion (DP.D n) (coords n), built from the plausible worlds themselves, so a genuine warrant cannot be stated in it at all. The admissibility hypothesis a warrant fails is hadm of compiled_end_to_end (NormativeInductorComposition.lean) and of Evaluation.deductive_normative_inductor (NormativeInductionInterface.lean): every plausible world's payout lies in the compiled bundle's region. The boundary of the deductive case is that hypothesis (B(i)).
3. B(ii)'s expected outcome — liability unbounded when the evaluation is unconstrained by the warrant — is refuted; the bankroll is independent of the evaluation (B(ii) below).
4. B(iii)'s "the enforcer is settled on nothing" is not expressible in the pinned substrate: a PCWorld assigns every sentence a truth value, so a security that never settles is one both of whose values stay live forever. That is evaluation settlement at n_E = ∞, and the account treats it identically (B(iii)).
5. P1's "the region compiled from G contains v" is read with a verdict as a value for the coordinate (a point in the forced interval), which is what A4's "two verdicts inside [a, b]" requires. Supported then needs two cited bound certificates plus their attained endpoints, and Supported → Admissible is a theorem by rational convexity (region_convex), not a projection.
6. The branch distance "96 commits behind main" is exact (git rev-list --count).

Part 0 — the port

Ported onto this branch, inside WarrantEntitlement.lean, against current main: truth, Settlement (with Pinned, le, empty, pinRowsAt, pinRows, their satisfaction lemmas), settledTerm, specialize, specialize_sat_iff, Form with Form.c, Form.row, premise_sat_iff and two new satisfaction lemmas (applicability_sat_iff, strength_sat_iff), SubItem, StrKind, StrItem, Constitutive, Seed with liveSub/liveStr, DocketState with quiet, Cite, pinCited, forcedBundle, forcedRegion with forcedRegion_iff_check, forcedRegion_iff, forcedRegion_anti, LowerBound, UpperBound, IsForcedInterval with le/unique/mono, widenSeed, defeat_widens, allowed_sat, BoundCert with value, sound and the new sound_of_pos, lowerCert_bound, upperCert_bound. Three small additions the branch did not have: DecidableEq on Form, SubItem, DocketState, Cite (the licence chain's decidability needs them), a Decidable instance for forcedRegion, and BoundCert.sound_of_pos.

Not ported, deliberately: the elimination section (forcedInterval by Fourier–Motzkin), Pins, Refuted, leverage, SureLoss, the Farkas support lemma, confinement, seed-independence, transport, stabilization, humility, and every fixture of the branch. The port compiled on the first build against main's Row/Bundle/FarkasCert API with no change to any ported statement. Cost recorded as item 116: when PR #102 lands, these declarations exist twice in two namespaces and one copy must go.

Part A — the licence chain

LICENCE_CHAIN.md. The typed warrant Occurrence (identity, Form, cited applicability claim, source, defeat set). Verdicts are values. Admissible, Supported (a VerdictCert: lower and upper BoundCerts whose positive-multiplier rows are cited by occurrence into the live bundle, with attained endpoints), Licensed (supported on the record's grounds and the issuing event authorized). licensed_supported, supported_admissible, licence_chain; Supported.valid says a supported certificate's endpoints are valid bounds, so citation is not merely a typing discipline. A3: Countermodel.admissible_not_supported — two occurrences with the same row, the region unchanged by defeating one (region_unchanged), the stale certificate unsupported, the fresh one supported. A4: Countermodel.supported_not_licensed — two verdicts inside [1/2, 1], both supported, one licensed and one not by the record's authorization; selection_not_transparent instantiates GateIsLegitimacy.tiebreak_transparency on the selection event with two parties and two continuations. Registered against item 56 as warrant.licence-chain, warrant.supported-admissible, warrant.admissible-not-supported, warrant.supported-not-licensed, warrant.selection-not-transparent.

Part B — the fork

SETTLEMENT_FORK.md. The enforcer is warrantEnforcer sched : AdaptiveTrader, the force layer's enforcementStrategy on a date-indexed Presentation; the realized enforcer plays exactly it (realizedEnforcer_strat). day_value_eq resolves a day's value at a world into units-weighted signed gaps plus intensity-weighted squared violations. The bankroll theorem netWorth_ge_neg_odds, its liability form liability_of_odds, and the composition warrant_normative_inductor against Evaluation.conditional_normative_inductor's actual signature, with B = 3ρ. The world-inclusive case is netWorth_nonneg_of_inclusive (B = 0). The withheld tail is netWorth_eq_of_tail_zero.

The fixture Fixture: X, X∧A, X∧A∧Y, Y; strengths c_P, c_A, c_S; the bridge toForceRow from a seed row to a force row with toForceRow_gap; stage/dp/L — X from n₁, the declared evaluation of Y from n_E (Y or ¬Y); gap_dominated at every propositionally consistent world; liability (affirming evaluation, every n₀, n₁, n_E), liability_disagree (disagreeing evaluation, force withheld from n_E); disagree_region_empty while the applicability row is live; orphan_region_nonempty and orphan_no_slack after its defeat. The witness Witness.fixture_liability: strengths 4/5, 3/4, 2/3, odds 4, 3, 2, bankroll 12, at n₁ = 3, n₀ = 5, n_E = 8, intensity 10.

Per semantics, in one line each (the full table is in SETTLEMENT_FORK.md):

• (i) deductive. World-inclusive rows cost nothing and are a logical fact wearing a strength (B = 0, hadm). A genuine warrant fails hadm and is affordable at B = 3ρ while a slack world is live; X settled at n₁ changes nothing.
• (ii) evaluation. B = 3ρ whatever the evaluation says. A disagreeing evaluation realizes the deficit, empties the region while the premise and applicability rows are live, and force is withheld; the loss incurred is at most B. The only working B does not presuppose the evaluation satisfies the row.
• (iii) pegged. The same object as (ii) at n_E = ∞; every clause of the criterion survives with B = 3ρ; no clause fails on any trader.
• (iv) the defeater. At n₀ the applicability row leaves (defeat_widens); the units already bought stay on the book and pay out at the eventual world — not recovered, absorbed by B (its own share is 3 · c_A/(1 − c_A) = 9); no new liability on that row. The hazard: the defeat removes the chain's guard, and a later refutation of Y leaves the strength row an orphan pin with unbounded liability (COUNTERMODELS.md §3; src/fixture.py::harmonic_buyer_run).
• (v) item 39. Weak under all three: the warrant's K_t excludes live worlds as points and adds nothing to liveness, which is settlement's. The requested pair of credal sets is exhibited (same_projection_different_support: A is invisible when X is false). Strong would be world-inclusion, i.e. B = 0, i.e. the logical case.

Part C — the record

RECORD.md. MarketRun (grounds, docket, settlement, certificate events, authorized events, prices), RecordEntry (record state, certificate events, enforcer position; no prices), Record, trace, positionOf with positionOf_eq_position. On the countermodel: trace_not_injective/trace_not_injOn (two prices clearing the row, one record), trace_not_const/trace_not_constant (a defeat shows), price_not_mediated and docket_mediated (the record mediates the docket, not the price), decideLicensed_iff. Stopped there as instructed; items 115 and 116 carry what it made visible.

The six questions

1. Under which semantics does a bankroll exist, as a function of what? Under all three, B = 3 · max_j c_j/(1 − c_j) — the market's capital 1 + 2 times the warrant's largest odds — provided a live world clears every enforced row with surplus dominating every live deficit at those odds; for the fixture that is the all-true world while X∧A∧Y is not refuted. Intensity, tolerance, n₀, n₁, n_E and the horizon do not enter. Where no slack world is live and the region is nonempty, no B exists (the orphan pin).
2. **Does the only working B under evaluation settlement presuppose the evaluation satisfies the row?** No. Fixture.liability_disagree holds the same 3ρ when the evaluation says ¬Y; the enforcer pays out at most B and force is withheld on the emptied region. What the bound presupposes is that the agreeing world is live until the evaluation lands — that the evaluation is not foreknown — not that it agrees.
3. Is item 39 strong or weak? Weak under all three. Strong coincides with world-inclusion and zero liability, the deductive-logical case.
4. **What does Licensed need from the record that the region cannot supply? Two things, and this is the content of item 56: the citation by occurrence identity of every positively weighted row of the certificate (the region is unchanged by defeating one of two duplicating occurrences, so no region-only licence can see the defeat — A3), and the authorization of the issuing and selecting event** (two verdicts in the same interval are both supported; which one is taken is a transparency fact of the record — A4). Both are decidable from the record (decideLicensed_iff) and neither from prices.
5. Which of M1's two forms does each semantics realize? All three realize the constraint form: a row is a standing position in the priced sentences it names. Under (iii) the same row is a position in a security that never settles, and the account cannot tell the two forms apart — a constraint on a priced sentence is a position in that security. Under (iii) nothing is ever answerable to a fact, so the row's only effect is on the market's response (the price); "obligation to respond" is the only coherent reading there. Under (i) and (ii) the row is also a claim that settles.
6. Reserved to the maintainer. Below.

What this round does not establish

• The bankroll theorem's slack hypothesis is checked for the fixture at every propositionally consistent world; for a general presentation it is a hypothesis, and the round does not characterize when a region admits a slack live world.
• The orphan-pin unboundedness is test-supported: the harmonic buyer is run against a one-coordinate market maker that zeroes the aggregate, one valid selection under the maker's contract, not the pinned dependency's MarketMaker. The Lean proves the preconditions (nonempty region, no slack world, a live deficit world) and not the divergence (item 114).
• enforcer_netWorth_lt_three uses the trading firm's floor −2 from AssessmentFirm.tradingFirmTrader_netWorth_floor; the constant 3 is that dependency's, not a property of warrants.
• Nothing here is about efficient computability of the enforcer or computability of the augmented market: warrant_normative_inductor keeps computableMarket and the uptake certificate as hypotheses, as conditional_normative_inductor does.
• The seed statics' real-valued and elimination results were not ported; the forced interval of a fixture is stated and proved by hand (Countermodel.forcedInterval), not computed.
• The port's one deviation from the branch — Decidable instances and sound_of_pos — changes no ported statement, and the round did not re-verify the branch's unported theorems against main.
• The item-39 pair uses an atom invisible on the fragment; on the four priced sentences themselves no two distinct credal sets share a projection at a point mass, so the weakness exhibited is the fibre-saturation one (SEMANTIC_PROJECTION.md §3), and the stronger statement is the point exclusion.

Items filed

112 (occurrence-level defeat, the orphan pin), 113 (settlement defeat for strength rows: linear rows contrapose), 114 (the pinned-region divergence against the pinned market maker; item 40 narrowed), 115 (Licensed transport over record transitions, the rest of item 56), 116 (the record as reason trace: what it mediates, the defect, and the port's duplicate when PR #102 lands). Item 56 carries a dated narrowing.

Candidate registrations, listed and not registered

All lean-proved on main at this branch, against item 39 unless noted: WarrantEntitlement.netWorth_ge_neg_odds, liability_of_odds, warrant_normative_inductor, netWorth_nonneg_of_inclusive, Fixture.gap_dominated, Fixture.liability, Fixture.liability_disagree, Fixture.disagree_region_empty, Fixture.orphan_region_nonempty, Fixture.orphan_no_slack (item 112), RecordFixture.trace_not_injOn, trace_not_constant, price_not_mediated, docket_mediated, decideLicensed_iff (item 116). The dispatch registers only the chain lemmas.

Names, provisional

settlement semantics (the fork's parameter), bankroll schedule (B), entitlement (the row may be enforced at bounded liability), odds bankroll (3ρ), slack world (a live world clearing every enforced row strictly), orphan pin (a nonempty region with no slack world left by a per-row defeat), verdict certificate (VerdictCert), cites live (CitesLive).

Outstanding maintainer actions

1. Confirm, amend or strike M1 — DECISIONS.md, Awaiting the author, the entry of 2026-10-20. The round's reading: the two forms coincide in the account for a never-settled sentence.
2. Rule on the settlement fork (M2) — DECISIONS.md, Awaiting the author, the second entry of 2026-10-20. The round finds the fork collapses in the account; what remains open is whether a pegged semantics the substrate cannot express is wanted, and whether linear strength rows that contrapose under settlement are acceptable or the warrant form changes (item 113).
3. Merge. Reserved on the pull request, not here.

What entitles a market to enforce a warrant — the settlement fork

Verdict: ONE-DEFEASIBLE-WARRANT-IS-ENTITLED-AT-THE-ODDS-UNDER-EVERY-SETTLEMENT-SEMANTICS-WHILE-A-SLACK-WORLD-IS-LIVE-THE-FORK-COLLAPSES-IN-THE-ACCOUNT-THE-ORPHANED-STRENGTH-ROW-IS-THE-ONE-UNAFFORDABLE-CASE-ITEM-39-IS-WEAK-AND-THE-LICENCE-CHAIN-HOLDS-WITH-BOTH-CONVERSES-FAILING — the force layer's compiled position on one defeasible warrant has assessed net worth at least −3 · max_j c_j/(1 − c_j) at every live world at every date, under deductive, evaluation and pegged settlement alike, whenever some live world clears every enforced row with a surplus dominating every live deficit at the odds: the market maker's constant 1 plus the trading firm's floor 2, times the odds, with intensity, tolerance and horizon absent, so the liability hypothesis of conditional_normative_inductor is discharged in Lean as warrant_normative_inductor; the evaluation need not satisfy the row, a disagreeing evaluation empties the region while the applicability row is live and force is withheld with the loss absorbed by the bankroll; the one unaffordable case is the orphan pin — after the applicability port is defeated a refutation of Y leaves a nonempty region with no slack world, the strength row contraposes to P(X∧A) = 0, and a harmonic buyer drives the enforcer below every bound on a convergent budget; item 39 is weak under all three semantics; the licence chain Licensed → Supported → Admissible is proved with both converses refuted, the citation-by-occurrence discipline being the content of item 56; and the record of a run is neither injective nor constant in the run, with Licensed decidable from it alone.

Read REPORT.md first. The parts: LICENCE_CHAIN.md (Part A), SETTLEMENT_FORK.md (Part B, with the fixture's numbers), RECORD.md (Part C), COUNTERMODELS.md (every obstruction with its fixture). The Lean is one file, lean/Workspace/Normativity/Contrib/WarrantEntitlement.lean; the exact-rational fixture and the two market exhibits are under src/, run by tests/run.py.

Dispatch: prompts/2026-10-20-warrant-enforcement-semantics/PROMPT.md.