31. Time limits of a new order🔗

Requirement ONE-502. Of its 6 acceptance criteria, 3 are proven and 3 are open.

rule

Rules.OneOrder.Offers.createOrder
  (r : Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
  (orderId : String) :
  Except Rules.OneOrder.Offers.CreateRejection
    Rules.OneOrder.Offers.NewOrder
Rules.OneOrder.Offers.createOrder
  (r :
    Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (now : Rules.Core.Instant)
  (orderId : String) :
  Except
    Rules.OneOrder.Offers.CreateRejection
    Rules.OneOrder.Offers.NewOrder

EARS: When a customer accepts an offer whose items carry time limits, the system shall create the order as ONE-001 does and give each order item its payment time limit and price guarantee from its offer item.

Story: As an airline, I want each new order item to start with the payment time limit and price guarantee its offer item promised, so that the customer gets the time to pay and the price the offer stated.

Acceptance criteria:

ONE-502.1: When an order is created from an offer item whose payment time limit is stated only as a duration, the system shall set the order item's payment time limit to the creation instant plus that duration.
ONE-502.2: When an order is created from an offer item whose payment time limit is stated only as a fixed date and time, the system shall set the order item's payment time limit to that instant.
ONE-502.3: When an order is created, the system shall carry each offer item's price guarantee time limit into its order item.
ONE-502.4: If a customer accepts an offer after the price guarantee of one of its items has lapsed, then the system shall not create the order at the offered price.
ONE-502.5: When an order is created, the system shall give no order item a payment time limit before the order's creation.
ONE-502.6: When an offer item's payment time limit is a duration of zero, the system shall accept a payment for its order item made at the instant the order is created.

The checks of ONE-001 run first (accept). Then, under the reading that asks for a new offer, an item whose price guarantee has lapsed refuses the acceptance. Which payment time limit applies when an offer item states both forms is a reading of the guide (BothForms).

31.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-502.1	Proven	Both forms readings, New order limits, Payment time limit from a duration
ONE-502.2	Proven	Both forms readings, New order limits, Payment time limit from a fixed instant
ONE-502.3	Proven	Price guarantee carried into the order, New order limits
ONE-502.4	Open	No order at a lapsed price, Lapsed guarantee accepted
ONE-502.5	Open	No order item overdue at creation, Fixed limit before creation
ONE-502.6	Open	Zero duration payment, Payment due at creation can be made

31.2. Guarantees🔗

31.2.1. Payment time limit from a duration🔗

guarantee

Rules.OneOrder.Offers.createOrder_duration
  (r : Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
  (orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
  (h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
  (oi : Rules.OneOrder.Offers.TimedOfferItem) (hoi : oi ∈ o.items)
  (d : ℕ) (hd : oi.limits.payWithin = some d)
  (hb : oi.limits.payBy = none) :
  ∃ ni ∈ n.items,
    ni.item.fromOfferItem = oi.item.id ∧
      ni.paymentBy =
        some (Rules.OneOrder.Offers.secondsAfter n.createdAt d)
Rules.OneOrder.Offers.createOrder_duration
  (r :
    Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (n : Rules.OneOrder.Offers.NewOrder)
  (h :
    Rules.OneOrder.Offers.createOrder r o
        now orderId =
      Except.ok n)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (hoi : oi ∈ o.items) (d : ℕ)
  (hd : oi.limits.payWithin = some d)
  (hb : oi.limits.payBy = none) :
  ∃ ni ∈ n.items,
    ni.item.fromOfferItem = oi.item.id ∧
      ni.paymentBy =
        some
          (Rules.OneOrder.Offers.secondsAfter
            n.createdAt d)

An order item created from an offer item whose payment time limit is stated only as a duration must be paid by the creation instant plus that duration.

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

Checks acceptance criteria ONE-502.1.

31.2.2. Payment time limit from a fixed instant🔗

guarantee

Rules.OneOrder.Offers.createOrder_fixed
  (r : Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
  (orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
  (h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
  (oi : Rules.OneOrder.Offers.TimedOfferItem) (hoi : oi ∈ o.items)
  (t : Rules.Core.Instant) (hd : oi.limits.payWithin = none)
  (hb : oi.limits.payBy = some t) :
  ∃ ni ∈ n.items,
    ni.item.fromOfferItem = oi.item.id ∧ ni.paymentBy = some t
Rules.OneOrder.Offers.createOrder_fixed
  (r :
    Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (n : Rules.OneOrder.Offers.NewOrder)
  (h :
    Rules.OneOrder.Offers.createOrder r o
        now orderId =
      Except.ok n)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (hoi : oi ∈ o.items)
  (t : Rules.Core.Instant)
  (hd : oi.limits.payWithin = none)
  (hb : oi.limits.payBy = some t) :
  ∃ ni ∈ n.items,
    ni.item.fromOfferItem = oi.item.id ∧
      ni.paymentBy = some t

An order item created from an offer item whose payment time limit is stated only as a fixed date and time must be paid by that instant.

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

Checks acceptance criteria ONE-502.2.

31.2.3. Price guarantee carried into the order🔗

guarantee

Rules.OneOrder.Offers.createOrder_keeps_guarantee
  (r : Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
  (orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
  (h :
    Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n) :
  List.map (fun x ↦ x.priceGuarantee) n.items =
    List.map (fun x ↦ x.limits.priceGuarantee) o.items
Rules.OneOrder.Offers.createOrder_keeps_guarantee
  (r :
    Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (n : Rules.OneOrder.Offers.NewOrder)
  (h :
    Rules.OneOrder.Offers.createOrder r o
        now orderId =
      Except.ok n) :
  List.map (fun x ↦ x.priceGuarantee)
      n.items =
    List.map
      (fun x ↦ x.limits.priceGuarantee)
      o.items

Each order item keeps the price guarantee time limit of its offer item, in the order of the offer's items.

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

Checks acceptance criteria ONE-502.3.

31.2.4. No order at a lapsed price🔗

guarantee

Rules.OneOrder.Offers.createOrder_price_guaranteed
  (r : Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
  (orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
  (h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
  (oi : Rules.OneOrder.Offers.TimedOfferItem) :
  oi ∈ o.items →
    Rules.OneOrder.Offers.TimedOffer.guaranteeLapsed r.guaranteeEnd o oi
        now =
      false
Rules.OneOrder.Offers.createOrder_price_guaranteed
  (r :
    Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (n : Rules.OneOrder.Offers.NewOrder)
  (h :
    Rules.OneOrder.Offers.createOrder r o
        now orderId =
      Except.ok n)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem) :
  oi ∈ o.items →
    Rules.OneOrder.Offers.TimedOffer.guaranteeLapsed
        r.guaranteeEnd o oi now =
      false

No order is created at the offered price while the price guarantee of one of the offer's items has lapsed.

Open question for the business. The guide recommends repricing into a new offer when a price guarantee has lapsed, and does not say what the airline must do when the customer accepts the offer before it expires. Under the reading that creates the order at the offered price, an offer whose 30 minute price guarantee lapsed is accepted at the offered price one minute before the offer expires. The example lapsedGuaranteeAccepted shows it. Is acceptance in this window refused, sent back for a new offer, or honoured at the offered price?

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

Checks acceptance criteria ONE-502.4.

31.2.5. No order item overdue at creation🔗

guarantee

Rules.OneOrder.Offers.createOrder_limit_not_before_creation
  (r : Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
  (orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
  (h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
  (ni : Rules.OneOrder.Offers.NewOrderItem) :
  ni ∈ n.items →
    ∀ (t : Rules.Core.Instant), ni.paymentBy = some t → n.createdAt ≤ t
Rules.OneOrder.Offers.createOrder_limit_not_before_creation
  (r :
    Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (n : Rules.OneOrder.Offers.NewOrder)
  (h :
    Rules.OneOrder.Offers.createOrder r o
        now orderId =
      Except.ok n)
  (ni :
    Rules.OneOrder.Offers.NewOrderItem) :
  ni ∈ n.items →
    ∀ (t : Rules.Core.Instant),
      ni.paymentBy = some t →
        n.createdAt ≤ t

No order item starts with a payment time limit before the order's creation.

Open question for the business. An offer item may state its payment time limit as a fixed date and time, and the guide does not say what happens when that instant has passed by the time the order is created. The rule copies the instant, so the order item is overdue the moment it exists. The example fixedLimitBeforeCreation shows it. Is such an acceptance refused, or does the order item get a new payment time limit?

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

Checks acceptance criteria ONE-502.5.

31.2.6. Payment due at creation can be made🔗

guarantee

Rules.OneOrder.Offers.zero_duration_payable
  (r : Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer) (now : Rules.Core.Instant)
  (orderId : String) (n : Rules.OneOrder.Offers.NewOrder)
  (h : Rules.OneOrder.Offers.createOrder r o now orderId = Except.ok n)
  (hz :
    ∀ oi ∈ o.items,
      oi.limits.payWithin = some 0 ∧ oi.limits.payBy = none)
  (p : Rules.OneOrder.Payment.Transaction) :
  Rules.OneOrder.Payment.acceptPayment n.payable p n.createdAt ≠
    Except.error Rules.OneOrder.Payment.PaymentRejection.timeLimitPassed
Rules.OneOrder.Offers.zero_duration_payable
  (r :
    Rules.OneOrder.Offers.CreationReading)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (now : Rules.Core.Instant)
  (orderId : String)
  (n : Rules.OneOrder.Offers.NewOrder)
  (h :
    Rules.OneOrder.Offers.createOrder r o
        now orderId =
      Except.ok n)
  (hz :
    ∀ oi ∈ o.items,
      oi.limits.payWithin = some 0 ∧
        oi.limits.payBy = none)
  (p :
    Rules.OneOrder.Payment.Transaction) :
  Rules.OneOrder.Payment.acceptPayment
      n.payable p n.createdAt ≠
    Except.error
      Rules.OneOrder.Payment.PaymentRejection.timeLimitPassed

An order item whose offer item's payment time limit is a duration of zero can be paid at the instant the order is created.

Open question for the business. The guide says a payment time limit of zero means payment is due at order creation. The rule sets the order item's limit to the creation instant, and the payment rule of ONE-304 rejects a payment made at or after the limit, so no payment for the item is ever on time. The example zeroDurationPayment shows it. Is a payment made at the creation instant on time, or must it come with the request that creates the order?

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

Checks acceptance criteria ONE-502.6.

31.3. Examples🔗

31.3.1. Both forms readings🔗

example

Rules.OneOrder.Offers.bothFormsReadings :
  List Rules.OneOrder.Offers.BothFormsRow
Rules.OneOrder.Offers.bothFormsReadings :
  List Rules.OneOrder.Offers.BothFormsRow

Given an offer item that states its payment time limit both as 72 hours after the order is created and as 12:00 UTC on 28 October.

When the order is created at 11:00 on 27 October.

Then the order item must be paid by 11:00 on 30 October if the duration applies, and by 12:00 on 28 October if the fixed date and time applies or the earlier of the two does.

What Lean computed:

Reading	Payment by
duration	2026-10-30 11:00 UTC
fixed	2026-10-28 12:00 UTC
earlier	2026-10-28 12:00 UTC

Checks acceptance criteria ONE-502.1, ONE-502.2.

31.3.2. New order limits🔗

example

Rules.OneOrder.Offers.newOrderLimits :
  Except Rules.OneOrder.Offers.CreateRejection
    (List Rules.OneOrder.Offers.NewItemRow)
Rules.OneOrder.Offers.newOrderLimits :
  Except
    Rules.OneOrder.Offers.CreateRejection
    (List
      Rules.OneOrder.Offers.NewItemRow)

Given an offer valid until 12:00 UTC on 27 October. Its flight has a price guarantee until 11:30 and 72 hours to pay after the order is created. Its bag must be paid by 12:00 UTC on 28 October.

When the customer accepts the offer at 11:00.

Then the flight's order item must be paid by 11:00 on 30 October, 72 hours after creation, and keeps its price guarantee until 11:30. The bag's order item must be paid by 12:00 on 28 October and has no price guarantee.

What Lean computed:

Accepted. The result:

From offer item	Payment by	Price guarantee
OI-FLT	2026-10-30 11:00 UTC	2026-10-27 11:30 UTC
OI-BAG	2026-10-28 12:00 UTC	none

Checks acceptance criteria ONE-502.1, ONE-502.2, ONE-502.3.

31.3.3. Lapsed guarantee accepted🔗

example

Rules.OneOrder.Offers.lapsedGuaranteeAccepted :
  List Rules.OneOrder.Offers.LapsedRow
Rules.OneOrder.Offers.lapsedGuaranteeAccepted :
  List Rules.OneOrder.Offers.LapsedRow

Given an offer made at 10:00 UTC and valid until 12:00, whose flight at 300.00 EUR has its price guaranteed for 30 minutes, until 10:30. This is the case the survey noted for the Time Limits and Pricing Offers pages.

When the customer accepts the offer at 11:59, one minute before it expires.

Then the price is no longer guaranteed. Under the reading that asks for a new offer, no order is created. Under the reading that keeps the offered price, the order is created with the flight at 300.00 EUR, a price the airline no longer stands behind.

What Lean computed:

Reading	Price guaranteed	Outcome
reprice	no	error price guarantee lapsed
offered price	no	ok 300.00 EUR

Checks acceptance criteria ONE-502.4.

31.3.4. Fixed limit before creation🔗

example

Rules.OneOrder.Offers.fixedLimitBeforeCreation :
  Except Rules.OneOrder.Offers.CreateRejection
    Rules.OneOrder.Offers.LimitAtCreation
Rules.OneOrder.Offers.fixedLimitBeforeCreation :
  Except
    Rules.OneOrder.Offers.CreateRejection
    Rules.OneOrder.Offers.LimitAtCreation

Given an offer valid until 12:00 UTC whose bag must be paid by 10:30, a fixed date and time.

When the customer accepts the offer at 11:00.

Then the order is created, and its bag item must be paid by 10:30, half an hour before the order existed.

What Lean computed:

Accepted. The result:

Created at: 2026-10-27 11:00 UTC
Payment by: 2026-10-27 10:30 UTC
Overdue at creation: yes

Checks acceptance criteria ONE-502.5.

31.3.5. Zero duration payment🔗

example

Rules.OneOrder.Offers.zeroDurationPayment :
  Except Rules.OneOrder.Offers.CreateRejection
    Rules.OneOrder.Offers.PaymentAtCreation
Rules.OneOrder.Offers.zeroDurationPayment :
  Except
    Rules.OneOrder.Offers.CreateRejection
    Rules.OneOrder.Offers.PaymentAtCreation

Given an offer valid until 12:00 UTC whose flight at 300.00 EUR has a payment time limit of zero: payment is due at order creation.

When the customer accepts the offer at 11:00 and pays 300.00 EUR by card at 11:00.

Then the order item must be paid by 11:00, and the payment rule of ONE-304 rejects the payment because the time limit has been reached. No payment for the item is ever on time.

What Lean computed:

Accepted. The result:

Created at: 2026-10-27 11:00 UTC
Payment by: 2026-10-27 11:00 UTC
Payment: error time limit passed

Checks acceptance criteria ONE-502.6.

31.4. Open question🔗

The guarantee No order at a lapsed price is open: the example Lapsed guarantee accepted shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

31.5. Open question🔗

The guarantee No order item overdue at creation is open: the example Fixed limit before creation shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.

31.6. Open question🔗

The guarantee Payment due at creation can be made is open: the example Zero duration payment shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.