23. Unpaid item at its time limit🔗

Requirement ONE-306. Of its 6 acceptance criteria, 4 are proven and 2 are open.

rule

Rules.OneOrder.Payment.expireUnpaid
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal) (now : Rules.Core.Instant)
  (o : Rules.OneOrder.Payment.PayableOrder) :
  Rules.OneOrder.Payment.PayableOrder
Rules.OneOrder.Payment.expireUnpaid
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal)
  (now : Rules.Core.Instant)
  (o :
    Rules.OneOrder.Payment.PayableOrder) :
  Rules.OneOrder.Payment.PayableOrder

EARS: When an order item's payment time limit passes with no SUCCESSFUL payment covering it, the system shall remove the item and mark FAILED every PENDING payment that covers it.

Story: As an airline, I want unpaid order items removed when their payment time limit passes, so that seats and services are not held for customers who do not pay.

Acceptance criteria:

ONE-306.1: When an order item's payment time limit has passed and no SUCCESSFUL payment covers it, the system shall remove the item, cancelling every service of it that the delivery status table lets end, so that none of those services is live afterwards.
ONE-306.2: When an order item is removed at its payment time limit, the system shall mark FAILED every PENDING payment that covers it.
ONE-306.3: If a SUCCESSFUL payment covers an order item, then the system shall not remove the item at a payment time limit.
ONE-306.4: While an order item's payment time limit has not passed, the system shall leave the item unchanged.
ONE-306.5: The system shall not keep an unpaid order item in the order indefinitely.
ONE-306.6: When an order item is removed at its payment time limit, the system shall leave none of its services holding value.

A time limit passes at its instant, as an offer expires at its expiry instant. Which delivery status a removed item's services end in is a reading of the guide (see Removal), and each service gets there through the delivery status table (Delivery.endWith).

23.1. How each acceptance criterion is checked🔗

A criterion is proven when a guarantee below proves it for every input, and example only when only examples check it.

Criterion	Status	Checked by
ONE-306.1	Proven	Unpaid items are removed at their time limit, Unpaid at time limit, Late redirect capture
ONE-306.2	Proven	Unpaid at time limit, Pending payments fail at the time limit, Late redirect capture
ONE-306.3	Proven	Paid items are not removed, Unpaid at time limit
ONE-306.4	Proven	Unpaid at time limit, Items before their time limit are unchanged
ONE-306.5	Open	No time limit, Time limit on unpaid items
ONE-306.6	Open	Removed items hold no value, Removal statuses

23.2. Guarantees🔗

23.2.1. Unpaid items are removed at their time limit🔗

guarantee

Rules.OneOrder.Payment.expireUnpaid_removes
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal) (now : Rules.Core.Instant)
  (o : Rules.OneOrder.Payment.PayableOrder)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
  (t : Rules.Core.Instant) (ht : pi.timeLimit = some t) (hle : now ≥ t)
  (hunpaid :
    Rules.OneOrder.Payment.isPaid o.payments pi.item.id = false) :
  ∃ pi' ∈ (Rules.OneOrder.Payment.expireUnpaid m r now o).items,
    pi'.item.id = pi.item.id ∧
      ∀ s ∈ pi.item.services,
        (Rules.OneOrder.Delivery.nextDelivery m r.event s).isSome =
            true →
          ∃ s' ∈ pi'.item.services,
            s'.id = s.id ∧
              s'.status = Rules.OneOrder.ServiceStatus.cancelled ∧
                Rules.OneOrder.Delivery.isLive s' = false
