Atanasov--Ranganathan configuration 3, generic in the core

Configuration 3 of Atanasov--Ranganathan, Proposition 5.1, is the local picture at a chip-free pair of adjacent core vertices, each of whose two remaining slots ends on a chip vertex. Several genus-five rows are covered by this one picture, and until now each row carried its own verbatim copy of the calculation against its own lookup tables.

This file states the picture once, as a ConfigThree bundle of the lookup data together with the incidence facts a row must check, and proves the whole closed-face calculation from those facts alone. A row supplies the tables and discharges the Prop fields; nothing else.

For a target centre, let a and b be the shorter arm lengths on the target and partner sides, and let m be the middle-slot length. We interpolate the core potentials -h₁, -h₂, where

• h₂ = min a b, and
• h₁ = min a (h₂ + m).

If h₁ = a, a target arm supplies the requested chip. Otherwise the middle slot is full and supplies it. Whenever the partner loses a chip through the middle slot, h₂ = b, so one of its arms replenishes that chip. This formula also has h₁ = h₂ when m = 0, which is exactly what is needed on a closed face where the two centres contract.

Core size

ConfigThree n p is generic in the core size: n vertices and p slots. The genus-five atlas instantiates it at ConfigThree 8 12; it also supports the instance ConfigThree 10 15. The whole file is size-free except for closedConstruction, which needs 0 < n and takes it as a hypothesis, the same one Guarding.GuardingSet.closedConstruction carries.

Unordered incidence

