Atanasov--Ranganathan's sixth configuration, generic in the core

This is the sixth local picture of Atanasov--Ranganathan, Proposition 5.1 (fig:configurations-for-genus-5, the scope commented %Sixth):

   a       b            a, b, d, f carry the four chips
    \     /             c, e are chip free
      \ /
       c
       |                c -- d  is the middle slot
       d
      / \                d == e is a banana (two parallel slots)
      \ /
       e
       |                e -- f  is the tail slot
       f

Note on the file name: the AR numbering is not available here, because ConfigurationThreeChain.lean in this directory is the chip-free three-chain, which is not one of AR's eleven pictures at all. This file is named after the geometry instead -- the centre sits at the far end of a banana whose near end carries a chip -- and the docstrings say which AR picture is meant.

Relation to ConfigurationFive. Configuration 5 is drawn on the same underlying graph, with the chips moved: there e carries a chip and d is chip free, so the banana runs from a chip-free vertex into a chip. Here it runs from the chip at d out to the chip-free e, which is what makes the picture genuinely different: d must give away one chip along each of the two parallel slots, so it has to be refilled along c -- d, and c in turn along its two arms.

Only the e-centre profile is proved here. On row 14 the other chip-free vertex c of the picture happens to be a configuration-2 tripod as well (all three of its slots end on chips), so it is covered by ConfigurationTwo and the c-centre profile is never needed. Should a later row need it, it goes next to center_nonneg below.

The profile. Write m = min |ca| |cb| and pq = min |de₁| |de₂|, and put the chips a, b, f and everything off the picture at height 0:

E = min |ef| (m + |cd| + pq)      -- height at the centre e
D = min E (m + |cd|)              -- height at the chip d
C = min D m                       -- height at the chip-free c

Three nested minima of slot lengths, so every height collapses along with any slot it spans and the same script works on every nonloopy forest face.

The shift. When |cd| collapses, c and d are one class, and d's two outgoing banana chips have to be paid for by c's two arms. The row's chip bookkeeping therefore carries one conditional transfer c ⟶ d, guarded by |cd| = 0 ∧ D < E; it appears below as the parameter shift. With it the target owner has only two branches: the centre e, except when a banana slot collapses and the tail slot is too long to reach, where the chip sits on d.

The one-edge arithmetic is ConfigurationFive's, reused unchanged, and the orientation ledger extends ConfigurationThreeChain.ChainLedger by the one fact the proofs below need that it does not carry.

The orientation ledger

structure AtanasovRanganathan.ConfigurationBananaTail.BananaLedgerextends AtanasovRanganathan.ConfigurationThreeChain.ChainLedger : Type

A ChainLedger that also knows when the far end of a full slot receives the chip. tail L hu hv is the contribution at the end carrying height hu, head L hu hv the contribution at the end carrying hv.

• tail : ℕ → ℕ → ℕ → ℤ
• head : ℕ → ℕ → ℕ → ℤ
• tail_same (L h : ℕ) : self.tail L h h = 0
• head_same (L h : ℕ) : self.head L h h = 0
• tail_nonneg {L hu hv : ℕ} : hv ≤ hu → hu ≤ hv + L → 0 ≤ self.tail L hu hv
• head_nonneg {L hu hv : ℕ} : hu ≤ hv → hv ≤ hu + L → 0 ≤ self.head L hu hv
• tail_ge_neg_one {L hu hv : ℕ} : hv ≤ hu + L → hu ≤ hv + L → -1 ≤ self.tail L hu hv
• head_ge_neg_one {L hu hv : ℕ} : hv ≤ hu + L → hu ≤ hv + L → -1 ≤ self.head L hu hv
• tail_eq_one_of_full {L hu hv : ℕ} : 0 < L → hu = hv + L → self.tail L hu hv = 1
• head_eq_one_of_full {L hu hv : ℕ} : 0 < L → hv = hu + L → self.head L hu hv = 1

def AtanasovRanganathan.ConfigurationBananaTail.fwd : BananaLedger

The slot read from its core tail.

Equations

• AtanasovRanganathan.ConfigurationBananaTail.fwd = { toChainLedger := AtanasovRanganathan.ConfigurationThreeChain.forward, head_eq_one_of_full := ⋯ }

def AtanasovRanganathan.ConfigurationBananaTail.rev : BananaLedger

The same slot read from its core head.

Equations

• AtanasovRanganathan.ConfigurationBananaTail.rev = { toChainLedger := AtanasovRanganathan.ConfigurationThreeChain.reverse, head_eq_one_of_full := ⋯ }

The chip leaves

a, b and f each give away at most the single chip they carry.

theorem AtanasovRanganathan.ConfigurationBananaTail.leaf_nonneg (S : BananaLedger) {L hu hv : ℕ} (h1 : hv ≤ hu) (h2 : hu ≤ hv + L) : 0 ≤ ConfigurationFive.positiveChip L + S.head L hu hv

Residual effectivity at a chip leaf of the picture.

The chip-free arm vertex c

theorem AtanasovRanganathan.ConfigurationBananaTail.armCenter_nonneg (Sa Sb Sw : BananaLedger) {la lb w p q u m pq C D E : ℕ} (shift : ℤ) (hm : m = min la lb) (hpq : pq = min p q) (hE : E = min u (m + w + pq)) (hD : D = min E (m + w)) (hC : C = min D m) (hshift : shift = if w = 0 ∧ D < E then 1 else 0) : 0 ≤ ConfigurationFive.zeroChip la + ConfigurationFive.zeroChip lb - shift + (Sa.tail la C 0 + Sb.tail lb C 0 + Sw.tail w C D)

Residual effectivity at the chip-free vertex c, which feeds the chip at d along the middle slot and is refilled by its two arms.

The chip at the near end of the banana

theorem AtanasovRanganathan.ConfigurationBananaTail.bananaChip_nonneg (Sw Sp Sq : BananaLedger) {la lb w p q u m pq C D E : ℕ} (shift k : ℤ) (hm : m = min la lb) (hpq : pq = min p q) (hE : E = min u (m + w + pq)) (hD : D = min E (m + w)) (hC : C = min D m) (hshift : shift = if w = 0 ∧ D < E then 1 else 0) (hk : k ≤ 1) (hkOwner : 1 ≤ k → pq = 0) : 0 ≤ 1 + shift - k + (Sw.head w C D + Sp.tail p D E + Sq.tail q D E)

Residual effectivity at the chip d. It gives away one chip along each of the two parallel slots and is refilled either along the middle slot or, if that slot has collapsed, by the shift.

The centre

theorem AtanasovRanganathan.ConfigurationBananaTail.center_nonneg (Sp Sq Su : BananaLedger) {la lb w p q u m pq C D E : ℕ} (k : ℤ) (hm : m = min la lb) (hpq : pq = min p q) (hE : E = min u (m + w + pq)) (hD : D = min E (m + w)) (_hC : C = min D m) (hk : k ≤ 1) (hkOwner : 1 ≤ k → ¬(pq = 0 ∧ m + w < u)) : 0 ≤ ConfigurationFive.zeroChip u - k + (Sp.head p D E + Sq.head q D E + Su.tail u E 0)

Residual effectivity at the centre e, the chip-free far end of the banana.