Atanasov--Ranganathan configuration 5, generic in the core

Configuration 5 of Atanasov--Ranganathan, Proposition 5.1, is the local picture at a centre of the length-independent row: two boundary arms, a middle slot to a second centre, two parallel slots onward to a cycle vertex, and one far slot closing the cycle. Two nested minima fix the three heights, and the whole verification reduces to one-edge arithmetic.

This file carries that arithmetic once, in two layers. The first is the one-edge ledger: what one slot contributes at each of its ends, stated for a slot read from either end -- tailContribution at the tail, headContribution at the head -- because a row reads the same picture at two centres in opposite orientations, and every fact here has a mirror.

The second layer states the residual effectivity at each vertex of the local picture, once per nested-min profile (outerTarget_* when the outer minimum saturates first, innerTarget_* when the inner one does) and once for the cycle vertex, which both profiles share. The three slots whose orientation varies between the two centres -- the two boundary arms and the far slot -- are read through a SlotLedger, so each statement covers both orientations; the middle and parallel slots point the same way at both centres and are spelled out directly. A row supplies its lookup tables and the five height equations; nothing else.

One-edge arithmetic used by configuration 5

def AtanasovRanganathan.ConfigurationFive.tailContribution (L hu hv : ℕ) : ℤ

The contribution at the tail of a subdivided edge with the prescribed endpoint heights.

Equations

• AtanasovRanganathan.ConfigurationFive.tailContribution L hu hv = if L = 0 then 0 else Utilities.Certificate.SubdivisionArithmetic.step L (↑hu - ↑hv) 0

def AtanasovRanganathan.ConfigurationFive.headContribution (L hu hv : ℕ) : ℤ

The contribution at the head of a subdivided edge with the prescribed endpoint heights.

Equations

• AtanasovRanganathan.ConfigurationFive.headContribution L hu hv = if L = 0 then 0 else -Utilities.Certificate.SubdivisionArithmetic.step L (↑hu - ↑hv) (L - 1)

theorem AtanasovRanganathan.ConfigurationFive.tailContribution_zero_zero (L : ℕ) : tailContribution L 0 0 = 0

theorem AtanasovRanganathan.ConfigurationFive.headContribution_zero_zero (L : ℕ) : headContribution L 0 0 = 0

theorem AtanasovRanganathan.ConfigurationFive.tailContribution_ge_neg_one {L hu hv : ℕ} (hLower : hv ≤ hu + L) (hUpper : hu ≤ hv + L) : -1 ≤ tailContribution L hu hv

theorem AtanasovRanganathan.ConfigurationFive.headContribution_ge_neg_one {L hu hv : ℕ} (hLower : hv ≤ hu + L) (hUpper : hu ≤ hv + L) : -1 ≤ headContribution L hu hv

theorem AtanasovRanganathan.ConfigurationFive.tailContribution_nonneg {L hu hv : ℕ} (h : hv ≤ hu) (hUpper : hu ≤ hv + L) : 0 ≤ tailContribution L hu hv

theorem AtanasovRanganathan.ConfigurationFive.headContribution_nonneg {L hu hv : ℕ} (h : hu ≤ hv) (hUpper : hv ≤ hu + L) : 0 ≤ headContribution L hu hv

theorem AtanasovRanganathan.ConfigurationFive.tailContribution_eq_one_of_full {L hu hv : ℕ} (hL : 0 < L) (hFull : hu = hv + L) : tailContribution L hu hv = 1

theorem AtanasovRanganathan.ConfigurationFive.headContribution_eq_one_of_full {L hu hv : ℕ} (hL : 0 < L) (hFull : hv = hu + L) : headContribution L hu hv = 1

def AtanasovRanganathan.ConfigurationFive.positiveChip (L : ℕ) : ℤ

One chip when the edge length is positive, and zero for a collapsed edge.

Equations

• AtanasovRanganathan.ConfigurationFive.positiveChip L = if L = 0 then 0 else 1

def AtanasovRanganathan.ConfigurationFive.zeroChip (L : ℕ) : ℤ

One chip for a collapsed edge, and zero when the edge length is positive.

Equations

• AtanasovRanganathan.ConfigurationFive.zeroChip L = if L = 0 then 1 else 0

theorem AtanasovRanganathan.ConfigurationFive.positiveChip_nonneg (L : ℕ) : 0 ≤ positiveChip L

theorem AtanasovRanganathan.ConfigurationFive.zeroChip_nonneg (L : ℕ) : 0 ≤ zeroChip L

@[simp]

theorem AtanasovRanganathan.ConfigurationFive.tailContribution_same (L h : ℕ) : tailContribution L h h = 0

@[simp]

theorem AtanasovRanganathan.ConfigurationFive.headContribution_same (L h : ℕ) : headContribution L h h = 0

theorem AtanasovRanganathan.ConfigurationFive.zeroChip_add_tail_full (L : ℕ) : 1 ≤ zeroChip L + tailContribution L L 0

theorem AtanasovRanganathan.ConfigurationFive.zeroChip_add_head_full (L : ℕ) : 1 ≤ zeroChip L + headContribution L 0 L

theorem AtanasovRanganathan.ConfigurationFive.positiveChip_add_head_nonneg {L h : ℕ} (hh : h ≤ L) : 0 ≤ positiveChip L + headContribution L h 0

theorem AtanasovRanganathan.ConfigurationFive.positiveChip_add_tail_nonneg {L h : ℕ} (hh : h ≤ L) : 0 ≤ positiveChip L + tailContribution L 0 h

