29. Order retention🔗

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

rule

Rules.OneOrder.Creation.mustKeep
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading) (o : Rules.OneOrder.Order)
  (firstUse finalSince : Option Rules.Core.Instant)
  (now : Rules.Core.Instant) : Bool
Rules.OneOrder.Creation.mustKeep
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (firstUse finalSince :
    Option Rules.Core.Instant)
  (now : Rules.Core.Instant) : Bool

EARS: The system shall keep an order accessible for 13 months from its creation and for 13 months from its first usage while it has an active item, and for 7 days after every item has reached a final status.

Story: As a seller, I want an order to stay retrievable while the customer can still use it, so that I can service the trip and any value it holds.

Acceptance criteria:

ONE-406.1: While an order has an active item, the system shall keep the order accessible until 13 months after its creation.
ONE-406.2: While an order has an active item and has been used, the system shall keep the order accessible until 13 months after its first usage.
ONE-406.3: When every item of an order has become closed or cancelled, the system shall keep the order accessible for 7 more days.
ONE-406.4: While an order has an active item, the system shall keep the order accessible.

The resolution defines neither an open item nor first usage. The model reads an open item as an active one, which depends on a reading of the guide (ValueReading). The instant of first usage, if any, and the instant every item reached a final status, if they all have, are inputs.

29.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-406.1	Proven	Retention of paid order, Orders kept 13 months from creation
ONE-406.2	Proven	Retention of paid order, Retention after first usage
ONE-406.3	Proven	Orders kept 7 days after their items are final, Delivered order retention
ONE-406.4	Open	Stored value never used, Orders holding value stay accessible

29.2. Guarantees🔗

29.2.1. Orders kept 13 months from creation🔗

guarantee

Rules.OneOrder.Creation.keep_from_creation
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading) (o : Rules.OneOrder.Order)
  (firstUse finalSince : Option Rules.Core.Instant)
  (now : Rules.Core.Instant)
  (hact : ∃ i ∈ o.items, Rules.OneOrder.OrderItem.isActive v i = true)
  (hnow : now < m.thirteenAfter o.createdAt) :
  Rules.OneOrder.Creation.mustKeep m v o firstUse finalSince now = true
Rules.OneOrder.Creation.keep_from_creation
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (firstUse finalSince :
    Option Rules.Core.Instant)
  (now : Rules.Core.Instant)
  (hact :
    ∃ i ∈ o.items,
      Rules.OneOrder.OrderItem.isActive v
          i =
        true)
  (hnow :
    now < m.thirteenAfter o.createdAt) :
  Rules.OneOrder.Creation.mustKeep m v o
      firstUse finalSince now =
    true

An order with an active item is kept until 13 months after its creation, under every reading and every count of months.

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

Checks acceptance criteria ONE-406.1.

29.2.2. Retention after first usage🔗

guarantee

Rules.OneOrder.Creation.keep_from_first_use
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading) (o : Rules.OneOrder.Order)
  (t : Rules.Core.Instant) (finalSince : Option Rules.Core.Instant)
  (now : Rules.Core.Instant)
  (hact : ∃ i ∈ o.items, Rules.OneOrder.OrderItem.isActive v i = true)
  (hnow : now < m.thirteenAfter t) :
  Rules.OneOrder.Creation.mustKeep m v o (some t) finalSince now = true
Rules.OneOrder.Creation.keep_from_first_use
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (t : Rules.Core.Instant)
  (finalSince : Option Rules.Core.Instant)
  (now : Rules.Core.Instant)
  (hact :
    ∃ i ∈ o.items,
      Rules.OneOrder.OrderItem.isActive v
          i =
        true)
  (hnow : now < m.thirteenAfter t) :
  Rules.OneOrder.Creation.mustKeep m v o
      (some t) finalSince now =
    true

An order with an active item that has been used is kept until 13 months after its first usage, under every reading and every count of months.

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

Checks acceptance criteria ONE-406.2.

29.2.3. Orders kept 7 days after their items are final🔗

guarantee

Rules.OneOrder.Creation.keep_after_final
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading) (o : Rules.OneOrder.Order)
  (firstUse : Option Rules.Core.Instant) (t now : Rules.Core.Instant)
  (hfinal :
    ∀ i ∈ o.items,
      i.isClosed = true ∨
        Rules.OneOrder.OrderItem.isCancelled v i = true)
  (hnow :
    now.epochSeconds <
      t.epochSeconds + Rules.OneOrder.Creation.sevenDays) :
  Rules.OneOrder.Creation.mustKeep m v o firstUse (some t) now = true
