The chipped triangle

This is the solid subgraph of Atanasov--Ranganathan's second scope for their seventh genus-five family (atlas row 08). It is not one of the eleven pictures of their Proposition 5.1: the closest, the Eighth, is a triangle with three chip arms too, but its triangle is chip free and it carries the extra hypothesis that one arm has length min of the other two, which row 08's second chamber does not supply. The module is therefore named for its geometry, following the ConfigurationThreeChain / ConfigurationBananaTail / ConfigurationBananaDoubleChip precedent.

        A            B           A, B, C each carry a chip
        |            |           c carries a chip as well
        u ==== q ====v           u, v are chip free
         \          /            |c u| = p, |u v| = q, |c v| = r
          p        r             |u A| = al, |v B| = be, |c C| = ga
            \    /
              c
              |
              C

Four chips in all: one on c, one at the end of each of the three arms. The target is u; the picture is read a second time at v by swapping u ↔ v, al ↔ be, p ↔ r. The profile is four nested minima,

 hc = min ga (min al be)                        -- the chipped vertex
 h0 = min be (hc + r)                           -- the partner, before clamping
 ht = min al (min (hc + p) (h0 + q))            -- the target
 hv = min h0 ht                                 -- the partner

The three ways u gets its chip are the three arguments of ht: its own arm goes full, or the triangle slot from c goes full and c refills along ga, or the triangle slot from v goes full.

The final clamp hv = min h0 ht ensures that the partner does not rise above the target; this is used in the slot-ledger inequalities below.

One chip moves inside a contracted class. When the triangle slot c - v collapses (r = 0) and c sits strictly above the partner's arm (hc < be), the partner has to pay one unit across q that neither its own arm nor the collapsed slot can supply; c and v are then the same contracted class, so c lends it the chip it is sitting on. That transfer is lend, and it is the only allocation the picture needs.

The four nested minima

def AtanasovRanganathan.ConfigurationChippedTriangle.chipHeight (al be ga : ℕ) : ℕ

The height at the chipped triangle vertex c.

Equations

• AtanasovRanganathan.ConfigurationChippedTriangle.chipHeight al be ga = min ga (min al be)

def AtanasovRanganathan.ConfigurationChippedTriangle.sideHeight (al be ga r : ℕ) : ℕ

The partner's height before the final clamp.

Equations

• AtanasovRanganathan.ConfigurationChippedTriangle.sideHeight al be ga r = min be (AtanasovRanganathan.ConfigurationChippedTriangle.chipHeight al be ga + r)

def AtanasovRanganathan.ConfigurationChippedTriangle.targetHeight (al be ga p q r : ℕ) : ℕ

The height at the target u.

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.ConfigurationChippedTriangle.partnerHeight (al be ga p q r : ℕ) : ℕ

The height at the partner v, clamped so that v is never deeper than the target -- without this clamp the picture breaks (see the module docstring).

Equations

• One or more equations did not get rendered due to their size.

def AtanasovRanganathan.ConfigurationChippedTriangle.lend (r hc be : ℕ) : ℤ

The chip c lends its partner when the slot between them has collapsed and c is strictly shallower than the partner's own arm.

Equations

• AtanasovRanganathan.ConfigurationChippedTriangle.lend r hc be = if r = 0 ∧ hc < be then 1 else 0

theorem AtanasovRanganathan.ConfigurationChippedTriangle.lend_nonneg (r hc be : ℕ) : 0 ≤ lend r hc be

theorem AtanasovRanganathan.ConfigurationChippedTriangle.lend_eq_one {r hc be : ℕ} (hr : r = 0) (hlt : hc < be) : lend r hc be = 1

theorem AtanasovRanganathan.ConfigurationChippedTriangle.lend_cases (r hc be : ℕ) : lend r hc be = 0 ∨ lend r hc be = 1

theorem AtanasovRanganathan.ConfigurationChippedTriangle.eq_of_lend_eq_one {r hc be : ℕ} (h : lend r hc be = 1) : r = 0 ∧ hc < be

The arithmetic of the four minima

Everything the three residual statements need about the profile is this one bundle of inequalities and "which argument is attained" disjunctions; each consumer then works with plain naturals and omega.

theorem AtanasovRanganathan.ConfigurationChippedTriangle.bounds {al be ga p q r hc h0 ht hv : ℕ} (hhc : hc = chipHeight al be ga) (hh0 : h0 = sideHeight al be ga r) (hht : ht = targetHeight al be ga p q r) (hhv : hv = partnerHeight al be ga p q r) : (hc ≤ ga ∧ hc ≤ al ∧ hc ≤ be) ∧ (hc = ga ∨ hc = al ∨ hc = be) ∧ (h0 ≤ be ∧ h0 ≤ hc + r ∧ hc ≤ h0) ∧ (h0 = be ∨ h0 = hc + r) ∧ (ht ≤ al ∧ ht ≤ hc + p ∧ ht ≤ h0 + q ∧ hc ≤ ht) ∧ (ht = al ∨ ht = hc + p ∨ ht = h0 + q) ∧ (hv ≤ h0 ∧ hv ≤ ht ∧ hc ≤ hv ∧ ht ≤ hv + q ∧ hv ≤ hc + r ∧ hv ≤ be) ∧ (hv = h0 ∨ hv = ht)

Who owns the delivered chip

def AtanasovRanganathan.ConfigurationChippedTriangle.Delivers (al p q hc h0 ht : ℕ) : Prop

The target delivers its own chip: its arm goes full, or one of the two triangle slots at it goes full.

