Verified Air

30. Price guarantee at an instant🔗

Requirement ONE-501. Of its 5 acceptance criteria, 4 are proven and 1 is open.

🔗rule
Rules.OneOrder.Offers.guaranteesAt
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi : Rules.OneOrder.Offers.TimedOfferItem)
  (now : Rules.Core.Instant) : Rules.OneOrder.Offers.Guarantees
Rules.OneOrder.Offers.guaranteesAt
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (now : Rules.Core.Instant) :
  Rules.OneOrder.Offers.Guarantees

EARS: While no order has been created from an offer, the system shall treat an offer item's price and inventory as guaranteed only until both the item's guarantee time limit and the offer's expiry.

Story: As an airline, I want an offer's guarantees to end when the offer expires, so that I never stand behind a price or a seat for an offer that can no longer be accepted.

Acceptance criteria:

  • ONE-501.1: If an offer item carries no price guarantee time limit, then the system shall treat its price as not guaranteed.

  • ONE-501.2: While an instant is before an offer item's price guarantee time limit and before the offer's expiry, the system shall treat the item's price as guaranteed.

  • ONE-501.3: While an instant is before an offer item's inventory guarantee time limit and before the offer's expiry, the system shall treat the item's inventory as guaranteed.

  • ONE-501.4: The system shall end every price and inventory guarantee of an offer no later than the offer's expiry.

  • ONE-501.5: The system shall not treat an offer item's price as guaranteed at an instant at which the offer can no longer be accepted.

A guarantee runs until the earlier of its own limit and the offer's expiry. Whether it still holds at that instant is a reading of the guide (GuaranteeEnd). The offer's expiry on its own guarantees nothing.

30.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-501.1

Proven

Guarantees through the morning, No price guarantee without a limit

ONE-501.2

Proven

Guarantees through the morning, Price guaranteed before its limit

ONE-501.3

Proven

Guarantees through the morning, Inventory guaranteed before its limit

ONE-501.4

Proven

Offer expiry ends other limits, Guarantee after expiry

ONE-501.5

Open

Guaranteed prices only on offers that can be accepted, Guarantee at expiry

30.2. Guarantees🔗

30.2.1. No price guarantee without a limit🔗

🔗guarantee
Rules.OneOrder.Offers.no_limit_no_guarantee
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi : Rules.OneOrder.Offers.TimedOfferItem) (now : Rules.Core.Instant)
  (h : oi.limits.priceGuarantee = none) :
  (Rules.OneOrder.Offers.guaranteesAt b o oi now).price = false
Rules.OneOrder.Offers.no_limit_no_guarantee
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (now : Rules.Core.Instant)
  (h : oi.limits.priceGuarantee = none) :
  (Rules.OneOrder.Offers.guaranteesAt b o
        oi now).price =
    false

An offer item that carries no price guarantee time limit has no guaranteed price at any instant, under every reading of the guide.

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

Checks acceptance criteria ONE-501.1.

30.2.2. Price guaranteed before its limit🔗

🔗guarantee
Rules.OneOrder.Offers.price_guaranteed_before
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi : Rules.OneOrder.Offers.TimedOfferItem)
  (now t : Rules.Core.Instant) (ht : oi.limits.priceGuarantee = some t)
  (h1 : now < t) (h2 : now < o.expiresAt) :
  (Rules.OneOrder.Offers.guaranteesAt b o oi now).price = true
Rules.OneOrder.Offers.price_guaranteed_before
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (now t : Rules.Core.Instant)
  (ht : oi.limits.priceGuarantee = some t)
  (h1 : now < t)
  (h2 : now < o.expiresAt) :
  (Rules.OneOrder.Offers.guaranteesAt b o
        oi now).price =
    true

An offer item's price is guaranteed at every instant before both its price guarantee time limit and the offer's expiry, under every reading of the guide.

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

Checks acceptance criteria ONE-501.2.

30.2.3. Inventory guaranteed before its limit🔗

🔗guarantee
Rules.OneOrder.Offers.inventory_guaranteed_before
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi : Rules.OneOrder.Offers.TimedOfferItem)
  (now t : Rules.Core.Instant)
  (ht : oi.limits.inventoryGuarantee = some t) (h1 : now < t)
  (h2 : now < o.expiresAt) :
  (Rules.OneOrder.Offers.guaranteesAt b o oi now).inventory = true
Rules.OneOrder.Offers.inventory_guaranteed_before
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (now t : Rules.Core.Instant)
  (ht :
    oi.limits.inventoryGuarantee = some t)
  (h1 : now < t)
  (h2 : now < o.expiresAt) :
  (Rules.OneOrder.Offers.guaranteesAt b o
        oi now).inventory =
    true

An offer item's inventory is guaranteed at every instant before both its inventory guarantee time limit and the offer's expiry, under every reading of the guide.

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

Checks acceptance criteria ONE-501.3.

30.2.4. Offer expiry ends other limits🔗

🔗guarantee
Rules.OneOrder.Offers.guarantees_end_by_expiry
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi : Rules.OneOrder.Offers.TimedOfferItem) (now : Rules.Core.Instant)
  (h :
    (Rules.OneOrder.Offers.guaranteesAt b o oi now).price = true ∨
      (Rules.OneOrder.Offers.guaranteesAt b o oi now).inventory =
        true) :
  now ≤ o.expiresAt
