14. Amounts due to and by the airline🔗

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

rule

Rules.OneOrder.Change.dueAmounts
  (r : Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote) :
  Rules.OneOrder.Change.DueAmounts
Rules.OneOrder.Change.dueAmounts
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (q :
    Rules.OneOrder.Change.ChangeQuote) :
  Rules.OneOrder.Change.DueAmounts

EARS: When a change or cancellation carries a penalty, the system shall either net the penalty against the price difference or charge it separately.

Story: As a customer, I want a penalty to cost me the same whether it is deducted from what I get back or charged on its own, so that the way the airline collects it does not change what I pay.

Acceptance criteria:

ONE-202.1: Where the penalty is netted, the system shall add the penalty charged to the price difference and state the result as a single amount, due either to or by the airline.
ONE-202.2: Where the penalty is charged separately, the system shall add the penalty charged to the amount due to the airline and settle the price difference on its own.
ONE-202.3: The system shall give the customer the same net amount whether the penalty is netted or charged separately.
ONE-202.4: If the penalty on a cancellation is larger than the refundable value of the cancelled items, then the system shall not leave the customer owing the airline money.

The price difference is the new price, less the old price, plus the forfeited amount. The worked examples fit this formula, though the guide does not state it. The penalty charged is the whole penalty, except when the penalty is larger than the refundable value: then it depends on the reading of the guide (ExcessPenalty).

14.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-202.1	Proven	Cancellation with forfeit, Change with collection, Netted penalty gives one amount
ONE-202.2	Proven	Separate penalty is added to the amount due, Penalty netted or separate
ONE-202.3	Proven	Penalty netted or separate, Penalty netted or charged separately
ONE-202.4	Open	Penalty above refund, Cancelling leaves the customer owing nothing

14.2. Guarantees🔗

14.2.1. Netted penalty gives one amount🔗

guarantee

