52. Net position of a party🔗

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

rule

Rules.OneOrder.Accounting.settlementRole
  (r : Rules.OneOrder.Accounting.EasyPayReading)
  (cs : List Rules.OneOrder.Accounting.Clearance) (date : String)
  (p : Rules.OneOrder.Accounting.Party) :
  Rules.OneOrder.Accounting.SettlementRole
Rules.OneOrder.Accounting.settlementRole
  (r :
    Rules.OneOrder.Accounting.EasyPayReading)
  (cs :
    List
      Rules.OneOrder.Accounting.Clearance)
  (date : String)
  (p : Rules.OneOrder.Accounting.Party) :
  Rules.OneOrder.Accounting.SettlementRole

EARS: When the Clearance Manager nets the clearances for a remittance date, the system shall make each party a settlement payee or a remittance payer for its net position.

Story: As a Clearance Manager, I want each party's clearances netted into one amount per remittance date, so that each party makes or receives one transfer and the transfers balance.

Acceptance criteria:

ONE-805.1: When the Clearance Manager nets the clearances for a remittance date, the system shall give each party the amounts of the clearances it is paid less the amounts of those it is netted as payer of.
ONE-805.2: When a party's net position for a remittance date is positive, the system shall make it a settlement payee for that amount.
ONE-805.3: When a party's net position for a remittance date is negative, the system shall make it a remittance payer for that amount.
ONE-805.4: If a clearance is paid through EasyPay, then the system shall leave it out of the net position of its payer.
ONE-805.5: The system shall make the net positions of all parties for a remittance date sum to zero.

How an EasyPay clearance enters the netting is a reading of the sources (EasyPayReading). The model nets one currency.

52.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-805.1	Proven	Net position formula, Settlement plan netting
ONE-805.2	Proven	Settlement payees, Settlement plan netting
ONE-805.3	Proven	Settlement plan netting, Remittance payers
ONE-805.4	Proven	Easy pay netting, EasyPay out of the payer's position
ONE-805.5	Open	Easy pay netting, Net position per remittance date

52.2. Guarantees🔗

52.2.1. Net position formula🔗

guarantee

Rules.OneOrder.Accounting.net_position_formula
  (r : Rules.OneOrder.Accounting.EasyPayReading)
  (cs : List Rules.OneOrder.Accounting.Clearance) (date : String)
  (p : Rules.OneOrder.Accounting.Party) :
  Rules.OneOrder.Accounting.netPosition r cs date p =
    (List.map
          (fun c ↦
            if Rules.OneOrder.Accounting.Party.org c.payee = p then
              ↑c.amount
            else 0)
          (List.filter (fun x ↦ x.remittanceDate == date) cs)).sum -
      (List.map
          (fun c ↦
            if Rules.OneOrder.Accounting.netPayer r c = some p then
              ↑c.amount
            else 0)
          (List.filter (fun x ↦ x.remittanceDate == date) cs)).sum
Rules.OneOrder.Accounting.net_position_formula
  (r :
    Rules.OneOrder.Accounting.EasyPayReading)
  (cs :
    List
      Rules.OneOrder.Accounting.Clearance)
  (date : String)
  (p : Rules.OneOrder.Accounting.Party) :
  Rules.OneOrder.Accounting.netPosition r
      cs date p =
    (List.map
          (fun c ↦
            if
                Rules.OneOrder.Accounting.Party.org
                    c.payee =
                  p then
              ↑c.amount
            else 0)
          (List.filter
            (fun x ↦
              x.remittanceDate == date)
            cs)).sum -
      (List.map
          (fun c ↦
            if
                Rules.OneOrder.Accounting.netPayer
                    r c =
                  some p then
              ↑c.amount
            else 0)
          (List.filter
            (fun x ↦
              x.remittanceDate == date)
            cs)).sum

A party's net position is the amounts of the clearances on the remittance date that it is paid, less the amounts of those it is netted as payer of, under every reading.

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

Checks acceptance criteria ONE-805.1.

52.2.2. Settlement payees🔗

guarantee