Equations

• AtanasovRanganathan.ConfigurationChippedTriangle.Delivers al p q hc h0 ht = (ht = al ∨ 0 < p ∧ ht = hc + p ∨ 0 < q ∧ ht = h0 + q)

@[instance_reducible]

instance AtanasovRanganathan.ConfigurationChippedTriangle.instDecidableDelivers (al p q hc h0 ht : ℕ) : Decidable (Delivers al p q hc h0 ht)

Equations

• AtanasovRanganathan.ConfigurationChippedTriangle.instDecidableDelivers al p q hc h0 ht = id inferInstance

def AtanasovRanganathan.ConfigurationChippedTriangle.PartnerOwns (be p q r hc h0 ht : ℕ) : Prop

The partner can be charged instead. Both disjuncts force hv = ht, so the partner never pays across q in this situation.

Equations

• AtanasovRanganathan.ConfigurationChippedTriangle.PartnerOwns be p q r hc h0 ht = (q = 0 ∧ ht = h0 ∨ p = 0 ∧ r = 0 ∧ hc < be)

theorem AtanasovRanganathan.ConfigurationChippedTriangle.cases_of_not_delivers {al be ga p q r hc h0 ht hv : ℕ} (hhc : hc = chipHeight al be ga) (hh0 : h0 = sideHeight al be ga r) (hht : ht = targetHeight al be ga p q r) (hhv : hv = partnerHeight al be ga p q r) (h : ¬Delivers al p q hc h0 ht) : p = 0 ∧ ht = hc ∨ q = 0 ∧ ht = h0

When the target does not deliver, one of the two triangle slots at it has collapsed -- which is what puts the fallback owner in the target's class.

theorem AtanasovRanganathan.ConfigurationChippedTriangle.partnerOwns_of_not_delivers {al be ga p q r hc h0 ht hv : ℕ} (hhc : hc = chipHeight al be ga) (hh0 : h0 = sideHeight al be ga r) (hht : ht = targetHeight al be ga p q r) (hhv : hv = partnerHeight al be ga p q r) (h : ¬Delivers al p q hc h0 ht) (h2 : ¬(p = 0 ∧ lend r hc be = 0)) : PartnerOwns be p q r hc h0 ht

theorem AtanasovRanganathan.ConfigurationChippedTriangle.class_of_not_delivers {al be ga p q r hc h0 ht hv : ℕ} (hhc : hc = chipHeight al be ga) (hh0 : h0 = sideHeight al be ga r) (hht : ht = targetHeight al be ga p q r) (hhv : hv = partnerHeight al be ga p q r) (h : ¬Delivers al p q hc h0 ht) (h2 : ¬(p = 0 ∧ lend r hc be = 0)) : q = 0 ∨ p = 0 ∧ r = 0

The fallback owner is in the target's contracted class: either the slot to the partner has collapsed, or both slots at the chipped vertex have.

The three residual statements

Each arm and each triangle slot may be a whole slot read from either end or the half of a marked slot, so all six are read through a PairLedger, exactly as in ConfigurationMarkedThree. S.tail L x y is the contribution at the end carrying height x.

theorem AtanasovRanganathan.ConfigurationChippedTriangle.triangleTarget_nonneg (SA SP SQ : ConfigurationMarkedThree.PairLedger) {al be ga p q r hc h0 ht hv : ℕ} {k : ℤ} (hhc : hc = chipHeight al be ga) (hh0 : h0 = sideHeight al be ga r) (hht : ht = targetHeight al be ga p q r) (hhv : hv = partnerHeight al be ga p q r) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hk : k = 1 → Delivers al p q hc h0 ht) : 0 ≤ ConfigurationFive.zeroChip al - k + (SA.tail al ht 0 + SP.tail p ht hc + SQ.tail q ht hv)

The target. k is one exactly when the delivered chip is charged here.

theorem AtanasovRanganathan.ConfigurationChippedTriangle.trianglePartner_nonneg (SB SR SQ : ConfigurationMarkedThree.PairLedger) {al be ga p q r hc h0 ht hv : ℕ} {k : ℤ} (hhc : hc = chipHeight al be ga) (hh0 : h0 = sideHeight al be ga r) (hht : ht = targetHeight al be ga p q r) (hhv : hv = partnerHeight al be ga p q r) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hk : k = 1 → PartnerOwns be p q r hc h0 ht) : 0 ≤ ConfigurationFive.zeroChip be + lend r hc be - k + (SB.tail be hv 0 + SR.tail r hv hc + SQ.tail q hv ht)

The partner. It pays across q only when its own arm or the slot to the chipped vertex is full, or when c lends it the chip it sits on.

theorem AtanasovRanganathan.ConfigurationChippedTriangle.triangleChipped_nonneg (SG SP SR : ConfigurationMarkedThree.PairLedger) {al be ga p q r hc h0 ht hv : ℕ} {k : ℤ} (hhc : hc = chipHeight al be ga) (hh0 : h0 = sideHeight al be ga r) (hht : ht = targetHeight al be ga p q r) (hhv : hv = partnerHeight al be ga p q r) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hk : k = 1 → p = 0 ∧ lend r hc be = 0) : 0 ≤ 1 + ConfigurationFive.zeroChip ga - lend r hc be - k + (SG.tail ga hc 0 + SP.tail p hc ht + SR.tail r hc hv)

The chipped vertex. It always has the slack of the chip it carries, so it can absorb both triangle slots running full away from it -- and when they both do, its own arm is full as well.