43. Answering a change notice🔗

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

rule

Rules.OneOrder.AirlineChange.resolve
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts : List Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant) : Rules.OneOrder.AirlineChange.Resolution
Rules.OneOrder.AirlineChange.resolve
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts :
    List
      Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant) :
  Rules.OneOrder.AirlineChange.Resolution

EARS: When an airline change notice offers follow-up actions, the system shall keep them pending until the seller answers with one of them or a consequence of inaction applies.

Story: As a seller, I want each change notice to show whether it waits for me, what I answered, or what the airline did when I did not answer, so that I can tell the customer where their trip stands.

Acceptance criteria:

ONE-701.1: When an airline change notice carries no follow-up action, the system shall ask the seller only to acknowledge it.
ONE-701.2: When the seller performs an offered Accept, Reshop, Cancel or RepriceAndAccept action before any consequence of inaction applies, the system shall resolve the notice with the seller's answer.
ONE-701.3: The system shall resolve a notice with an answer only when the seller took that action, the notice offers it, and the seller took it before any consequence of inaction applied.
ONE-701.4: While the seller has not answered a notice that offers follow-up actions, the system shall keep it pending until a consequence of inaction applies, and then resolve it with that consequence.
ONE-701.5: When the seller contacts the airline about a notice that offers ContactAirline before any consequence of inaction applies, the system shall apply no consequence of inaction.

The seller's acts are listed in the order they happened; the first act that answers the notice resolves it, and answering one follow-up action resolves them all. Whether contacting the airline counts as an answer is the reading's (FollowUpReading).

43.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-701.1	Proven	A notice without follow-up actions needs only acknowledgement, Notice standings
ONE-701.2	Proven	An offered action answers the notice, Notice standings
ONE-701.3	Proven	Answers are offered actions taken in time
ONE-701.4	Proven	Unanswered notices stay pending until they lapse, Notice standings
ONE-701.5	Open	Contact then auto accept, Pending follow-up actions

43.2. Guarantees🔗

43.2.1. A notice without follow-up actions needs only acknowledgement🔗

guarantee

Rules.OneOrder.AirlineChange.resolve_acknowledge_only
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts : List Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant) (h : n.followUps = []) :
  Rules.OneOrder.AirlineChange.resolve r n acts now =
    Rules.OneOrder.AirlineChange.Resolution.acknowledgeOnly
Rules.OneOrder.AirlineChange.resolve_acknowledge_only
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts :
    List
      Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (h : n.followUps = []) :
  Rules.OneOrder.AirlineChange.resolve r n
      acts now =
    Rules.OneOrder.AirlineChange.Resolution.acknowledgeOnly

A notice with no follow-up action needs only acknowledgement.

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

Checks acceptance criteria ONE-701.1.

43.2.2. An offered action answers the notice🔗

guarantee

Rules.OneOrder.AirlineChange.resolve_answers
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts : List Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (a : Rules.OneOrder.AirlineChange.SellerAct) (ha : a ∈ acts)
  (hoff : n.offers a.action = true)
  (hkind :
    a.action ≠
      Rules.OneOrder.AirlineChange.FollowUpAction.contactAirline)
  (hnow : a.time ≤ now)
  (hbefore :
    Rules.OneOrder.AirlineChange.consequenceAt r n a.time = none) :
  ∃ b ∈ acts,
    Rules.OneOrder.AirlineChange.resolve r n acts now =
      Rules.OneOrder.AirlineChange.Resolution.answered b.action
Rules.OneOrder.AirlineChange.resolve_answers
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts :
    List
      Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (a :
    Rules.OneOrder.AirlineChange.SellerAct)
  (ha : a ∈ acts)
  (hoff : n.offers a.action = true)
  (hkind :
    a.action ≠
      Rules.OneOrder.AirlineChange.FollowUpAction.contactAirline)
  (hnow : a.time ≤ now)
  (hbefore :
    Rules.OneOrder.AirlineChange.consequenceAt
        r n a.time =
      none) :
  ∃ b ∈ acts,
    Rules.OneOrder.AirlineChange.resolve r
        n acts now =
      Rules.OneOrder.AirlineChange.Resolution.answered
        b.action

When the seller takes an offered action other than contacting the airline, before any consequence of inaction applies, the notice is resolved with one of the seller's acts, under every reading.

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

Checks acceptance criteria ONE-701.2.

43.2.3. Answers are offered actions taken in time🔗

guarantee

Rules.OneOrder.AirlineChange.resolve_answered_sound
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts : List Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (x : Rules.OneOrder.AirlineChange.FollowUpAction)
  (h :
    Rules.OneOrder.AirlineChange.resolve r n acts now =
      Rules.OneOrder.AirlineChange.Resolution.answered x) :
  ∃ a ∈ acts,
    a.action = x ∧
      n.offers x = true ∧
        a.time ≤ now ∧
          Rules.OneOrder.AirlineChange.consequenceAt r n a.time = none
Rules.OneOrder.AirlineChange.resolve_answered_sound
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts :
    List
      Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (x :
    Rules.OneOrder.AirlineChange.FollowUpAction)
  (h :
    Rules.OneOrder.AirlineChange.resolve r
        n acts now =
      Rules.OneOrder.AirlineChange.Resolution.answered
        x) :
  ∃ a ∈ acts,
    a.action = x ∧
      n.offers x = true ∧
        a.time ≤ now ∧
          Rules.OneOrder.AirlineChange.consequenceAt
              r n a.time =
            none

A notice is resolved with an answer only when the seller took that action, the notice offers it, and the seller took it before any consequence of inaction applied.

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