Rules.OneOrder.Payment.expireUnpaid_removes
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal)
  (now : Rules.Core.Instant)
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ o.items)
  (t : Rules.Core.Instant)
  (ht : pi.timeLimit = some t)
  (hle : now ≥ t)
  (hunpaid :
    Rules.OneOrder.Payment.isPaid
        o.payments pi.item.id =
      false) :
  ∃
    pi' ∈
      (Rules.OneOrder.Payment.expireUnpaid
          m r now o).items,
    pi'.item.id = pi.item.id ∧
      ∀ s ∈ pi.item.services,
        (Rules.OneOrder.Delivery.nextDelivery
                m r.event s).isSome =
            true →
          ∃ s' ∈ pi'.item.services,
            s'.id = s.id ∧
              s'.status =
                  Rules.OneOrder.ServiceStatus.cancelled ∧
                Rules.OneOrder.Delivery.isLive
                    s' =
                  false

An order item whose payment time limit has passed, with no SUCCESSFUL payment covering it, is removed: each of its services that the delivery status table lets end is cancelled and no longer live, under every reading.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-306.1.

23.2.2. Pending payments fail at the time limit🔗

guarantee

Rules.OneOrder.Payment.expireUnpaid_fails_pending
  (mr : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal) (now : Rules.Core.Instant)
  (o : Rules.OneOrder.Payment.PayableOrder)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
  (t : Rules.Core.Instant) (ht : pi.timeLimit = some t) (hle : now ≥ t)
  (hunpaid :
    Rules.OneOrder.Payment.isPaid o.payments pi.item.id = false)
  (p : Rules.OneOrder.Payment.Transaction) (hp : p ∈ o.payments)
  (hpend : p.status = Rules.OneOrder.Payment.PaymentStatus.pending)
  (hc : pi.item.id ∈ p.covers) :
  ∃ p' ∈ (Rules.OneOrder.Payment.expireUnpaid mr r now o).payments,
    p'.id = p.id ∧
      p'.status = Rules.OneOrder.Payment.PaymentStatus.failed
Rules.OneOrder.Payment.expireUnpaid_fails_pending
  (mr :
    Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal)
  (now : Rules.Core.Instant)
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ o.items)
  (t : Rules.Core.Instant)
  (ht : pi.timeLimit = some t)
  (hle : now ≥ t)
  (hunpaid :
    Rules.OneOrder.Payment.isPaid
        o.payments pi.item.id =
      false)
  (p : Rules.OneOrder.Payment.Transaction)
  (hp : p ∈ o.payments)
  (hpend :
    p.status =
      Rules.OneOrder.Payment.PaymentStatus.pending)
  (hc : pi.item.id ∈ p.covers) :
  ∃
    p' ∈
      (Rules.OneOrder.Payment.expireUnpaid
          mr r now o).payments,
    p'.id = p.id ∧
      p'.status =
        Rules.OneOrder.Payment.PaymentStatus.failed

When an order item is removed at its payment time limit, every payment covering it that was PENDING is FAILED afterwards.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-306.2.

23.2.3. Paid items are not removed🔗

guarantee

Rules.OneOrder.Payment.expireUnpaid_keeps_paid
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal) (now : Rules.Core.Instant)
  (o : Rules.OneOrder.Payment.PayableOrder)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
  (hpaid : Rules.OneOrder.Payment.isPaid o.payments pi.item.id = true) :
  pi ∈ (Rules.OneOrder.Payment.expireUnpaid m r now o).items
Rules.OneOrder.Payment.expireUnpaid_keeps_paid
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal)
  (now : Rules.Core.Instant)
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ o.items)
  (hpaid :
    Rules.OneOrder.Payment.isPaid
        o.payments pi.item.id =
      true) :
  pi ∈
    (Rules.OneOrder.Payment.expireUnpaid m
        r now o).items

An order item that a SUCCESSFUL payment covers is never removed at a payment time limit.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-306.3.

23.2.4. Items before their time limit are unchanged🔗

guarantee

Rules.OneOrder.Payment.expireUnpaid_keeps_before_limit
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal) (now : Rules.Core.Instant)
  (o : Rules.OneOrder.Payment.PayableOrder)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
  (hbefore :
    ∀ (t : Rules.Core.Instant), pi.timeLimit = some t → now < t) :
  pi ∈ (Rules.OneOrder.Payment.expireUnpaid m r now o).items