Rules.OneOrder.Change.netted_single_amount
  (r : Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (h : q.handling = Rules.OneOrder.Change.PenaltyHandling.netted) :
  (Rules.OneOrder.Change.dueAmounts r q).net =
      q.difference + ↑(r.charged q) ∧
    ((Rules.OneOrder.Change.dueAmounts r q).toAirline = 0 ∨
      (Rules.OneOrder.Change.dueAmounts r q).byAirline = 0)
Rules.OneOrder.Change.netted_single_amount
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (h :
    q.handling =
      Rules.OneOrder.Change.PenaltyHandling.netted) :
  (Rules.OneOrder.Change.dueAmounts r
          q).net =
      q.difference + ↑(r.charged q) ∧
    ((Rules.OneOrder.Change.dueAmounts r
            q).toAirline =
        0 ∨
      (Rules.OneOrder.Change.dueAmounts r
            q).byAirline =
        0)

With a netted penalty, the due amounts net to the price difference plus the penalty charged, and at most one of them is above zero.

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

Checks acceptance criteria ONE-202.1.

14.2.2. Separate penalty is added to the amount due🔗

guarantee

Rules.OneOrder.Change.separate_penalty_added
  (r : Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (h : q.handling = Rules.OneOrder.Change.PenaltyHandling.separate) :
  (Rules.OneOrder.Change.dueAmounts r q).toAirline =
      r.charged q + q.difference.toNat ∧
    (Rules.OneOrder.Change.dueAmounts r q).byAirline =
      (-q.difference).toNat
Rules.OneOrder.Change.separate_penalty_added
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (h :
    q.handling =
      Rules.OneOrder.Change.PenaltyHandling.separate) :
  (Rules.OneOrder.Change.dueAmounts r
          q).toAirline =
      r.charged q + q.difference.toNat ∧
    (Rules.OneOrder.Change.dueAmounts r
          q).byAirline =
      (-q.difference).toNat

With a separate penalty, the amount due to the airline is the penalty charged plus any price difference the customer pays, and the amount due by the airline is any price difference the airline returns.

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

Checks acceptance criteria ONE-202.2.

14.2.3. Penalty netted or charged separately🔗

guarantee

Rules.OneOrder.Change.net_same_either_way
  (r : Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote) :
  (Rules.OneOrder.Change.dueAmounts r
        { oldPrice := q.oldPrice, newPrice := q.newPrice,
          penalty := q.penalty, forfeited := q.forfeited,
          handling := Rules.OneOrder.Change.PenaltyHandling.netted,
          settlement := q.settlement }).net =
    (Rules.OneOrder.Change.dueAmounts r
        { oldPrice := q.oldPrice, newPrice := q.newPrice,
          penalty := q.penalty, forfeited := q.forfeited,
          handling := Rules.OneOrder.Change.PenaltyHandling.separate,
          settlement := q.settlement }).net
Rules.OneOrder.Change.net_same_either_way
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (q :
    Rules.OneOrder.Change.ChangeQuote) :
  (Rules.OneOrder.Change.dueAmounts r
        { oldPrice := q.oldPrice,
          newPrice := q.newPrice,
          penalty := q.penalty,
          forfeited := q.forfeited,
          handling :=
            Rules.OneOrder.Change.PenaltyHandling.netted,
          settlement :=
            q.settlement }).net =
    (Rules.OneOrder.Change.dueAmounts r
        { oldPrice := q.oldPrice,
          newPrice := q.newPrice,
          penalty := q.penalty,
          forfeited := q.forfeited,
          handling :=
            Rules.OneOrder.Change.PenaltyHandling.separate,
          settlement :=
            q.settlement }).net

Netting the penalty or charging it separately gives the customer the same net amount, under both readings of the guide.

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

Checks acceptance criteria ONE-202.3.

14.2.4. Cancelling leaves the customer owing nothing🔗

guarantee

Rules.OneOrder.Change.cancel_not_owing
  (r : Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote) (hnew : q.newPrice.amount = 0)
  (hf : q.forfeited.amount ≤ q.oldPrice.amount) :
  (Rules.OneOrder.Change.dueAmounts r q).toAirline ≤
    (Rules.OneOrder.Change.dueAmounts r q).byAirline
Rules.OneOrder.Change.cancel_not_owing
  (r :
    Rules.OneOrder.Change.ExcessPenalty)
  (q : Rules.OneOrder.Change.ChangeQuote)
  (hnew : q.newPrice.amount = 0)
  (hf :
    q.forfeited.amount ≤
      q.oldPrice.amount) :
  (Rules.OneOrder.Change.dueAmounts r
        q).toAirline ≤
    (Rules.OneOrder.Change.dueAmounts r
        q).byAirline

A cancellation never leaves the customer owing the airline money: the amount due to the airline is no larger than the amount due by the airline, when the forfeited amount is part of the old price.

Open question for the business. Under the reading that collects the whole penalty, a penalty larger than the refundable value leaves the customer owing the difference. The example penaltyAboveRefund shows it: a 1,000.00 order with 20.00 forfeited and a 1,000.00 penalty leaves 20.00 due to the airline on a cancellation. Under the other reading the guarantee holds, but the due amounts no longer net to the formula of ONE-201.5. Is a penalty capped at the refundable value, or is the excess collected?

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

Checks acceptance criteria ONE-202.4.

14.3. Examples🔗

14.3.1. Change with collection🔗

example

Rules.OneOrder.Change.changeWithCollection :
  List Rules.OneOrder.Change.PricedCase
Rules.OneOrder.Change.changeWithCollection :
  List Rules.OneOrder.Change.PricedCase

Given a paid trip at 1,000.00 EUR, of which 120.00 EUR is forfeited, changed to a trip at 900.00 EUR with a penalty of 40.00 EUR netted. These are the figures of worked example EXM_ORD_003C.

When the airline prices the change.

Then the customer pays 60.00 EUR, the airline returns nothing, and the type code is AddCol, as in the worked example.

What Lean computed:

Case	Due to airline	Due by airline	Type
change to a cheaper trip	60.00 EUR	0.00 EUR	add col

Checks acceptance criteria ONE-201.2, ONE-202.1.

14.3.2. Penalty netted or separate🔗

example

Rules.OneOrder.Change.penaltyNettedOrSeparate :
  List Rules.OneOrder.Change.PricedCase
Rules.OneOrder.Change.penaltyNettedOrSeparate :
  List Rules.OneOrder.Change.PricedCase

Given a paid trip at 1,000.00 EUR changed to a trip at 840.00 EUR with a penalty of 60.00 EUR, where the airline keeps what it owes in a value store. The amounts due match worked example EXM_ORD_003G.

When the airline prices the change with the penalty netted, and again with the penalty charged separately.

Then netted, the customer pays nothing and 100.00 EUR goes to a value store. Charged separately, the customer pays 60.00 EUR and 160.00 EUR goes to a value store. Either way the customer is 100.00 EUR better off.

What Lean computed:

Case	Due to airline	Due by airline	Type
penalty netted	0.00 EUR	100.00 EUR	residual
penalty charged separately	60.00 EUR	160.00 EUR	add col and residual

Checks acceptance criteria ONE-201.2, ONE-201.3, ONE-202.2, ONE-202.3.

14.3.3. Cancellation with forfeit🔗

example

Rules.OneOrder.Change.cancellationWithForfeit :
  List Rules.OneOrder.Change.PricedCase
Rules.OneOrder.Change.cancellationWithForfeit :
  List Rules.OneOrder.Change.PricedCase

Given a paid order at 1,000.00 EUR, of which 20.00 EUR is forfeited, cancelled with a penalty of 50.00 EUR netted and a refund. These are the figures of worked example EXM_ORD_030B.

When the airline prices the cancellation.

Then the airline refunds 930.00 EUR and the type code is Refund, as in the worked example.

What Lean computed:

Case	Due to airline	Due by airline	Type
cancellation	0.00 EUR	930.00 EUR	refund

Checks acceptance criteria ONE-201.3, ONE-202.1.

14.3.4. Penalty above refund🔗

example

Rules.OneOrder.Change.penaltyAboveRefund :
  List Rules.OneOrder.Change.FormulaCase
Rules.OneOrder.Change.penaltyAboveRefund :
  List Rules.OneOrder.Change.FormulaCase

Given the cancellation of worked example EXM_ORD_030B (a paid order at 1,000.00 EUR with 20.00 EUR forfeited) with a penalty of 1,000.00 EUR netted in place of 50.00 EUR. The refundable value is 980.00 EUR, less than the penalty.

When the airline prices the cancellation under each reading of the guide.

Then under the reading that collects the whole penalty, the customer owes 20.00 EUR on a cancellation. Under the reading that waives the excess, nothing is due either way, while the formula of ONE-201.5 requires 20.00 EUR due to the airline.

What Lean computed:

Case	Due to airline	Due by airline	Type	Formula to airline	Formula by airline
collect the whole penalty	20.00 EUR	0.00 EUR	add col	20.00 EUR	0.00 EUR
waive the excess	0.00 EUR	0.00 EUR	even exchange	20.00 EUR	0.00 EUR

Checks acceptance criteria ONE-201.5, ONE-202.4.

14.4. Open question🔗

The guarantee Cancelling leaves the customer owing nothing is open: the example Penalty above refund shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.