44. Consequence of a missed time limit🔗

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

rule

Rules.OneOrder.AirlineChange.consequenceAt
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant) :
  Option Rules.OneOrder.AirlineChange.Inaction
Rules.OneOrder.AirlineChange.consequenceAt
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant) :
  Option
    Rules.OneOrder.AirlineChange.Inaction

EARS: When a time limit of a change notice passes and the seller has not answered, the system shall apply the consequence of inaction of the follow-up action whose time limit passed first.

Story: As a seller, I want to know what happens if I do not answer a change notice in time, so that the customer is not surprised by an outcome nobody chose.

Acceptance criteria:

ONE-702.1: When a time limit that carries a consequence of inaction passes, the system shall apply the consequence of a follow-up action whose time limit is the earliest.
ONE-702.2: If no follow-up action of a notice has a time limit, then the system shall apply no consequence of inaction.
ONE-702.3: While no time limit of a notice has passed, the system shall apply no consequence of inaction.
ONE-702.4: If the seller does not answer a change notice that carries follow-up actions, then the system shall resolve it before the affected flight departs.

A time limit passes at its instant, as an offer expires at its expiry instant. A follow-up action with no stated consequence takes the reading's default (FollowUpReading). The result is the consequence that applies at the instant given, or none when none applies yet.

44.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-702.1	Proven	Auto cancellation, Notice standings, The earliest time limit decides the consequence
ONE-702.2	Proven	Notices at departure, No time limit, no consequence
ONE-702.3	Proven	No consequence before the time limits, Notice standings
ONE-702.4	Open	Notices at departure, Notices are resolved before departure

44.2. Guarantees🔗

44.2.1. The earliest time limit decides the consequence🔗

guarantee

Rules.OneOrder.AirlineChange.lapse_applies_earliest
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant) (f : Rules.OneOrder.AirlineChange.FollowUp)
  (hf : f ∈ n.followUps) (t : Rules.Core.Instant)
  (c : Rules.OneOrder.AirlineChange.Inaction)
  (hl : Rules.OneOrder.AirlineChange.FollowUp.lapse r f = some (t, c))
  (ht : t ≤ now) :
  ∃ g ∈ n.followUps,
    ∃ t' c',
      Rules.OneOrder.AirlineChange.FollowUp.lapse r g = some (t', c') ∧
        Rules.OneOrder.AirlineChange.consequenceAt r n now = some c' ∧
          ∀ h ∈ n.followUps,
            ∀ p ∈ Rules.OneOrder.AirlineChange.FollowUp.lapse r h,
              t' ≤ p.1
Rules.OneOrder.AirlineChange.lapse_applies_earliest
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant)
  (f :
    Rules.OneOrder.AirlineChange.FollowUp)
  (hf : f ∈ n.followUps)
  (t : Rules.Core.Instant)
  (c :
    Rules.OneOrder.AirlineChange.Inaction)
  (hl :
    Rules.OneOrder.AirlineChange.FollowUp.lapse
        r f =
      some (t, c))
  (ht : t ≤ now) :
  ∃ g ∈ n.followUps,
    ∃ t' c',
      Rules.OneOrder.AirlineChange.FollowUp.lapse
            r g =
          some (t', c') ∧
        Rules.OneOrder.AirlineChange.consequenceAt
              r n now =
            some c' ∧
          ∀ h ∈ n.followUps,
            ∀
              p ∈
                Rules.OneOrder.AirlineChange.FollowUp.lapse
                  r h,
              t' ≤ p.1

Once a time limit that carries a consequence of inaction has passed, a consequence applies: that of a follow-up action whose time limit is the earliest.

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

Checks acceptance criteria ONE-702.1.

44.2.2. No time limit, no consequence🔗

guarantee

Rules.OneOrder.AirlineChange.no_limit_no_consequence
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant)
  (h : ∀ f ∈ n.followUps, f.timeLimit = none) :
  Rules.OneOrder.AirlineChange.consequenceAt r n now = none
Rules.OneOrder.AirlineChange.no_limit_no_consequence
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant)
  (h :
    ∀ f ∈ n.followUps,
      f.timeLimit = none) :
  Rules.OneOrder.AirlineChange.consequenceAt
      r n now =
    none

A notice none of whose follow-up actions has a time limit never has a consequence of inaction applied, under every reading.

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

Checks acceptance criteria ONE-702.2.

44.2.3. No consequence before the time limits🔗

guarantee

Rules.OneOrder.AirlineChange.before_limits_no_consequence
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant)
  (h : ∀ f ∈ n.followUps, ∀ t ∈ f.timeLimit, now < t) :
  Rules.OneOrder.AirlineChange.consequenceAt r n now = none