Rules.OneOrder.Payment.expireUnpaid_keeps_before_limit
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal)
  (now : Rules.Core.Instant)
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ o.items)
  (hbefore :
    ∀ (t : Rules.Core.Instant),
      pi.timeLimit = some t → now < t) :
  pi ∈
    (Rules.OneOrder.Payment.expireUnpaid m
        r now o).items

An order item whose payment time limit has not passed, or that has none, is left as it was.

Proven Lean checked the proof, and the proof depends on no unproven step.

Checks acceptance criteria ONE-306.4.

23.2.5. Time limit on unpaid items🔗

guarantee

Rules.OneOrder.Payment.unpaid_item_removed_eventually
  (m : Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal)
  (o : Rules.OneOrder.Payment.PayableOrder)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
  (hunpaid :
    Rules.OneOrder.Payment.isPaid o.payments pi.item.id = false) :
  ∃ t,
    ∀ now ≥ t,
      Rules.OneOrder.Payment.PayableItem.remove m r pi ∈
        (Rules.OneOrder.Payment.expireUnpaid m r now o).items
Rules.OneOrder.Payment.unpaid_item_removed_eventually
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (r : Rules.OneOrder.Payment.Removal)
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ o.items)
  (hunpaid :
    Rules.OneOrder.Payment.isPaid
        o.payments pi.item.id =
      false) :
  ∃ t,
    ∀ now ≥ t,
      Rules.OneOrder.Payment.PayableItem.remove
          m r pi ∈
        (Rules.OneOrder.Payment.expireUnpaid
            m r now o).items

An unpaid order item does not stay in the order indefinitely: from some instant on, the time limit rule removes it.

Open question for the business. The rule removes an item only when its payment time limit passes, and the guide lets an airline create an order item without one. The ARMI guidance expects a limit on every unpaid item, while the EASD guide says a missing limit only means the airline gave no advice. An item without a limit is never removed and holds its services with nothing paid; the example noTimeLimit shows it a year after the order was created. May an unpaid order item exist without a payment time limit, and if so, may it stay unpaid indefinitely?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-306.5.

23.2.6. Removed items hold no value🔗

guarantee

Rules.OneOrder.Payment.removed_item_holds_no_value
  (m : Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading) (r : Rules.OneOrder.Payment.Removal)
  (now : Rules.Core.Instant) (o : Rules.OneOrder.Payment.PayableOrder)
  (pi : Rules.OneOrder.Payment.PayableItem) (hpi : pi ∈ o.items)
  (hl : o.lapses now pi = true) :
  Rules.OneOrder.OrderItem.isActive v
      (Rules.OneOrder.Payment.PayableItem.remove m r pi).item =
    false
Rules.OneOrder.Payment.removed_item_holds_no_value
  (m :
    Rules.OneOrder.Delivery.MoveReading)
  (v : Rules.OneOrder.ValueReading)
  (r : Rules.OneOrder.Payment.Removal)
  (now : Rules.Core.Instant)
  (o :
    Rules.OneOrder.Payment.PayableOrder)
  (pi :
    Rules.OneOrder.Payment.PayableItem)
  (hpi : pi ∈ o.items)
  (hl : o.lapses now pi = true) :
  Rules.OneOrder.OrderItem.isActive v
      (Rules.OneOrder.Payment.PayableItem.remove
          m r pi).item =
    false

An order item removed at its payment time limit holds no value: none of its services holds value afterwards.

Open question for the business. The guide says such an item is removed and names no resulting statuses. If its services become REMOVED, none holds value under every reading of the guide. If they become EXPIRED, whether they hold value is itself unsettled: under the cautious reading an expired service holds value, so the removed item stays active and keeps its order opened. If they become REMOVED HOLD VALUE, they hold value under every reading. The example removalStatuses shows all three. Which delivery status does an item's service take when its payment time limit passes unpaid?