@[reducible, inline]

abbrev AtanasovRanganathan.ConfigurationFive.drain (height : ℕ) : ℤ

The drain indicator: one unit for a positive height and zero at height zero.

Equations

• AtanasovRanganathan.ConfigurationFive.drain = AtanasovRanganathan.ConfigurationThree.drain

theorem AtanasovRanganathan.ConfigurationFive.headContribution_eq_neg_drain_of_ge {L hi lo : ℕ} (hGe : lo ≤ hi) (hLe : hi ≤ lo + L) : headContribution L hi lo = -drain (hi - lo)

theorem AtanasovRanganathan.ConfigurationFive.tailContribution_eq_neg_drain_of_le {L hi lo : ℕ} (hLe : hi ≤ lo) (hBound : lo ≤ hi + L) : tailContribution L hi lo = -drain (lo - hi)

The orientation ledger

Row 07 reads the same local picture at two centres. The middle slot and the two parallel slots point the same way at both, but the two boundary arms and the far slot are traversed in opposite directions. A SlotLedger names the two ends of those three slots, so that the whole calculation below is written once and instantiated twice.

structure AtanasovRanganathan.ConfigurationFive.SlotLedger : Type

The two ends of a slot whose orientation depends on which centre is being read. 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 : ℕ → ℕ → ℕ → ℤ

  The tail contribution as a function of edge length and the two endpoint heights.

• head : ℕ → ℕ → ℕ → ℤ

  The head contribution as a function of edge length and the two endpoint heights.

• tail_nonneg {L hu hv : ℕ} : hv ≤ hu → hu ≤ hv + L → 0 ≤ self.tail L hu hv
• zeroChip_add_tail_full (L : ℕ) : 1 ≤ zeroChip L + self.tail L L 0
• positiveChip_add_head_nonneg {L h : ℕ} : h ≤ L → 0 ≤ positiveChip L + self.head L h 0

def AtanasovRanganathan.ConfigurationFive.forward : SlotLedger

The slot read from its tail.

Equations

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

def AtanasovRanganathan.ConfigurationFive.reverse : SlotLedger

The same slot read from its head.

Equations

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

The outer-target reading

o is the height at the centre, i at the second centre, e at the cycle vertex, and the two nested minima saturate outer-first.

theorem AtanasovRanganathan.ConfigurationFive.outerTarget_center_nonneg (SA SB : SlotLedger) {la lb c lp lq b a m o i : ℕ} (ha : a = min la lb) (hm : m = min lp lq) (ho : o = min a (b + m + c)) (hi : i = min o (b + m)) : 0 ≤ (zeroChip la + zeroChip lb - if c = 0 then if a ≤ b + m then 1 else 0 else 1) + (SA.tail la o 0 + SB.tail lb o 0 + tailContribution c o i)

Residual effectivity at an outer-target centre.

The two boundary arms get independent ledgers: a row whose centre is the tail of one arm and the head of the other (any core whose local cycle is a directed one, such as atlas row 09) reads them in opposite orientations. A row whose arms point the same way passes the same ledger twice.

theorem AtanasovRanganathan.ConfigurationFive.outerTarget_inner_nonneg {c lp lq b a m o i e : ℕ} (hm : m = min lp lq) (ho : o = min a (b + m + c)) (hi : i = min o (b + m)) (he : e = min i b) : 0 ≤ (zeroChip m - if c = 0 then if a ≤ b + m then 0 else 1 else 0) + (headContribution c o i + tailContribution lp i e + tailContribution lq i e)

Residual effectivity at the second centre of an outer-target reading.

The inner-target reading

The same ledger with the two nested minima saturating inner-first.

theorem AtanasovRanganathan.ConfigurationFive.innerTarget_center_nonneg (SA SB : SlotLedger) {la lb c lp lq b a m o i : ℕ} (ha : a = min la lb) (hm : m = min lp lq) (hi : i = min (a + c) (b + m)) (ho : o = min a i) : 0 ≤ (zeroChip la + zeroChip lb - if c = 0 then if a ≤ b + m then 1 else 0 else 0) + (SA.tail la o 0 + SB.tail lb o 0 + tailContribution c o i)

Residual effectivity at the outer centre of an inner-target reading.

As with outerTarget_center_nonneg, the two boundary arms carry independent ledgers.

theorem AtanasovRanganathan.ConfigurationFive.innerTarget_inner_nonneg {c lp lq b a m o i e : ℕ} (hm : m = min lp lq) (hi : i = min (a + c) (b + m)) (ho : o = min a i) (he : e = min b i) : 0 ≤ (zeroChip m - if c = 0 then if a ≤ b + m then 0 else 1 else 1) + (headContribution c o i + tailContribution lp i e + tailContribution lq i e)

Residual effectivity at the inner centre of an inner-target reading.

The cycle vertex

Shared by both readings: only the far slot's orientation varies.

theorem AtanasovRanganathan.ConfigurationFive.cycle_nonneg (S : SlotLedger) {lp lq b m i e : ℕ} (hm : m = min lp lq) (heI : e ≤ i) (heB : e ≤ b) (hEB : e = i ∨ e = b) (hiEM : i ≤ e + m) : 0 ≤ positiveChip m + zeroChip b + (headContribution lp i e + headContribution lq i e + S.tail b e 0)

Residual effectivity at the cycle vertex.