The chip-free pair over a marked script

ConfigurationThree states Atanasov--Ranganathan's third local picture -- two adjacent chip-free vertices, two chip arms each -- against DegSpec.interpolatedScript, one canonical ramp per slot. AR's sixth and seventh genus-five families need the same picture when two of the four arms are halves of a marked slot, because their figures put a chip at an interior point whose offset is a length (Utilities/Subdivision/SplitRampScript.lean).

Nothing about the profile changes: the two heights are still

 h₂ = min a b            -- the partner
 h₁ = min a (h₂ + m)     -- the target

with a, b the two arm minima and m the middle slot. What changes is only which one-edge quantity an arm contributes, and this file supplies the three missing pieces.

• The endpoint ledger of a marked script. positiveEndpointContribution is the marked analogue of the per-vertex sum a row uses, and positiveEndpointContribution_classSum_eq identifies its class sums with the Laplacian. The three reading lemmas slot*_of_unmarked, slot*_of_markedTail and slot*_of_markedHead turn each slot's two terms into ConfigurationFive's tailContribution / headContribution at the relevant half length. A marked slot always has one flat half in the intended configurations, which is why exactly two readings suffice.
• The chip at a mark, read at a core class. markChipWeight records where the interior chip lands when the mark degenerates to an end of its slot (mark = 0 on a collapsed leg, mark = length on a chamber wall), and markChip_classSum_eq proves the class sum.
• The pair profile itself, pairTarget_nonneg and pairPartner_nonneg, stated through a PairLedger so that each of the four arms may be a whole slot read from either end or the half of a marked slot, and so that the pair is proved once and instantiated at both centres.

The k parameter of the two pair statements is the indicator of which vertex of the contracted class owns the delivered chip: when the middle slot collapses the two centres merge, and the chip may have to be charged to the partner. That is the targetOwner device every finished row already uses.

The two endpoint terms of one slot under a marked script

def AtanasovRanganathan.ConfigurationMarkedThree.slotTailTerm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (potential : Fin 8 → ℤ) (mark : Fin 12 → ℕ) (markValue : Fin 12 → ℤ) (e : Fin 12) : ℤ

What one slot contributes at its tail class, with a collapsed slot's artificial term suppressed.

Equations

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

def AtanasovRanganathan.ConfigurationMarkedThree.slotHeadTerm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (potential : Fin 8 → ℤ) (mark : Fin 12 → ℕ) (markValue : Fin 12 → ℤ) (e : Fin 12) : ℤ

What one slot contributes at its head class, with a collapsed slot's artificial term suppressed.

Equations

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