Rules.OneOrder.Creation.keep_after_final
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (firstUse : Option Rules.Core.Instant)
  (t now : Rules.Core.Instant)
  (hfinal :
    ∀ i ∈ o.items,
      i.isClosed = true ∨
        Rules.OneOrder.OrderItem.isCancelled
            v i =
          true)
  (hnow :
    now.epochSeconds <
      t.epochSeconds +
        Rules.OneOrder.Creation.sevenDays) :
  Rules.OneOrder.Creation.mustKeep m v o
      firstUse (some t) now =
    true

An order whose items have all become closed or cancelled is kept for 7 days after that, under every reading and every count of months.

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

Checks acceptance criteria ONE-406.3.

29.2.4. Orders holding value stay accessible🔗

guarantee

Rules.OneOrder.Creation.keep_while_active
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading) (o : Rules.OneOrder.Order)
  (firstUse finalSince : Option Rules.Core.Instant)
  (now : Rules.Core.Instant)
  (hact : ∃ i ∈ o.items, Rules.OneOrder.OrderItem.isActive v i = true) :
  Rules.OneOrder.Creation.mustKeep m v o firstUse finalSince now = true
Rules.OneOrder.Creation.keep_while_active
  (m : Rules.OneOrder.Creation.MonthCount)
  (v : Rules.OneOrder.ValueReading)
  (o : Rules.OneOrder.Order)
  (firstUse finalSince :
    Option Rules.Core.Instant)
  (now : Rules.Core.Instant)
  (hact :
    ∃ i ∈ o.items,
      Rules.OneOrder.OrderItem.isActive v
          i =
        true) :
  Rules.OneOrder.Creation.mustKeep m v o
      firstUse finalSince now =
    true

An order is kept while it has an active item, under every reading and every count of months.

Open question for the business. The resolution asks for 13 months from creation and 13 months from first usage, and nothing after both have passed. An item whose services are removed with their value held stays active for as long as the customer does not use the value. The example storedValueNeverUsed shows it: two years after creation the order still holds value and no longer has to be kept. What are an open item and first usage, and must an order that still holds value stay accessible?

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

Checks acceptance criteria ONE-406.4.

29.3. Examples🔗

29.3.1. Retention of paid order🔗

example

Rules.OneOrder.Creation.retentionOfPaidOrder :
  List Rules.OneOrder.Creation.RetentionRow
Rules.OneOrder.Creation.retentionOfPaidOrder :
  List
    Rules.OneOrder.Creation.RetentionRow

Given an order created on 2026-01-01 with a paid flight, which holds value. Thirteen months are counted as 396 days.

When the airline checks on 2027-01-15, 2027-03-01 and 2027-08-01 whether it must keep the order, once for an order never used and once for an order first used on 2026-06-01.

Then on 2027-01-15, within 13 months of creation, it must keep the order either way. On 2027-03-01 it must keep it only if it was used, within 13 months of its first usage. On 2027-08-01 it need not keep it.

What Lean computed:

Checked at	First use	Must keep
2027-01-15 00:00 UTC	none	yes
2027-01-15 00:00 UTC	2026-06-01 00:00 UTC	yes
2027-03-01 00:00 UTC	none	no
2027-03-01 00:00 UTC	2026-06-01 00:00 UTC	yes
2027-08-01 00:00 UTC	none	no
2027-08-01 00:00 UTC	2026-06-01 00:00 UTC	no

Checks acceptance criteria ONE-406.1, ONE-406.2.

29.3.2. Delivered order retention🔗

example

Rules.OneOrder.Creation.deliveredOrderRetention :
  List Rules.OneOrder.Creation.FinalRow
Rules.OneOrder.Creation.deliveredOrderRetention :
  List Rules.OneOrder.Creation.FinalRow

Given an order created on 2026-01-01 whose one flight was delivered, so its item is closed, on 2026-11-10.

When the airline checks on 2026-11-15 and on 2026-11-20 whether it must keep the order.

Then it must keep it on 2026-11-15, within 7 days, and need not on 2026-11-20.

What Lean computed:

Checked at	Must keep
2026-11-15 00:00 UTC	yes
2026-11-20 00:00 UTC	no

Checks acceptance criteria ONE-406.3.

29.3.3. Stored value never used🔗

example

Rules.OneOrder.Creation.storedValueNeverUsed :
  Rules.OneOrder.Creation.ValueKept
Rules.OneOrder.Creation.storedValueNeverUsed :
  Rules.OneOrder.Creation.ValueKept

Given an order created on 2026-01-01 whose flight was removed with its value held for the customer, and never used.

When the airline checks on 2028-01-01 whether it must keep the order.

Then the order still holds value under every reading, and the airline need not keep it: 13 months from creation have passed, and there was no first usage.

What Lean computed:

Holds value: yes
Must keep: no

Checks acceptance criteria ONE-406.4.

29.4. Open question🔗

The guarantee Orders holding value stay accessible is open: the example Stored value never used shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.