def AtanasovRanganathan.ConfigurationThree.Ends {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (e : Fin p) (u v : Fin n) : Prop

The slot e joins u and v, in either orientation.

Equations

• AtanasovRanganathan.ConfigurationThree.Ends core e u v = (core.tail e = u ∧ core.head e = v ∨ core.tail e = v ∧ core.head e = u)

@[instance_reducible]

instance AtanasovRanganathan.ConfigurationThree.instDecidableEnds {n p : ℕ} (core : Utilities.Certificate.ExplicitPotential.Core n p) (e : Fin p) (u v : Fin n) : Decidable (Ends core e u v)

Equations

• AtanasovRanganathan.ConfigurationThree.instDecidableEnds core e u v = id inferInstance

theorem AtanasovRanganathan.ConfigurationThree.Ends.pair_eq {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} {e : Fin p} {u v u' v' : Fin n} (h : Ends core e u v) (h' : Ends core e u' v') : u = u' ∧ v = v' ∨ u = v' ∧ v = u'

A slot has one pair of endpoints: two Ends readings of the same slot agree as unordered pairs.

theorem AtanasovRanganathan.ConfigurationThree.ne_of_ends_of_ne {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} {e f : Fin p} {u a v b : Fin n} (he : Ends core e u a) (hf : Ends core f v b) (huv : u ≠ v) (hub : u ≠ b) : e ≠ f

Two slots with different first endpoints are different slots.

theorem AtanasovRanganathan.ConfigurationThree.ne_of_ends_same {n p : ℕ} {core : Utilities.Certificate.ExplicitPotential.Core n p} {e f : Fin p} {u a b : Fin n} (he : Ends core e u a) (hf : Ends core f u b) (hab : a ≠ b) (hub : u ≠ b) : e ≠ f

Two slots at the same vertex with different far endpoints are different slots.

Small arithmetic reused from the row-11 step lemmas

theorem AtanasovRanganathan.ConfigurationThree.step_zero {L i : ℕ} (hi : i < L) : Utilities.Certificate.SubdivisionArithmetic.step L 0 i = 0

def AtanasovRanganathan.ConfigurationThree.drain (height : ℕ) : ℤ

One chip leaves an arm exactly when its ramp has positive height.

Equations

• AtanasovRanganathan.ConfigurationThree.drain height = if 0 < height then 1 else 0

theorem AtanasovRanganathan.ConfigurationThree.drain_bounds (height : ℕ) : 0 ≤ drain height ∧ drain height ≤ 1

theorem AtanasovRanganathan.ConfigurationThree.drain_eq_one {height : ℕ} (h : 0 < height) : drain height = 1

theorem AtanasovRanganathan.ConfigurationThree.drain_eq_zero : drain 0 = 0

theorem AtanasovRanganathan.ConfigurationThree.indicator_bounds (p : Prop) [Decidable p] : (0 ≤ if p then 1 else 0) ∧ (if p then 1 else 0) ≤ 1

theorem AtanasovRanganathan.ConfigurationThree.firstStep_neg_eq_neg_drain {L height : ℕ} (hLength : 0 < L) (hLe : height ≤ L) : Utilities.Certificate.SubdivisionArithmetic.step L (-↑height) 0 = -drain height

theorem AtanasovRanganathan.ConfigurationThree.lastStep_pos_eq_drain {L height : ℕ} (hLength : 0 < L) (hLe : height ≤ L) : Utilities.Certificate.SubdivisionArithmetic.step L (↑height) (L - 1) = drain height

Splitting a slot sum over the finitely many active slots

theorem AtanasovRanganathan.ConfigurationThree.sum_three {p : ℕ} (g : Fin p → ℤ) {a b c : Fin p} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hzero : ∀ (x : Fin p), x ≠ a → x ≠ b → x ≠ c → g x = 0) : ∑ x : Fin p, g x = g a + g b + g c

theorem AtanasovRanganathan.ConfigurationThree.sum_five {p : ℕ} (g : Fin p → ℤ) {a b c u v : Fin p} (hab : a ≠ b) (hac : a ≠ c) (hau : a ≠ u) (hav : a ≠ v) (hbc : b ≠ c) (hbu : b ≠ u) (hbv : b ≠ v) (hcu : c ≠ u) (hcv : c ≠ v) (huv : u ≠ v) (hzero : ∀ (x : Fin p), x ≠ a → x ≠ b → x ≠ c → x ≠ u → x ≠ v → g x = 0) : ∑ x : Fin p, g x = g a + g b + g c + g u + g v

One slot's endpoint terms

def AtanasovRanganathan.ConfigurationThree.slotTerm {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (e : Fin p) (v : Fin n) : ℤ

The two endpoint terms one core slot contributes at one core vertex. This is literally the summand of ConfigurationCommon.endpointContribution.

Equations

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

theorem AtanasovRanganathan.ConfigurationThree.endpointContribution_eq_sum {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (v : Fin n) : ConfigurationCommon.endpointContribution d potential v = ∑ e : Fin p, slotTerm d potential e v

def AtanasovRanganathan.ConfigurationThree.slotValue {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (e : Fin p) (a b : ℤ) : ℤ

The value of one slot's endpoint terms at a vertex where the potential is a and whose far end carries potential b.

Equations

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

theorem AtanasovRanganathan.ConfigurationThree.slotTerm_eq_slotValue {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) {e : Fin p} {center other : Fin n} (hEnds : Ends d.core e center other) (hne : other ≠ center) : slotTerm d potential e center = slotValue d center e (potential center) (potential other)

def AtanasovRanganathan.ConfigurationThree.armContribution {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (edge : Fin p) (height : ℕ) : ℤ

Contribution at a centre from one of its arms, whose far endpoint carries potential zero.

Equations

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

theorem AtanasovRanganathan.ConfigurationThree.armContribution_eq_slotValue {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (edge : Fin p) (height : ℕ) : armContribution d center edge height = slotValue d center edge (-↑height) 0

theorem AtanasovRanganathan.ConfigurationThree.slotValue_nonneg {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (e : Fin p) {a b : ℤ} {k : ℕ} (hk : b - a = ↑k) (hLength : 0 < d.length e) (hLe : k ≤ d.length e) : 0 ≤ slotValue d center e a b

A ramp that goes down from the centre never removes a chip there.

theorem AtanasovRanganathan.ConfigurationThree.slotValue_eq_one_of_full {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (e : Fin p) {a b : ℤ} (hFull : b - a = ↑(d.length e)) (hLength : 0 < d.length e) : slotValue d center e a b = 1

A full-length ramp delivers exactly one chip to the centre.

theorem AtanasovRanganathan.ConfigurationThree.slotValue_eq_neg_drain {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (e : Fin p) {a b : ℤ} {k : ℕ} (hk : a - b = ↑k) (hLength : 0 < d.length e) (hLe : k ≤ d.length e) : slotValue d center e a b = -drain k

A ramp that goes up from the centre removes exactly one chip there when its height is positive, and nothing when it is flat.

theorem AtanasovRanganathan.ConfigurationThree.armContribution_nonneg {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (e : Fin p) {height : ℕ} (hLe : height ≤ d.length e) (hLength : 0 < d.length e) : 0 ≤ armContribution d center e height

theorem AtanasovRanganathan.ConfigurationThree.armContribution_eq_one_of_full {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (e : Fin p) {height : ℕ} (hFull : height = d.length e) (hLength : 0 < d.length e) : armContribution d center e height = 1

One slot's contribution to a different contracted class

theorem AtanasovRanganathan.ConfigurationThree.endpointPair_eq_zero_of_reps {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) (e : Fin p) (r : Fin n) (hTail : d.rep (d.core.tail e) ≠ d.rep r) (hHead : d.rep (d.core.head e) ≠ d.rep r) : ConfigurationCommon.endpointPair d potential e r = 0

theorem AtanasovRanganathan.ConfigurationThree.endpointPair_arm {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (potential : Fin n → ℤ) {e : Fin p} {center chip r : Fin n} {h : ℕ} (hEnds : Ends d.core e center chip) (hCentre : potential center = -↑h) (hFar : potential chip = 0) (hLength : 0 < d.length e) (hLe : h ≤ d.length e) (hNot : d.rep center ≠ d.rep r) : ConfigurationCommon.endpointPair d potential e r = -drain h * if d.rep chip = d.rep r then 1 else 0

An arm of height h from a centre off the class of r removes drain h chips from the class of its far endpoint.

The configuration data

def AtanasovRanganathan.ConfigurationThree.IsChipOf {n : ℕ} (a b c e v : Fin n) : Prop

Membership in a displayed four-chip set. Spelled out so that the fields of ConfigThree can refer to it.

Equations

• AtanasovRanganathan.ConfigurationThree.IsChipOf a b c e v = (v = a ∨ v = b ∨ v = c ∨ v = e)

@[instance_reducible]

instance AtanasovRanganathan.ConfigurationThree.instDecidableIsChipOf {n : ℕ} (a b c e v : Fin n) : Decidable (IsChipOf a b c e v)

Equations

• AtanasovRanganathan.ConfigurationThree.instDecidableIsChipOf a b c e v = id inferInstance

structure AtanasovRanganathan.ConfigurationThree.ConfigThree (n p : ℕ) : Type

The lookup data of one AR configuration-3 row, together with exactly the incidence facts the calculation uses.

The four chips carry the divisor. Each declared centre v is chip free and paired with partner v, joined to it by middleSlot v, and its two other slots firstArm v, secondArm v end on the chips firstChip v, secondChip v.

As in ConfigTwo, the centres are named by an explicit predicate isCenter rather than "every chip-free vertex", so that a row combining several local pictures can declare only some of its chip-free vertices to be configuration-3 centres. A row all of whose chip-free vertices are centres gets the whole closed-orthant construction from closedConstruction.

• core : Utilities.Certificate.ExplicitPotential.Core n p

  The finite core graph carrying configuration three and its designated chip vertices.

• chipOne : Fin n

  The first of the four designated chip vertices of configuration three.

• chipTwo : Fin n

  The second of the four designated chip vertices of configuration three.

• chipThree : Fin n

  The third of the four designated chip vertices of configuration three.

• chipFour : Fin n

  The fourth of the four designated chip vertices of configuration three.

• isCenter : Fin n → Bool

  The Boolean selector of the paired center vertices, disjoint from the chip vertices.

• partner : Fin n → Fin n

  The opposite center in the involutive pairing of center vertices.

• firstArm : Fin n → Fin p

  The core slot connecting a center to its first assigned chip vertex.

• secondArm : Fin n → Fin p

  The core slot connecting a center to its second assigned chip vertex.

• middleSlot : Fin n → Fin p

  The middle slot joining a pair of centers, shared by the two partners.

• firstChip : Fin n → Fin n

  The chip vertex reached from a center along its first arm.

• secondChip : Fin n → Fin n

  The chip vertex reached from a center along its second arm.

• center_not_chip (v : Fin n) : self.isCenter v = true → ¬IsChipOf self.chipOne self.chipTwo self.chipThree self.chipFour v
• partner_isCenter (v : Fin n) : self.isCenter v = true → self.isCenter (self.partner v) = true
• partner_ne (v : Fin n) : self.isCenter v = true → self.partner v ≠ v
• partner_partner (v : Fin n) : self.isCenter v = true → self.partner (self.partner v) = v
• middleSlot_partner (v : Fin n) : self.isCenter v = true → self.middleSlot (self.partner v) = self.middleSlot v
• firstChip_isChip (v : Fin n) : self.isCenter v = true → IsChipOf self.chipOne self.chipTwo self.chipThree self.chipFour (self.firstChip v)
• secondChip_isChip (v : Fin n) : self.isCenter v = true → IsChipOf self.chipOne self.chipTwo self.chipThree self.chipFour (self.secondChip v)
• firstArm_ends (v : Fin n) : self.isCenter v = true → Ends self.core (self.firstArm v) v (self.firstChip v)
• secondArm_ends (v : Fin n) : self.isCenter v = true → Ends self.core (self.secondArm v) v (self.secondChip v)
• middleSlot_ends (v : Fin n) : self.isCenter v = true → Ends self.core (self.middleSlot v) v (self.partner v)
• firstArm_ne_secondArm (v : Fin n) : self.isCenter v = true → self.firstArm v ≠ self.secondArm v
• incident_slots (v : Fin n) : self.isCenter v = true → ∀ (e : Fin p), self.core.tail e = v ∨ self.core.head e = v → e = self.firstArm v ∨ e = self.secondArm v ∨ e = self.middleSlot v
• chipSum (v : Fin n) : self.isCenter v = true → ∀ (f : Fin n → ℤ), f self.chipOne + f self.chipTwo + f self.chipThree + f self.chipFour = f (self.firstChip v) + f (self.secondChip v) + f (self.firstChip (self.partner v)) + f (self.secondChip (self.partner v))

@[reducible, inline]

abbrev AtanasovRanganathan.ConfigurationThree.ConfigThree.IsChip {n p : ℕ} (cfg : ConfigThree n p) (v : Fin n) : Prop

The four displayed chip vertices.

Equations

• cfg.IsChip v = AtanasovRanganathan.ConfigurationThree.IsChipOf cfg.chipOne cfg.chipTwo cfg.chipThree cfg.chipFour v

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.chip_ne_of_not_chip {n p : ℕ} (cfg : ConfigThree n p) {u v : Fin n} (hu : cfg.IsChip u) (hv : ¬cfg.IsChip v) : u ≠ v

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.notChip {n p : ℕ} (cfg : ConfigThree n p) (v : Fin n) (h : cfg.isCenter v = true) : ¬cfg.IsChip v

A declared centre carries no chip.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partner_not_chip {n p : ℕ} (cfg : ConfigThree n p) (v : Fin n) (h : cfg.isCenter v = true) : ¬cfg.IsChip (cfg.partner v)

The partner of a declared centre carries no chip.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.center_ne_partner {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : center ≠ cfg.partner center

Incidence facts transported to a degenerate spec

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.ends_firstArm {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) : Ends d.core (cfg.firstArm center) center (cfg.firstChip center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.ends_secondArm {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) : Ends d.core (cfg.secondArm center) center (cfg.secondChip center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.ends_middleSlot {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) : Ends d.core (cfg.middleSlot center) center (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.ends_middleSlot_partner {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) : Ends d.core (cfg.middleSlot center) (cfg.partner center) center

The middle slot read from the partner side.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.not_incident_of_ne {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) {e : Fin p} (h1 : e ≠ cfg.firstArm center) (h2 : e ≠ cfg.secondArm center) (h3 : e ≠ cfg.middleSlot center) : cfg.core.tail e ≠ center ∧ cfg.core.head e ≠ center

The displayed divisor

def AtanasovRanganathan.ConfigurationThree.ConfigThree.chipInd {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (r v : Fin n) : ℤ

The indicator of "the chip at v sits in the contracted class of r".

Equations

• AtanasovRanganathan.ConfigurationThree.ConfigThree.chipInd d r v = if d.rep v = d.rep r then 1 else 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.chipInd_nonneg {n p : ℕ} (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (r v : Fin n) : 0 ≤ chipInd d r v

def AtanasovRanganathan.ConfigurationThree.ConfigThree.divisor {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) : CFDiv d.graph

One chip on each of the four displayed vertices.

Equations

• cfg.divisor d = AtanasovRanganathan.Configurations.fourChipDivisor (d.coreVertex cfg.chipOne) (d.coreVertex cfg.chipTwo) (d.coreVertex cfg.chipThree) (d.coreVertex cfg.chipFour)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.divisor_effective {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) : effective (cfg.divisor d)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.deg_divisor {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) : CFDiv.degree (cfg.divisor d) = 4

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.one_le_divisor_at_chip {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {chip : Fin n} (hChip : cfg.IsChip chip) : 1 ≤ cfg.divisor d (d.coreVertex chip)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.one_le_divisor_of_chip_rep_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {chip center : Fin n} (hChip : cfg.IsChip chip) (hEq : d.rep chip = d.rep center) : 1 ≤ cfg.divisor d (d.coreVertex center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.divisor_coreVertex_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (r : Fin n) : cfg.divisor d (d.coreVertex r) = chipInd d r cfg.chipOne + chipInd d r cfg.chipTwo + chipInd d r cfg.chipThree + chipInd d r cfg.chipFour

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.divisor_interiorVertex_eq_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (e : Fin p) (o : Fin (d.length e - 1)) : cfg.divisor d (d.interiorVertex e o) = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.length_pos_of_incident_chip {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {center chip : Fin n} {edge : Fin p} (hChip : cfg.IsChip chip) (hEnds : Ends d.core edge center chip) (hZero : cfg.divisor d (d.coreVertex center) = 0) : 0 < d.length edge

A slot from a chip-free class to a chip cannot have collapsed.

The two interpolation heights

def AtanasovRanganathan.ConfigurationThree.ConfigThree.armMin {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (v : Fin n) : ℕ

The smaller length of the two arms incident to the selected center.

Equations

• cfg.armMin d v = min (d.length (cfg.firstArm v)) (d.length (cfg.secondArm v))

def AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerHeight {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : ℕ

Height at the partner centre.

Equations

• cfg.partnerHeight d center = min (cfg.armMin d center) (cfg.armMin d (cfg.partner center))

def AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : ℕ

Height at the requested centre.

Equations

• cfg.targetHeight d center = min (cfg.armMin d center) (cfg.partnerHeight d center + d.length (cfg.middleSlot center))

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.armMin_le_first {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (v : Fin n) : cfg.armMin d v ≤ d.length (cfg.firstArm v)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.armMin_le_second {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (v : Fin n) : cfg.armMin d v ≤ d.length (cfg.secondArm v)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.armMin_eq_first_or_second {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (v : Fin n) : cfg.armMin d v = d.length (cfg.firstArm v) ∨ cfg.armMin d v = d.length (cfg.secondArm v)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerHeight_le_targetArmMin {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.partnerHeight d center ≤ cfg.armMin d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerHeight_le_partnerArmMin {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.partnerHeight d center ≤ cfg.armMin d (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight_le_armMin {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.targetHeight d center ≤ cfg.armMin d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerHeight_le_targetHeight {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.partnerHeight d center ≤ cfg.targetHeight d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight_sub_partnerHeight_le_middle {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.targetHeight d center - cfg.partnerHeight d center ≤ d.length (cfg.middleSlot center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight_eq_armMin_or_full_middle {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.targetHeight d center = cfg.armMin d center ∨ cfg.targetHeight d center = cfg.partnerHeight d center + d.length (cfg.middleSlot center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerHeight_eq_partnerArmMin_of_lt {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hLt : cfg.partnerHeight d center < cfg.targetHeight d center) : cfg.partnerHeight d center = cfg.armMin d (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight_eq_partnerHeight_of_middle_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hZero : d.length (cfg.middleSlot center) = 0) : cfg.targetHeight d center = cfg.partnerHeight d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight_eq_min_armMins_of_middle_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hMiddleZero : d.length (cfg.middleSlot center) = 0) : cfg.targetHeight d center = min (cfg.armMin d center) (cfg.armMin d (cfg.partner center))

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight_le_middle_of_partnerHeight_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hPartnerHeight : cfg.partnerHeight d center = 0) : cfg.targetHeight d center ≤ d.length (cfg.middleSlot center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerHeight_eq_zero_of_firstPartnerArm_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hZero : d.length (cfg.firstArm (cfg.partner center)) = 0) : cfg.partnerHeight d center = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerHeight_eq_zero_of_secondPartnerArm_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hZero : d.length (cfg.secondArm (cfg.partner center)) = 0) : cfg.partnerHeight d center = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.armMin_pos {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) : 0 < cfg.armMin d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetHeight_pos {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) : 0 < cfg.targetHeight d center

Which core classes a chip-free centre can meet

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.adjacent_pair_or_chip {n p : ℕ} (cfg : ConfigThree n p) {l : List (Fin p)} {center u v : Fin n} (hCenter : cfg.isCenter center = true) (hPair : u = center ∨ u = cfg.partner center) (hAdjacent : Utilities.Certificate.ContractionForestCensusGeneral.AdjInList cfg.core l u v) : cfg.IsChip v ∨ v = center ∨ v = cfg.partner center

From one of the two chip-free centres, every step either lands on a chip or stays in that two-vertex pair.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.reach_mem_pair_of_no_chip {n p : ℕ} (cfg : ConfigThree n p) {F : Finset (Fin p)} {center v : Fin n} (hCenter : cfg.isCenter center = true) (hNoChip : ∀ (s : Fin n), cfg.IsChip s → ¬Utilities.Certificate.ContractionForestCensusGeneral.ReachIn cfg.core F center s) (hReach : Utilities.Certificate.ContractionForestCensusGeneral.ReachIn cfg.core F center v) : v = center ∨ v = cfg.partner center

A zero-edge class with no chip consists only of the two centres in one configuration-3 component.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.rep_eq_center_or_partner_of_divisor_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (F : Finset (Fin p)) (hRepReach : ∀ (x y : Fin n), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn cfg.core F x y) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) {v : Fin n} (hEq : d.rep v = d.rep center) : v = center ∨ v = cfg.partner center

A zero-divisor core class is contained in its displayed centre pair.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.reach_eq_center_of_slots_positive {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (F : Finset (Fin p)) (hFZero : ∀ (e : Fin p), e ∈ F ↔ d.length e = 0) {center v : Fin n} (hCenter : cfg.isCenter center = true) (hFirst : 0 < d.length (cfg.firstArm center)) (hSecond : 0 < d.length (cfg.secondArm center)) (hMiddle : 0 < d.length (cfg.middleSlot center)) (hReach : Utilities.Certificate.ContractionForestCensusGeneral.ReachIn cfg.core F center v) : v = center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.singleton_class_of_slots_positive {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (F : Finset (Fin p)) (hRepReach : ∀ (x y : Fin n), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn cfg.core F x y) (hFZero : ∀ (e : Fin p), e ∈ F ↔ d.length e = 0) {center : Fin n} (hCenter : cfg.isCenter center = true) (hFirst : 0 < d.length (cfg.firstArm center)) (hSecond : 0 < d.length (cfg.secondArm center)) (hMiddle : 0 < d.length (cfg.middleSlot center)) (v : Fin n) : d.rep v = d.rep center ↔ v = center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.firstPartnerChip_rep_eq_of_length_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : d.length (cfg.firstArm (cfg.partner center)) = 0) : d.rep (cfg.firstChip (cfg.partner center)) = d.rep (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.secondPartnerChip_rep_eq_of_length_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : d.length (cfg.secondArm (cfg.partner center)) = 0) : d.rep (cfg.secondChip (cfg.partner center)) = d.rep (cfg.partner center)

The five active slots of a configuration-3 component

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.firstArm_ne_middleSlot {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.firstArm center ≠ cfg.middleSlot center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.secondArm_ne_middleSlot {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.secondArm center ≠ cfg.middleSlot center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.center_ne_partnerFirstChip {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : center ≠ cfg.firstChip (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.center_ne_partnerSecondChip {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : center ≠ cfg.secondChip (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.firstArm_ne_partnerFirstArm {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.firstArm center ≠ cfg.firstArm (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.firstArm_ne_partnerSecondArm {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.firstArm center ≠ cfg.secondArm (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.secondArm_ne_partnerFirstArm {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.secondArm center ≠ cfg.firstArm (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.secondArm_ne_partnerSecondArm {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.secondArm center ≠ cfg.secondArm (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.middleSlot_ne_partnerFirstArm {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.middleSlot center ≠ cfg.firstArm (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.middleSlot_ne_partnerSecondArm {n p : ℕ} (cfg : ConfigThree n p) {center : Fin n} (hCenter : cfg.isCenter center = true) : cfg.middleSlot center ≠ cfg.secondArm (cfg.partner center)

Splitting the endpoint sum

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_eq_center_slots {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) (potential : Fin n → ℤ) {center : Fin n} (hCenter : cfg.isCenter center = true) : ConfigurationCommon.endpointContribution d potential center = slotTerm d potential (cfg.firstArm center) center + slotTerm d potential (cfg.secondArm center) center + slotTerm d potential (cfg.middleSlot center) center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_eq_partner_slots {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) (potential : Fin n → ℤ) {center : Fin n} (hCenter : cfg.isCenter center = true) : ConfigurationCommon.endpointContribution d potential (cfg.partner center) = slotTerm d potential (cfg.firstArm (cfg.partner center)) (cfg.partner center) + slotTerm d potential (cfg.secondArm (cfg.partner center)) (cfg.partner center) + slotTerm d potential (cfg.middleSlot center) (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.middleSlot_terms_cancel {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) (potential : Fin n → ℤ) {center : Fin n} (hCenter : cfg.isCenter center = true) (hMiddleZero : d.length (cfg.middleSlot center) = 0) : slotTerm d potential (cfg.middleSlot center) center + slotTerm d potential (cfg.middleSlot center) (cfg.partner center) = 0

Both endpoint terms of a collapsed middle slot cancel.

The interpolated potentials

def AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center v : Fin n) : ℤ

The closed-face core potential for configuration 3.

Equations

• cfg.pairPotential d center v = if d.rep v = d.rep center then -↑(cfg.targetHeight d center) else if d.rep v = d.rep (cfg.partner center) then -↑(cfg.partnerHeight d center) else 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential_repInvariant {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : d.RepInvariant (cfg.pairPotential d center)

@[reducible, inline]

abbrev AtanasovRanganathan.ConfigurationThree.ConfigThree.targetOnlyPotential {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : Fin n → ℤ

The potential used when only the target class fires.

Equations

• cfg.targetOnlyPotential d center = AtanasovRanganathan.ConfigurationCommon.centerPotential d center (cfg.targetHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential_center {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.pairPotential d center center = -↑(cfg.targetHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential_partner {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hne : d.rep (cfg.partner center) ≠ d.rep center) : cfg.pairPotential d center (cfg.partner center) = -↑(cfg.partnerHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential_partner_merged {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hMerged : d.rep (cfg.partner center) = d.rep center) : cfg.pairPotential d center (cfg.partner center) = -↑(cfg.targetHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential_eq_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) {v : Fin n} (h1 : d.rep v ≠ d.rep center) (h2 : d.rep v ≠ d.rep (cfg.partner center)) : cfg.pairPotential d center v = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.rep_partner_ne {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) (hCenter : cfg.isCenter center = true) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) : d.rep (cfg.partner center) ≠ d.rep center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.rep_chip_ne_center {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) {chip : Fin n} (hChip : cfg.IsChip chip) (hCenter : cfg.isCenter center = true) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) : d.rep chip ≠ d.rep center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential_chip_eq_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) {chip : Fin n} (hChip : cfg.IsChip chip) (hCenter : cfg.isCenter center = true) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : cfg.pairPotential d center chip = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pairPotential_chip_eq_zero_merged {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) {chip : Fin n} (hChip : cfg.IsChip chip) (hCenter : cfg.isCenter center = true) (hMerged : d.rep (cfg.partner center) = d.rep center) (hClass : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center ∨ v = cfg.partner center) : cfg.pairPotential d center chip = 0

The three arm contributions at each centre

def AtanasovRanganathan.ConfigurationThree.ConfigThree.middleTargetContribution {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : ℤ

Contribution at the requested centre from the middle slot.

Equations

• cfg.middleTargetContribution d center = AtanasovRanganathan.ConfigurationThree.slotValue d center (cfg.middleSlot center) (-↑(cfg.targetHeight d center)) (-↑(cfg.partnerHeight d center))

def AtanasovRanganathan.ConfigurationThree.ConfigThree.middlePartnerContribution {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : ℤ

Contribution at the partner from the same interpolated middle slot.

Equations

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

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.middleTargetContribution_nonneg {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {center : Fin n} (hMiddlePos : 0 < d.length (cfg.middleSlot center)) : 0 ≤ cfg.middleTargetContribution d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.middleTargetContribution_eq_one_of_full {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {center : Fin n} (hFull : cfg.targetHeight d center = cfg.partnerHeight d center + d.length (cfg.middleSlot center)) (hLength : 0 < d.length (cfg.middleSlot center)) : cfg.middleTargetContribution d center = 1

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.middlePartnerContribution_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {center : Fin n} (hMiddlePos : 0 < d.length (cfg.middleSlot center)) : cfg.middlePartnerContribution d center = -drain (cfg.targetHeight d center - cfg.partnerHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetOnlyPotential_center {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) : cfg.targetOnlyPotential d center center = -↑(cfg.targetHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetOnlyPotential_eq_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (center : Fin n) {v : Fin n} (h : d.rep v ≠ d.rep center) : cfg.targetOnlyPotential d center v = 0

The endpoint contribution at each of the two centres

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_target_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) center = armContribution d center (cfg.firstArm center) (cfg.targetHeight d center) + armContribution d center (cfg.secondArm center) (cfg.targetHeight d center) + cfg.middleTargetContribution d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_partner_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) (cfg.partner center) = armContribution d (cfg.partner center) (cfg.firstArm (cfg.partner center)) (cfg.partnerHeight d center) + armContribution d (cfg.partner center) (cfg.secondArm (cfg.partner center)) (cfg.partnerHeight d center) + cfg.middlePartnerContribution d center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_merged_eq_arms {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hMerged : d.rep (cfg.partner center) = d.rep center) (hClass : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center ∨ v = cfg.partner center) (hMiddleZero : d.length (cfg.middleSlot center) = 0) : ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) center + ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) (cfg.partner center) = armContribution d center (cfg.firstArm center) (cfg.targetHeight d center) + armContribution d center (cfg.secondArm center) (cfg.targetHeight d center) + armContribution d (cfg.partner center) (cfg.firstArm (cfg.partner center)) (cfg.targetHeight d center) + armContribution d (cfg.partner center) (cfg.secondArm (cfg.partner center)) (cfg.targetHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_targetOnly_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hSingleton : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) : ConfigurationCommon.endpointContribution d (cfg.targetOnlyPotential d center) center = armContribution d center (cfg.firstArm center) (cfg.targetHeight d center) + armContribution d center (cfg.secondArm center) (cfg.targetHeight d center) + armContribution d center (cfg.middleSlot center) (cfg.targetHeight d center)

The chip actually delivered to each centre

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_target_ge_one {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) (hMiddlePos : 0 < d.length (cfg.middleSlot center)) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : 1 ≤ ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) center

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerFirstArm_length_pos {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : 0 < d.length (cfg.firstArm (cfg.partner center))

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.partnerSecondArm_length_pos {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : 0 < d.length (cfg.secondArm (cfg.partner center))

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_partner_nonneg {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hMiddlePos : 0 < d.length (cfg.middleSlot center)) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : 0 ≤ ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_merged_ge_one {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) (hMiddleZero : d.length (cfg.middleSlot center) = 0) (hMerged : d.rep (cfg.partner center) = d.rep center) (hClass : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center ∨ v = cfg.partner center) : 1 ≤ ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) center + ConfigurationCommon.endpointContribution d (cfg.pairPotential d center) (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.middleArmContribution_nonneg {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {center : Fin n} (hPartnerHeight : cfg.partnerHeight d center = 0) (hMiddlePos : 0 < d.length (cfg.middleSlot center)) : 0 ≤ armContribution d center (cfg.middleSlot center) (cfg.targetHeight d center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointContribution_targetOnly_ge_one {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) (hPartnerHeight : cfg.partnerHeight d center = 0) (hMiddlePos : 0 < d.length (cfg.middleSlot center)) (hSingleton : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) : 1 ≤ ConfigurationCommon.endpointContribution d (cfg.targetOnlyPotential d center) center

The Laplacian away from the fired classes

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.coreRise_eq_zero_of_not_active {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {potential : Fin n → ℤ} {center : Fin n} (hCenter : cfg.isCenter center = true) (hSupport : ∀ (v : Fin n), v ≠ center → v ≠ cfg.partner center → potential v = 0) {e : Fin p} (h1 : e ≠ cfg.firstArm center) (h2 : e ≠ cfg.secondArm center) (h3 : e ≠ cfg.middleSlot center) (h4 : e ≠ cfg.firstArm (cfg.partner center)) (h5 : e ≠ cfg.secondArm (cfg.partner center)) : d.coreRise potential e = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.coreRise_eq_zero_of_not_center {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {potential : Fin n → ℤ} {center : Fin n} (hCenter : cfg.isCenter center = true) (hSupport : ∀ (v : Fin n), v ≠ center → potential v = 0) {e : Fin p} (h1 : e ≠ cfg.firstArm center) (h2 : e ≠ cfg.secondArm center) (h3 : e ≠ cfg.middleSlot center) : d.coreRise potential e = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.endpointPair_middle_eq_zero {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (potential : Fin n → ℤ) (r : Fin n) (h1 : d.rep center ≠ d.rep r) (h2 : d.rep (cfg.partner center) ≠ d.rep r) : ConfigurationCommon.endpointPair d potential (cfg.middleSlot center) r = 0

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.prin_pair_nonTarget_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hHeightPos : 0 < cfg.targetHeight d center) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) (hPartnerFirstLength : 0 < d.length (cfg.firstArm (cfg.partner center))) (hPartnerSecondLength : 0 < d.length (cfg.secondArm (cfg.partner center))) (r : Fin n) (hNotTarget : d.rep r ≠ d.rep center) (hNotPartner : d.rep r ≠ d.rep (cfg.partner center)) : (prin d.graph) (d.interpolatedScript (cfg.pairPotential d center)) (d.coreVertex r) = -chipInd d r (cfg.firstChip center) - chipInd d r (cfg.secondChip center) - drain (cfg.partnerHeight d center) * (chipInd d r (cfg.firstChip (cfg.partner center)) + chipInd d r (cfg.secondChip (cfg.partner center)))

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.prin_targetOnly_nonTarget_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hHeightPos : 0 < cfg.targetHeight d center) (hPartnerHeight : cfg.partnerHeight d center = 0) (hMiddlePos : 0 < d.length (cfg.middleSlot center)) (hSingleton : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (r : Fin n) (hNotTarget : d.rep r ≠ d.rep center) : (prin d.graph) (d.interpolatedScript (cfg.targetOnlyPotential d center)) (d.coreVertex r) = -chipInd d r (cfg.firstChip center) - chipInd d r (cfg.secondChip center) - chipInd d r (cfg.partner center)

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.prin_merged_nonTarget_eq {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hMiddleZero : d.length (cfg.middleSlot center) = 0) (hMerged : d.rep (cfg.partner center) = d.rep center) (hClass : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center ∨ v = cfg.partner center) (hHeightPos : 0 < cfg.targetHeight d center) (r : Fin n) (hNotClass : d.rep r ≠ d.rep center) : (prin d.graph) (d.interpolatedScript (cfg.pairPotential d center)) (d.coreVertex r) = -chipInd d r (cfg.firstChip center) - chipInd d r (cfg.secondChip center) - chipInd d r (cfg.firstChip (cfg.partner center)) - chipInd d r (cfg.secondChip (cfg.partner center))

Effectivity of the residual divisor

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.residual_effective_of_coreVertex {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (center : Fin n) (hCoreCase : ∀ (r : Fin n), 0 ≤ cfg.divisor d (d.coreVertex r) - oneChip (d.coreVertex center) (d.coreVertex r) + (prin d.graph) (d.interpolatedScript potential) (d.coreVertex r)) : effective (cfg.divisor d - oneChip (d.coreVertex center) + (prin d.graph) (d.interpolatedScript potential))

Only the contracted core classes need checking: at a subdivision-interior vertex the interpolated script is nonnegative for free.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.pair_residual_effective {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) (hMiddlePos : 0 < d.length (cfg.middleSlot center)) (hTarget : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartner : ∀ (v : Fin n), d.rep v = d.rep (cfg.partner center) ↔ v = cfg.partner center) : effective (cfg.divisor d - oneChip (d.coreVertex center) + (prin d.graph) (d.interpolatedScript (cfg.pairPotential d center)))

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.targetOnly_residual_effective {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) (hPartnerHeight : cfg.partnerHeight d center = 0) (hMiddlePos : 0 < d.length (cfg.middleSlot center)) (hSingleton : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center) (hPartnerChip : d.rep (cfg.firstChip (cfg.partner center)) = d.rep (cfg.partner center) ∨ d.rep (cfg.secondChip (cfg.partner center)) = d.rep (cfg.partner center)) : effective (cfg.divisor d - oneChip (d.coreVertex center) + (prin d.graph) (d.interpolatedScript (cfg.targetOnlyPotential d center)))

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.merged_residual_effective {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) {center : Fin n} (hCenter : cfg.isCenter center = true) (hZero : cfg.divisor d (d.coreVertex center) = 0) (hMiddleZero : d.length (cfg.middleSlot center) = 0) (hMerged : d.rep (cfg.partner center) = d.rep center) (hClass : ∀ (v : Fin n), d.rep v = d.rep center ↔ v = center ∨ v = cfg.partner center) : effective (cfg.divisor d - oneChip (d.coreVertex center) + (prin d.graph) (d.interpolatedScript (cfg.pairPotential d center)))

The configuration-3 divisor reaches every contracted class

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.reaches_center {n p : ℕ} (cfg : ConfigThree n p) (d : Utilities.Certificate.DegenerateSpec.DegSpec n p) (hCore : d.core = cfg.core) (F : Finset (Fin p)) (hRepReach : ∀ (x y : Fin n), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn cfg.core F x y) (hFZero : ∀ (e : Fin p), e ∈ F ↔ d.length e = 0) {center : Fin n} (hCenter : cfg.isCenter center = true) : Utilities.Certificate.StrongSeparator.Reaches d.graph (cfg.divisor d) (d.coreVertex center)

Configuration 3 at one declared centre. This is the statement a row consumes, one centre at a time, so that several local pictures compose.

theorem AtanasovRanganathan.ConfigurationThree.ConfigThree.closedConstruction {n p : ℕ} (cfg : ConfigThree n p) (core_nonempty : 0 < n) (hConnected : cfg.core.Connected) (hCenters : ∀ (v : Fin n), ¬cfg.IsChip v → cfg.isCenter v = true) : Configurations.ClosedSubdivisionDharConstruction cfg.core core_nonempty

Configuration 3 on a closed face. A row every one of whose chip-free vertices is a declared centre gets the whole closed-orthant AR construction.

core_nonempty is the one place in this file where the core size is used at all. It used to be 0 < 8, discharged by norm_num; it is now a hypothesis, exactly as in Guarding.GuardingSet.closedConstruction.