Open The proof is not complete. See the open questions chapter.

Checks acceptance criteria ONE-306.6.

23.3. Examples🔗

23.3.1. Late redirect capture🔗

example

Rules.OneOrder.Payment.lateRedirectCapture :
  Rules.OneOrder.Payment.LateCapture
Rules.OneOrder.Payment.lateRedirectCapture :
  Rules.OneOrder.Payment.LateCapture

Given the trip at 100.00 EUR, unpaid, with a redirected card payment for it still pending.

When the payment time limit passes, and one minute later the customer completes the redirect and the airline reports the card transaction successful.

Then at the limit the trip is removed and the payment fails. Under the final reading the late report changes nothing. Under the late capture reading the payment becomes successful, but the trip's flights stay removed: the customer has paid for nothing.

What Lean computed:

Payment at limit: failed
Trip at limit: removed, removed
Under final reading: failed
Under late capture reading: successful
Trip after capture: removed, removed

Checks acceptance criteria ONE-303.3, ONE-306.1, ONE-306.2.

23.3.2. Unpaid at time limit🔗

example

Rules.OneOrder.Payment.unpaidAtTimeLimit :
  Rules.OneOrder.Payment.OrderView
Rules.OneOrder.Payment.unpaidAtTimeLimit :
  Rules.OneOrder.Payment.OrderView

Given the trip and the bag, due by 2026-10-27 12:00 UTC, and the free seat, due a day later. The bag was paid by card. A redirected card payment for the trip is still pending.

When the trip's payment time limit passes, with removal to the statuses CANCELLED and REMOVED.

Then the trip is removed and its pending payment fails. The paid bag stays ready to proceed, and the seat, whose limit has not passed, is unchanged.

What Lean computed:

Payments: successful, failed
Items: see the table below.

Items:

Item	Paid	Delivery	Time limit
TRIP	no	removed, removed	2026-10-27 12:00 UTC
BAG	yes	ready to proceed	none
SEAT	no	confirmed	2026-10-28 12:00 UTC

Checks acceptance criteria ONE-306.1, ONE-306.2, ONE-306.3, ONE-306.4.

23.3.3. No time limit🔗

example

Rules.OneOrder.Payment.noTimeLimit : Rules.OneOrder.Payment.OrderView
Rules.OneOrder.Payment.noTimeLimit :
  Rules.OneOrder.Payment.OrderView

Given an order created without payment, where the airline gave the trip no payment time limit.

When a year has passed and nothing has been paid.

Then the trip is still in the order with its flights confirmed, holding its seats with nothing paid.

What Lean computed:

Payments: none
Items: see the table below.

Items:

Item	Paid	Delivery	Time limit
TRIP	no	confirmed, confirmed	none

Checks acceptance criteria ONE-306.5.

23.3.4. Removal statuses🔗

example

Rules.OneOrder.Payment.removalStatuses :
  List Rules.OneOrder.Payment.RemovalRow
Rules.OneOrder.Payment.removalStatuses :
  List Rules.OneOrder.Payment.RemovalRow

Given the trip at 100.00 EUR, unpaid, with a payment time limit.

When the limit passes and the trip is removed, its services cancelled and ended in one of the three delivery statuses a removal can give.

Then with REMOVED the item is cancelled under both readings of the guide. With EXPIRED it stays active under the cautious reading, where an expired service holds value. With REMOVED HOLD VALUE it stays active under both.

What Lean computed:

Removed as	Cautious	Strict
removed	cancelled	cancelled
expired	active	cancelled
removed hold value	active	active

Checks acceptance criteria ONE-306.6.

23.4. Open question🔗

The guarantee Time limit on unpaid items is open: the example No time limit shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

23.5. Open question🔗

The guarantee Removed items hold no value is open: the example Removal statuses shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.