Item 112: Occurrence-level defeat: the orphan pin
Deference line — second wave · difficulty substantial · project normativity · closed · node item-112
— *narrowed 2026-10-21: under settleForm (DECISIONS.md M1–M2) the orphan cannot form — WarrantEntitlement.Fixture.no_strength_after, rebutted_region_nonempty; what remains is transitive retirement along cites without the settlement's closure, item 121* — *answered 2026-10-22 by the grounded rule (WarrantEntitlement.mem_survivors, registered inductor.grounded-survivors): undercutting an applicability withdraws every row that cites it, at the undercut*
The warrant-enforcement-semantics round (projects/normativity/rounds/2026-10-20-warrant-enforcement-semantics/) finds that with per-row docket ports a warrant whose applicability port has been defeated leaves its strength row behind, and a later refutation of the consequent turns that row into a pin on its antecedent — P(X∧A∧Y) ≥ c_S P(X∧A) with X∧A∧Y pinned to 0 reads P(X∧A) ≤ 0 — inside a nonempty region with no slack live world (WarrantEntitlement.Fixture.orphan_region_nonempty, orphan_no_slack). The odds bankroll has no witness there and an efficiently computable buyer drives the enforcer below every bound on a convergent budget (src/fixture.py::harmonic_buyer_run). With the applicability row live the same refutation empties the region and force is withheld (Fixture.disagree_region_empty): the per-row defeat removed the chain's guard.
Wanted: a compiler rule consuming Occurrence.cites and Occurrence.defeaters so that undercutting an applicability claim withdraws every row conditioned on it, and the theorem that under it a refutation of any link of a chain warrant either empties the region or withdraws the chain — no orphan pins.
Deliverable shape: the rule as a def on Grounds replacing Grounds.region's port-only filter, the no-orphan theorem on the fixture and in general for chains, and the fixture of this round re-run under it. Acceptance check: lake build and the axiom audit green; the round's tests/run.py extended with the rule and green. Context: .../2026-10-20-warrant-enforcement-semantics/SETTLEMENT_FORK.md (iv), COUNTERMODELS.md §3, LICENCE_CHAIN.md A1.
Deliverable shape: the rule as a def on Grounds replacing Grounds.region's port-only filter, the no-orphan theorem on the fixture and in general for chains, and the fixture of this round re-run under it.
Acceptance check: lake build and the axiom audit green; the round's tests/run.py extended with the rule and green.
Registered results bearing on this item
- inductor.grounded-survivors: An occurrence survives iff it is in the grounds, not undercut (own port or a defeater port), kept by settleOutcome, and cites a survivor; the survivors are the least fixed point of activeStep, so unde
Where it hangs
- held by normativity
Rounds and decisions that touch it
- round 2026-10-22-normative-inductor-integration
- decision What a warrant's security settles against (M2 of the warrant-enforcement-semantics round).
- decision the licence is three-level with verdicts as values, enforcement's conclusion is a defect bound with the account beside it, the record of a run is its own object, and a warrant's defeat condition belongs to the occurrence
- decision rebuttal by settlement: a form whose consequent is pinned false is rebutted, whose antecedent is pinned false is vacuous, whose premise is pinned false retires its occurrence; rebuttal does not discount applicability; interval monotonicity is traded for a reopening account; the seed statics become one file