A banana pair with a double chip at the short end

This is the solid subgraph of Atanasov--Ranganathan's third 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 Fourth, puts its single chip on a banana vertex rather than at the end of a leg. The module is therefore named for its geometry, following the ConfigurationThreeChain / ConfigurationBananaTail precedent.

      A                B          A carries one chip, B carries TWO
      |                |          u, v are chip free, joined by a banana
      u ===== v                   |u A| = p,  |v B| = q,  q ≤ p

The pair is lopsided -- the arms have different lengths -- and the target is the far vertex u, the one whose arm is the long one. With par = min m1 m2 the profile is the two nested minima

 hv = min (2 * q) p
 hu = min p (hv + par)

and only the double chip makes it possible: with a single chip at B the far vertex of a lopsided banana pair is unreachable by any script of this shape, because the arm v B can then carry at most one unit of slope while the two banana slots charge v twice.

Three ways u gets its chip, which are the three arguments of the two minima:

• hu = p -- the arm u A is full and delivers;
• hu = hv + par with par > 0 -- the shorter banana slot is full and delivers, and v pays the two banana chips out of the two it drew along q;
• par = 0 -- the banana has collapsed, u and v are the same contracted class, and the chip is charged to v (or, when q = 0 as well, to B itself). That is the k parameter below.

The near vertex is where the double chip is spent: far_partner_nonneg is the statement that v still balances, and its proof is the only place in the whole programme where a canonical ramp runs at slope two -- headContribution q 0 (2 * q) = 2. The four one-edge facts that needs are proved first.

One-edge arithmetic at slope two

ConfigurationFive's ledger bounds every endpoint slope by one in absolute value, which is right for a divisor with one chip per arm end. The double chip allows -- and needs -- slope two on its own arm.

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.headContribution_ge_one_of_ge {L h : ℕ} (hL : 0 < L) (hle : L ≤ h) : 1 ≤ ConfigurationFive.headContribution L 0 h

An arm read from its head delivers a chip as soon as its rise reaches the arm's length.

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.headContribution_ge_two_of_ge {L h : ℕ} (hL : 0 < L) (hle : 2 * L ≤ h) : 2 ≤ ConfigurationFive.headContribution L 0 h

Slope two. An arm whose rise is twice its length delivers two chips at its head. This is what the double chip buys.

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.tailContribution_ge_neg_two {L h : ℕ} (hh : h ≤ 2 * L) : -2 ≤ ConfigurationFive.tailContribution L 0 h

The matching cost: an arm of rise at most twice its length takes at most two chips from its tail.

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.doubleChip_add_tail_nonneg {L h : ℕ} (hh : h ≤ 2 * L) : 0 ≤ 2 * ConfigurationFive.positiveChip L + ConfigurationFive.tailContribution L 0 h

The double chip pays for its own arm.

The profile

def AtanasovRanganathan.ConfigurationBananaDoubleChip.nearHeight (p q : ℕ) : ℕ

The height at the near vertex: two chips' worth of its own arm, clamped by the far arm.

Equations

• AtanasovRanganathan.ConfigurationBananaDoubleChip.nearHeight p q = min (2 * q) p

def AtanasovRanganathan.ConfigurationBananaDoubleChip.farHeight (p q par : ℕ) : ℕ

The height at the far vertex, the target.

Equations

• AtanasovRanganathan.ConfigurationBananaDoubleChip.farHeight p q par = min p (AtanasovRanganathan.ConfigurationBananaDoubleChip.nearHeight p q + par)

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.nearHeight_le_far {p q par : ℕ} : nearHeight p q ≤ farHeight p q par

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.nearHeight_ge_short {p q : ℕ} (hqp : q ≤ p) : q ≤ nearHeight p q

The two residual statements

Both are stated at the orientation row 08 reads them in: the far arm from its tail, the near arm from its head. The mirror orientation is not needed, because the fourth sign pattern of row 08 is the sigma image of the third and is obtained by transport rather than by a second proof.

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.far_center_nonneg {p q par m1 m2 hv hu : ℕ} {k : ℤ} (hpar : par = min m1 m2) (hnear : hv = nearHeight p q) (hfar : hu = farHeight p q par) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hk : k = 1 → 0 < par ∨ hu = p) : 0 ≤ ConfigurationFive.zeroChip p - k + (ConfigurationFive.tailContribution p hu 0 + ConfigurationFive.tailContribution m1 hu hv + ConfigurationFive.tailContribution m2 hu hv)

The far vertex, the target. k is one exactly when the delivered chip is charged here; the hypothesis says that is legitimate.

theorem AtanasovRanganathan.ConfigurationBananaDoubleChip.far_partner_nonneg {p q par m1 m2 hv hu : ℕ} {k : ℤ} (hpar : par = min m1 m2) (hnear : hv = nearHeight p q) (hfar : hu = farHeight p q par) (hqp : q ≤ p) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hk : k = 1 → par = 0 ∧ 0 < q) : 0 ≤ 2 * ConfigurationFive.zeroChip q - k + (ConfigurationFive.headContribution q 0 hv + ConfigurationFive.headContribution m1 hu hv + ConfigurationFive.headContribution m2 hu hv)

The near vertex, under the double chip. It balances because its own arm runs at slope two exactly when the banana charges it twice.