Rules.OneOrder.Accounting.positive_position_payee
  (r : Rules.OneOrder.Accounting.EasyPayReading)
  (cs : List Rules.OneOrder.Accounting.Clearance) (date : String)
  (p : Rules.OneOrder.Accounting.Party)
  (h : 0 < Rules.OneOrder.Accounting.netPosition r cs date p) :
  Rules.OneOrder.Accounting.settlementRole r cs date p =
    Rules.OneOrder.Accounting.SettlementRole.settlementPayee
      (Rules.OneOrder.Accounting.netPosition r cs date p).toNat
Rules.OneOrder.Accounting.positive_position_payee
  (r :
    Rules.OneOrder.Accounting.EasyPayReading)
  (cs :
    List
      Rules.OneOrder.Accounting.Clearance)
  (date : String)
  (p : Rules.OneOrder.Accounting.Party)
  (h :
    0 <
      Rules.OneOrder.Accounting.netPosition
        r cs date p) :
  Rules.OneOrder.Accounting.settlementRole
      r cs date p =
    Rules.OneOrder.Accounting.SettlementRole.settlementPayee
      (Rules.OneOrder.Accounting.netPosition
          r cs date p).toNat

A party with a positive net position is a settlement payee for that amount, under every reading.

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

Checks acceptance criteria ONE-805.2.

52.2.3. Remittance payers🔗

guarantee

Rules.OneOrder.Accounting.negative_position_payer
  (r : Rules.OneOrder.Accounting.EasyPayReading)
  (cs : List Rules.OneOrder.Accounting.Clearance) (date : String)
  (p : Rules.OneOrder.Accounting.Party)
  (h : Rules.OneOrder.Accounting.netPosition r cs date p < 0) :
  Rules.OneOrder.Accounting.settlementRole r cs date p =
    Rules.OneOrder.Accounting.SettlementRole.remittancePayer
      (-Rules.OneOrder.Accounting.netPosition r cs date p).toNat
Rules.OneOrder.Accounting.negative_position_payer
  (r :
    Rules.OneOrder.Accounting.EasyPayReading)
  (cs :
    List
      Rules.OneOrder.Accounting.Clearance)
  (date : String)
  (p : Rules.OneOrder.Accounting.Party)
  (h :
    Rules.OneOrder.Accounting.netPosition
        r cs date p <
      0) :
  Rules.OneOrder.Accounting.settlementRole
      r cs date p =
    Rules.OneOrder.Accounting.SettlementRole.remittancePayer
      (-Rules.OneOrder.Accounting.netPosition
            r cs date p).toNat

A party with a negative net position is a remittance payer for that amount, under every reading.

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

Checks acceptance criteria ONE-805.3.

52.2.4. EasyPay out of the payer's position🔗

guarantee

Rules.OneOrder.Accounting.easyPay_left_out_of_payer
  (r : Rules.OneOrder.Accounting.EasyPayReading)
  (c : Rules.OneOrder.Accounting.Clearance)
  (hm : c.method = Rules.OneOrder.Accounting.ClearanceMethod.easyPay) :
  Rules.OneOrder.Accounting.Clearance.netFor r
      (Rules.OneOrder.Accounting.Party.org c.payer) c =
    if c.payee = c.payer then ↑c.amount else 0
Rules.OneOrder.Accounting.easyPay_left_out_of_payer
  (r :
    Rules.OneOrder.Accounting.EasyPayReading)
  (c :
    Rules.OneOrder.Accounting.Clearance)
  (hm :
    c.method =
      Rules.OneOrder.Accounting.ClearanceMethod.easyPay) :
  Rules.OneOrder.Accounting.Clearance.netFor
      r
      (Rules.OneOrder.Accounting.Party.org
        c.payer)
      c =
    if c.payee = c.payer then ↑c.amount
    else 0

An EasyPay clearance is never netted against its payer, under every reading: it adds to the payer's position only what it adds to the payer as its payee, which is nothing unless the payer is also the payee.

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

Checks acceptance criteria ONE-805.4.

52.2.5. Net position per remittance date🔗

guarantee