Checks acceptance criteria ONE-701.3.

43.2.4. Unanswered notices stay pending until they lapse🔗

guarantee

Rules.OneOrder.AirlineChange.resolve_unanswered
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts : List Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant) (hne : n.followUps ≠ [])
  (h :
    ∀ a ∈ acts,
      Rules.OneOrder.AirlineChange.ChangeNotice.answeredBy r n now a =
        false) :
  (Rules.OneOrder.AirlineChange.consequenceAt r n now = none →
      Rules.OneOrder.AirlineChange.resolve r n acts now =
        Rules.OneOrder.AirlineChange.Resolution.pending) ∧
    ∀ (c : Rules.OneOrder.AirlineChange.Inaction),
      Rules.OneOrder.AirlineChange.consequenceAt r n now = some c →
        Rules.OneOrder.AirlineChange.resolve r n acts now =
          Rules.OneOrder.AirlineChange.Resolution.lapsed c
Rules.OneOrder.AirlineChange.resolve_unanswered
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts :
    List
      Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (hne : n.followUps ≠ [])
  (h :
    ∀ a ∈ acts,
      Rules.OneOrder.AirlineChange.ChangeNotice.answeredBy
          r n now a =
        false) :
  (Rules.OneOrder.AirlineChange.consequenceAt
          r n now =
        none →
      Rules.OneOrder.AirlineChange.resolve
          r n acts now =
        Rules.OneOrder.AirlineChange.Resolution.pending) ∧
    ∀
      (c :
        Rules.OneOrder.AirlineChange.Inaction),
      Rules.OneOrder.AirlineChange.consequenceAt
            r n now =
          some c →
        Rules.OneOrder.AirlineChange.resolve
            r n acts now =
          Rules.OneOrder.AirlineChange.Resolution.lapsed
            c

While no act of the seller answers a notice that offers follow-up actions, the notice is pending until a consequence of inaction applies, and then it is resolved with that consequence.

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

Checks acceptance criteria ONE-701.4.

43.2.5. Pending follow-up actions🔗

guarantee

Rules.OneOrder.AirlineChange.contact_airline_answers
  (r : Rules.OneOrder.AirlineChange.FollowUpReading)
  (n : Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts : List Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (a : Rules.OneOrder.AirlineChange.SellerAct) (ha : a ∈ acts)
  (hact :
    a.action =
      Rules.OneOrder.AirlineChange.FollowUpAction.contactAirline)
  (hoff :
    n.offers
        Rules.OneOrder.AirlineChange.FollowUpAction.contactAirline =
      true)
  (hnow : a.time ≤ now)
  (hbefore :
    Rules.OneOrder.AirlineChange.consequenceAt r n a.time = none)
  (c : Rules.OneOrder.AirlineChange.Inaction) :
  Rules.OneOrder.AirlineChange.resolve r n acts now ≠
    Rules.OneOrder.AirlineChange.Resolution.lapsed c
Rules.OneOrder.AirlineChange.contact_airline_answers
  (r :
    Rules.OneOrder.AirlineChange.FollowUpReading)
  (n :
    Rules.OneOrder.AirlineChange.ChangeNotice)
  (acts :
    List
      Rules.OneOrder.AirlineChange.SellerAct)
  (now : Rules.Core.Instant)
  (a :
    Rules.OneOrder.AirlineChange.SellerAct)
  (ha : a ∈ acts)
  (hact :
    a.action =
      Rules.OneOrder.AirlineChange.FollowUpAction.contactAirline)
  (hoff :
    n.offers
        Rules.OneOrder.AirlineChange.FollowUpAction.contactAirline =
      true)
  (hnow : a.time ≤ now)
  (hbefore :
    Rules.OneOrder.AirlineChange.consequenceAt
        r n a.time =
      none)
  (c :
    Rules.OneOrder.AirlineChange.Inaction) :
  Rules.OneOrder.AirlineChange.resolve r n
      acts now ≠
    Rules.OneOrder.AirlineChange.Resolution.lapsed
      c

When the seller contacts the airline about a notice that offers ContactAirline, before any consequence of inaction applies, no consequence of inaction is applied.

Open question for the business. Contacting the airline happens outside the order, and the sources do not say whether the order records it or whether it clears the other pending actions. Under a reading where it is not recorded, a seller who phones the airline before the time limit still sees Auto-acceptance applied when the limit passes. The example contactThenAutoAccept shows it. Does contacting the airline count as an answer, and does it stop the time limit?

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

Checks acceptance criteria ONE-701.5.

43.3. Examples🔗

43.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.

43.3.2. Contact then auto accept🔗

example

Rules.OneOrder.AirlineChange.contactThenAutoAccept :
  List Rules.OneOrder.AirlineChange.ReadingStanding
Rules.OneOrder.AirlineChange.contactThenAutoAccept :
  List
    Rules.OneOrder.AirlineChange.ReadingStanding

Given the itinerary change notice, which offers ContactAirline among its follow-up actions until 5 November 12:00 UTC with Auto-acceptance. The seller phones the airline on 3 November, two days before the time limit.

When the notice is looked at on 6 November, under each reading.

Then where the order does not record contacting the airline, Auto-acceptance applies although the seller acted in time. Where it records it, the notice is answered with ContactAirline.

What Lean computed:

Reading	Standing
contacting the airline is not recorded	lapsed auto accept
contacting the airline is recorded	answered contact airline

Checks acceptance criteria ONE-701.5.

43.4. Open question🔗

The guarantee Pending follow-up actions is open: the example Contact then auto accept shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.