Rules.OneOrder.AirlineChange.before_limits_no_consequence
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (now : Rules.Core.Instant)
  (h :
    ∀ f ∈ n.followUps,
      ∀ t ∈ f.timeLimit, now < t) :
  Rules.OneOrder.AirlineChange.consequenceAt
      r n now =
    none

Before every time limit of a notice, no consequence of inaction applies.

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

Checks acceptance criteria ONE-702.3.

44.2.4. Notices are resolved before departure🔗

guarantee

Rules.OneOrder.AirlineChange.resolved_before_departure
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (h : n.followUps ≠ []) :
  ∃ t < n.departure,
    (Rules.OneOrder.AirlineChange.consequenceAt r n t).isSome = true
Rules.OneOrder.AirlineChange.resolved_before_departure
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (h : n.followUps ≠ []) :
  ∃ t < n.departure,
    (Rules.OneOrder.AirlineChange.consequenceAt
          r n t).isSome =
      true

A notice that offers follow-up actions is resolved before the affected flight departs, even if the seller never answers.

Open question for the business. The sources make both the time limit and the consequence optional, and do not tie the time limit to the departure. A notice that offers Cancel with neither, like the guide's Cancel example, never lapses; a time limit set after the departure lapses too late. The example noticesAtDeparture shows both still unresolved when the flight departs. What applies when a follow-up action has no time limit or no consequence, and must the time limit fall before the affected flight departs?

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

Checks acceptance criteria ONE-702.4.

44.3. Examples🔗

44.3.1. Notice standings🔗

example

Rules.OneOrder.AirlineChange.noticeStandings :
  List Rules.OneOrder.AirlineChange.Standing
Rules.OneOrder.AirlineChange.noticeStandings :
  List
    Rules.OneOrder.AirlineChange.Standing

Given a notice that a departure moved by 10 minutes, with no follow-up action, and the itinerary change notice, which offers Accept, Cancel, Reshop and ContactAirline until 5 November 12:00 UTC with Auto-acceptance.

When each notice is looked at after what the seller did, under the reading that adds nothing to the sources.

Then the time change needs only acknowledgement. The itinerary change is pending a day before the time limit. A Cancel on 3 November answers it. A Cancel on 6 November comes after the time limit, and Auto-acceptance applies, as it does when the seller never answers.

What Lean computed:

Case	Checked	Standing
10-minute time change	2026-11-04 12:00 UTC	acknowledge only
itinerary change, no answer	2026-11-04 12:00 UTC	pending
itinerary change, Cancel on 3 November	2026-11-06 12:00 UTC	answered cancel
itinerary change, Cancel on 6 November	2026-11-06 12:00 UTC	lapsed auto accept
itinerary change, no answer	2026-11-06 12:00 UTC	lapsed auto accept

Checks acceptance criteria ONE-701.1, ONE-701.2, ONE-701.4, ONE-702.1, ONE-702.3.

44.3.2. Auto cancellation🔗

example

Rules.OneOrder.AirlineChange.autoCancellation :
  List Rules.OneOrder.AirlineChange.AutoCancelled
Rules.OneOrder.AirlineChange.autoCancellation :
  List
    Rules.OneOrder.AirlineChange.AutoCancelled

Given the same paid trip at 1,000.00 EUR that the airline moved, and a notice that offers Accept until 5 November 12:00 UTC with Auto-cancellation, the pairing the follow-up actions page shows.

When the seller misses the time limit, and the cancellation is priced on 6 November under the reading where the airline's fees apply.

Then Auto-cancellation applies, and the customer loses the trip the airline changed, pays the 50 EUR cancellation fee and gets 950 EUR back.

What Lean computed:

Standing	Penalty	Due by airline
lapsed auto cancel	50.00 EUR	950.00 EUR

Checks acceptance criteria ONE-702.1, ONE-703.1, ONE-703.4.

44.3.3. Notices at departure🔗

example

Rules.OneOrder.AirlineChange.noticesAtDeparture :
  List Rules.OneOrder.AirlineChange.AtDeparture
Rules.OneOrder.AirlineChange.noticesAtDeparture :
  List
    Rules.OneOrder.AirlineChange.AtDeparture

Given a notice that offers Cancel with neither a time limit nor a consequence, and a notice that offers Accept with Auto-acceptance and a time limit a day after the affected flight departs. The seller answers neither.

When the flight departs on 20 November 09:00 UTC.

Then no consequence of inaction applies to either notice under either reading, so both are still unresolved when the flight leaves. The first never lapses, even under the reading that applies Auto-acceptance when no consequence is stated, since it has no time limit.

What Lean computed:

Case	Literal	Filled
Cancel, no time limit or consequence	none	none
Accept, time limit after departure	none	none

Checks acceptance criteria ONE-702.2, ONE-702.4.

44.4. Open question🔗

The guarantee Notices are resolved before departure is open: the example Notices at departure shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.