def AtanasovRanganathan.ConfigurationMarkedThree.positiveEndpointContribution (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (potential : Fin 8 → ℤ) (mark : Fin 12 → ℕ) (markValue : Fin 12 → ℤ) (v : Fin 8) : ℤ

The per-vertex endpoint ledger of a marked script.

Equations

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

theorem AtanasovRanganathan.ConfigurationMarkedThree.positiveEndpointContribution_classSum_eq (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, positiveEndpointContribution d potential mark markValue v = (prin d.graph) (d.splitScript potential mark markValue) (d.coreVertex r)

The class sum is the Laplacian. The artificial endpoint terms of a collapsed slot cancel, which is what lets a row work vertex by vertex on the uncontracted core.

Reading one slot as one or two ordinary arms

Throughout, hu is the height at the tail class and hv the height at the head class; the script is potential = -height. The two marked readings are the ones the AR rows use: the chip at the mark sits where a flat stretch meets a full ramp, so exactly one of the two heights is zero.

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotTailTerm_of_unmarked (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hu hv : ℕ} (hMark : mark e = 0) (hValue : markValue e = potential (d.rep (d.core.tail e))) (hTail : potential (d.rep (d.core.tail e)) = -↑hu) (hHead : potential (d.rep (d.core.head e)) = -↑hv) : slotTailTerm d potential mark markValue e = ConfigurationFive.tailContribution (d.length e) hu hv

An unmarked slot is an ordinary arm of its own length.

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotHeadTerm_of_unmarked (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hu hv : ℕ} (hMark : mark e = 0) (hValue : markValue e = potential (d.rep (d.core.tail e))) (hTail : potential (d.rep (d.core.tail e)) = -↑hu) (hHead : potential (d.rep (d.core.head e)) = -↑hv) : slotHeadTerm d potential mark markValue e = ConfigurationFive.headContribution (d.length e) hu hv

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotTailTerm_of_markedTail (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hu : ℕ} (hMarks : d.MarksAdmissible potential mark markValue) (hValue : markValue e = 0) (hTail : potential (d.rep (d.core.tail e)) = -↑hu) (hHead : potential (d.rep (d.core.head e)) = 0) : slotTailTerm d potential mark markValue e = ConfigurationFive.tailContribution (mark e) hu 0

A marked slot whose head carries height zero: its tail sees an ordinary arm of the near half length, and its head sees nothing unless the mark has reached the head.

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotHeadTerm_of_markedTail (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hu : ℕ} (hMarks : d.MarksAdmissible potential mark markValue) (hValue : markValue e = 0) (hTail : potential (d.rep (d.core.tail e)) = -↑hu) (hHead : potential (d.rep (d.core.head e)) = 0) : slotHeadTerm d potential mark markValue e = if mark e < d.length e then 0 else ConfigurationFive.headContribution (d.length e) hu 0

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotTailTerm_of_markedHead (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hv : ℕ} (hMarks : d.MarksAdmissible potential mark markValue) (hValue : markValue e = 0) (hTail : potential (d.rep (d.core.tail e)) = 0) (hHead : potential (d.rep (d.core.head e)) = -↑hv) : slotTailTerm d potential mark markValue e = if 0 < mark e then 0 else ConfigurationFive.tailContribution (d.length e) 0 hv

A marked slot whose tail carries height zero: its head sees an ordinary arm of the far half length, and its tail sees nothing unless the mark is still at the tail.

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotHeadTerm_of_markedHead (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hv : ℕ} (hMarks : d.MarksAdmissible potential mark markValue) (hValue : markValue e = 0) (hTail : potential (d.rep (d.core.tail e)) = 0) (hHead : potential (d.rep (d.core.head e)) = -↑hv) : slotHeadTerm d potential mark markValue e = ConfigurationFive.headContribution (d.length e - mark e) 0 hv

The uniform marked reading

In the intended configurations one of the two heights at a marked slot's ends is zero -- the chip sits where a flat stretch meets a full ramp, which is also the hypothesis under which the chip pays for the kink. Under that single assumption the two readings above collapse into one pair of formulas, valid at either orientation, and (taking mark e = 0) agreeing with the unmarked slot's tail reading.

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotTailTerm_of_marked (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hu hv : ℕ} (hMarks : d.MarksAdmissible potential mark markValue) (hValue : markValue e = 0) (hTail : potential (d.rep (d.core.tail e)) = -↑hu) (hHead : potential (d.rep (d.core.head e)) = -↑hv) (hflat : hu = 0 ∨ hv = 0) : slotTailTerm d potential mark markValue e = if 0 < mark e then ConfigurationFive.tailContribution (mark e) hu 0 else ConfigurationFive.tailContribution (d.length e) hu hv

theorem AtanasovRanganathan.ConfigurationMarkedThree.slotHeadTerm_of_marked (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {potential : Fin 8 → ℤ} {mark : Fin 12 → ℕ} {markValue : Fin 12 → ℤ} {e : Fin 12} {hu hv : ℕ} (hMarks : d.MarksAdmissible potential mark markValue) (hValue : markValue e = 0) (hTail : potential (d.rep (d.core.tail e)) = -↑hu) (hHead : potential (d.rep (d.core.head e)) = -↑hv) (hflat : hu = 0 ∨ hv = 0) : slotHeadTerm d potential mark markValue e = if mark e < d.length e then ConfigurationFive.headContribution (d.length e - mark e) 0 hv else ConfigurationFive.headContribution (d.length e) hu hv

The chip at a mark, seen from a core class

When the mark degenerates to an end of its slot the interior chip is a core vertex. Both degeneracies occur on real faces: mark = 0 when the leg carrying the chip collapses, mark = length on the chamber wall where the figure's inequality is an equality.

def AtanasovRanganathan.ConfigurationMarkedThree.markChipWeight (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (mark : Fin 12 → ℕ) (e : Fin 12) (v : Fin 8) : ℤ

Where the chip at the mark of e sits, as a weight on core vertices.

Equations

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

theorem AtanasovRanganathan.ConfigurationMarkedThree.markChipWeight_nonneg (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (mark : Fin 12 → ℕ) (e : Fin 12) (v : Fin 8) : 0 ≤ markChipWeight d mark e v

theorem AtanasovRanganathan.ConfigurationMarkedThree.markChip_classSum_eq (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (mark : Fin 12 → ℕ) (e : Fin 12) (r : Fin 8) : oneChip (d.pathAt e (mark e)) (d.coreVertex r) = ∑ v : Fin 8 with d.rep v = d.rep r, markChipWeight d mark e v

Redistributing chips inside a contracted class

A chip may be delivered to a vertex of the target's class other than the target itself, and a collapsed arm may put its chip in the centre's class. Both are handled by moving weight within a class, which leaves every class sum -- hence the divisor -- unchanged.

theorem AtanasovRanganathan.ConfigurationMarkedThree.sum_conditional_transfer_eq_zero (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (P : Prop) [Decidable P] (source target : Fin 8) (hRep : P → d.rep source = d.rep target) (r : Fin 8) : (∑ v : Fin 8 with d.rep v = d.rep r, if P then transferWeight source target v else 0) = 0

The pair profile

An arm of the picture may be a whole slot read from either end, or the half of a marked slot. A PairLedger names the contribution at the end carrying the height, so that both the target and the partner statement are proved once.

structure AtanasovRanganathan.ConfigurationMarkedThree.PairLedger : Type

The one-edge facts the pair profile consumes. tail L hu hv is the contribution at the end carrying height hu.

• tail : ℕ → ℕ → ℕ → ℤ

  The tail contribution of a paired slot as a function of length and endpoint heights.

• tail_nonneg {L hu hv : ℕ} : hv ≤ hu → hu ≤ hv + L → 0 ≤ self.tail L hu hv
• tail_ge_neg_one {L hu hv : ℕ} : hv ≤ hu + L → hu ≤ hv + L → -1 ≤ self.tail L hu hv
• tail_same (L h : ℕ) : self.tail L h h = 0
• zeroChip_add_tail_full (L : ℕ) : 1 ≤ ConfigurationFive.zeroChip L + self.tail L L 0
• tail_eq_one_of_full {L hu hv : ℕ} : 0 < L → hu = hv + L → self.tail L hu hv = 1

def AtanasovRanganathan.ConfigurationMarkedThree.fwd : PairLedger

The slot read from its tail.

Equations

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

def AtanasovRanganathan.ConfigurationMarkedThree.rev : PairLedger

The same slot read from its head.

Equations

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

@[simp]

theorem AtanasovRanganathan.ConfigurationMarkedThree.fwd_tail (L hu hv : ℕ) : fwd.tail L hu hv = ConfigurationFive.tailContribution L hu hv

@[simp]

theorem AtanasovRanganathan.ConfigurationMarkedThree.rev_tail (L hu hv : ℕ) : rev.tail L hu hv = ConfigurationFive.headContribution L hv hu

theorem AtanasovRanganathan.ConfigurationMarkedThree.pairTarget_nonneg (SA SB SM : PairLedger) {la lb m a b g o : ℕ} {k : ℤ} (ha : a = min la lb) (hg : g = min a b) (ho : o = min a (g + m)) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hk : k = 1 → m = 0 → a ≤ b) : 0 ≤ ConfigurationFive.zeroChip la + ConfigurationFive.zeroChip lb - k + (SA.tail la o 0 + SB.tail lb o 0 + SM.tail m o g)

The target of a configuration-3 pair. la, lb are the target's two arm lengths, m the middle slot, a = min la lb, b the partner's arm minimum, g = min a b the partner height and o = min a (g + m) the target height. k is one exactly when the delivered chip is charged to this vertex.

theorem AtanasovRanganathan.ConfigurationMarkedThree.pairPartner_nonneg (SC SD SM : PairLedger) {lc ld m a b g o : ℕ} {k : ℤ} (hb : b = min lc ld) (hg : g = min a b) (ho : o = min a (g + m)) (hk0 : 0 ≤ k) (hk1 : k ≤ 1) (hk : k = 1 → m = 0 ∧ b < a) : 0 ≤ ConfigurationFive.zeroChip lc + ConfigurationFive.zeroChip ld - k + (SC.tail lc g 0 + SD.tail ld g 0 + SM.tail m g o)

The partner of a configuration-3 pair. lc, ld are the partner's two arm lengths and b = min lc ld; the partner sits at height g and reads the middle slot from below.