Rules.OneOrder.Accounting.net_positions_sum_zero
  (r : Rules.OneOrder.Accounting.EasyPayReading)
  (cs : List Rules.OneOrder.Accounting.Clearance) (date : String)
  (ps : List Rules.OneOrder.Accounting.Party) (hnd : ps.Nodup)
  (hcover :
    ∀ c ∈ cs,
      Rules.OneOrder.Accounting.Party.org c.payee ∈ ps ∧
        ∀ (q : Rules.OneOrder.Accounting.Party),
          Rules.OneOrder.Accounting.netPayer r c = some q → q ∈ ps) :
  (List.map (Rules.OneOrder.Accounting.netPosition r cs date) ps).sum =
    0
Rules.OneOrder.Accounting.net_positions_sum_zero
  (r :
    Rules.OneOrder.Accounting.EasyPayReading)
  (cs :
    List
      Rules.OneOrder.Accounting.Clearance)
  (date : String)
  (ps :
    List Rules.OneOrder.Accounting.Party)
  (hnd : ps.Nodup)
  (hcover :
    ∀ c ∈ cs,
      Rules.OneOrder.Accounting.Party.org
            c.payee ∈
          ps ∧
        ∀
          (q :
            Rules.OneOrder.Accounting.Party),
          Rules.OneOrder.Accounting.netPayer
                r c =
              some q →
            q ∈ ps) :
  (List.map
        (Rules.OneOrder.Accounting.netPosition
          r cs date)
        ps).sum =
    0

The net positions of all parties on a remittance date sum to zero.

Open question for the business. Under the reading that leaves an EasyPay clearance out of its payer's position and keeps it in the payee's, the positions add up to the EasyPay amounts. The example easyPayNetting shows it: a seller owing an airline 100.00 by settlement plan and 50.00 by EasyPay is a remittance payer for 100.00, while the airline is a settlement payee for 150.00. Does the EasyPay provider count as a party in the netting?

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

Checks acceptance criteria ONE-805.5.

52.3. Examples🔗

52.3.1. Settlement plan netting🔗

example

Rules.OneOrder.Accounting.settlementPlanNetting :
  Rules.OneOrder.Accounting.Netting
Rules.OneOrder.Accounting.settlementPlanNetting :
  Rules.OneOrder.Accounting.Netting

Given three settlement plan clearances due on 2026-11-16: seller S owes airline A 300.00 EUR and airline B 100.00 EUR, and A owes S a commission of 20.00 EUR.

When the Clearance Manager nets them.

Then S is a remittance payer for 380.00 EUR, A a settlement payee for 280.00 EUR and B a settlement payee for 100.00 EUR. The positions sum to zero.

What Lean computed:

Positions: org S, -38000, org A, 28000, org B, 10000
Roles: org S, remittance payer 38000, org A, settlement payee 28000, org B, settlement payee 10000
Sum: 0

Checks acceptance criteria ONE-805.1, ONE-805.2, ONE-805.3.

52.3.2. Easy pay netting🔗

example

Rules.OneOrder.Accounting.easyPayNetting :
  Rules.OneOrder.Accounting.EasyPayNetting
Rules.OneOrder.Accounting.easyPayNetting :
  Rules.OneOrder.Accounting.EasyPayNetting

Given a seller S that owes airline A 100.00 EUR through a settlement plan and 50.00 EUR through EasyPay, both due on 2026-11-16.

When the Clearance Manager nets them.

Then S is a remittance payer for 100.00 EUR and A a settlement payee for 150.00 EUR under both readings. Where EasyPay is only left out of the payer's position, the positions sum to 50.00 EUR. Where the EasyPay provider takes the payer's place, it is a remittance payer for 50.00 EUR and the positions sum to zero.

What Lean computed:

Left out: positions org S, -10000, org A, 15000, easy pay provider, 0, roles org S, remittance payer 10000, org A, settlement payee 15000, easy pay provider, even, sum 5000
Provider pays: positions org S, -10000, org A, 15000, easy pay provider, -5000, roles org S, remittance payer 10000, org A, settlement payee 15000, easy pay provider, remittance payer 5000, sum 0

Checks acceptance criteria ONE-805.4, ONE-805.5.

52.4. Open question🔗

The guarantee Net position per remittance date is open: the example Easy pay netting shows the rule as written breaking it. Questions from the ONE Order rules sets out the question for the team.