Rules.OneOrder.Offers.guarantees_end_by_expiry
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (now : Rules.Core.Instant)
  (h :
    (Rules.OneOrder.Offers.guaranteesAt b
            o oi now).price =
        true ∨
      (Rules.OneOrder.Offers.guaranteesAt
            b o oi now).inventory =
        true) :
  now ≤ o.expiresAt

Every price and inventory guarantee of an offer ends no later than the offer's expiry, under every reading of the guide, whatever the item's own limits say.

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

Checks acceptance criteria ONE-501.4.

30.2.5. Guaranteed prices only on offers that can be accepted🔗

🔗guarantee
Rules.OneOrder.Offers.guaranteed_while_acceptable
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi : Rules.OneOrder.Offers.TimedOfferItem) (now : Rules.Core.Instant)
  (orderId : String)
  (h : (Rules.OneOrder.Offers.guaranteesAt b o oi now).price = true) :
  Rules.OneOrder.accept o.toOffer now orderId ≠
    Except.error Rules.OfferOrder.Rejection.expired
Rules.OneOrder.Offers.guaranteed_while_acceptable
  (b : Rules.OneOrder.Offers.GuaranteeEnd)
  (o : Rules.OneOrder.Offers.TimedOffer)
  (oi :
    Rules.OneOrder.Offers.TimedOfferItem)
  (now : Rules.Core.Instant)
  (orderId : String)
  (h :
    (Rules.OneOrder.Offers.guaranteesAt b
          o oi now).price =
      true) :
  Rules.OneOrder.accept o.toOffer now
      orderId ≠
    Except.error
      Rules.OfferOrder.Rejection.expired

An offer item's price is guaranteed only at instants at which the offer can still be accepted.

Open question for the business. The guide says a price is guaranteed until its time limit and does not say whether the limit's own instant is inside. An offer is rejected as expired at its expiry instant. Under the reading that a guarantee still holds at its instant, an item whose price guarantee ends at the same instant as the offer has a guaranteed price at an instant when the offer can no longer be accepted. The example guaranteeAtExpiry shows it. Does a price guarantee still hold at the instant its time limit names?

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

Checks acceptance criteria ONE-501.5.

30.3. Examples🔗

30.3.1. Guarantees through the morning🔗

🔗example
Rules.OneOrder.Offers.guaranteesThroughTheMorning :
  List Rules.OneOrder.Offers.GuaranteeRow
Rules.OneOrder.Offers.guaranteesThroughTheMorning :
  List Rules.OneOrder.Offers.GuaranteeRow

Given an offer valid until 12:00 UTC with a flight whose price is guaranteed until 11:00 and whose seat is guaranteed until 11:30, and a bag with no guarantees.

When the guarantees are read at 10:00, 11:15 and 11:45.

Then at 10:00 the flight's price and seat are guaranteed. At 11:15 only its seat is, and at 11:45 neither is. The bag's price and inventory are never guaranteed, although the offer is still valid. Both readings of the guide give the same answers, since no instant falls on a limit.

What Lean computed:

Time

Item

Price

Inventory

2026-10-27 10:00 UTC

OI-FLT

yes

yes

2026-10-27 10:00 UTC

OI-BAG

no

no

2026-10-27 11:15 UTC

OI-FLT

no

yes

2026-10-27 11:15 UTC

OI-BAG

no

no

2026-10-27 11:45 UTC

OI-FLT

no

no

2026-10-27 11:45 UTC

OI-BAG

no

no

Checks acceptance criteria ONE-501.1, ONE-501.2, ONE-501.3.

30.3.2. Guarantee after expiry🔗

🔗example
Rules.OneOrder.Offers.guaranteeAfterExpiry :
  Rules.OneOrder.Offers.CappedGuarantee
Rules.OneOrder.Offers.guaranteeAfterExpiry :
  Rules.OneOrder.Offers.CappedGuarantee

Given an offer valid until 12:00 UTC with a flight whose price guarantee ends at 13:00, an hour after the offer expires. This is the case the survey noted for the Offers and Time Limits pages.

When the guarantee is read at 12:30.

Then the item's own limit has not passed, but the rule does not guarantee the price under either reading: no guarantee outlasts the offer.

What Lean computed:

  • Limit alone: yes

  • Exclusive: no

  • Inclusive: no

Checks acceptance criteria ONE-501.4.

30.3.3. Guarantee at expiry🔗

🔗example
Rules.OneOrder.Offers.guaranteeAtExpiry :
  Rules.OneOrder.Offers.GuaranteeAtExpiry
Rules.OneOrder.Offers.guaranteeAtExpiry :
  Rules.OneOrder.Offers.GuaranteeAtExpiry

Given an offer valid until 12:00 UTC with a flight whose price guarantee also ends at 12:00.

When the guarantee is read at 12:00, and the customer accepts the offer at 12:00.

Then the offer is rejected as expired. Under the reading that a guarantee ends at its instant, the price is not guaranteed. Under the reading that it still holds at its instant, the price is guaranteed for an offer that can no longer be accepted.

What Lean computed:

  • Exclusive: no

  • Inclusive: yes

  • Acceptance: expired

Checks acceptance criteria ONE-501.5.

30.4. Open question🔗

The guarantee Guaranteed prices only on offers that can be accepted is open: the example Guarantee at expiry shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.