AR row 08, chamber 3

The third scope AR draw for their seventh family: |e3| ≤ |e4| and |e7| ≤ |e2|, i.e. b ≤ a and d ≤ c. This is the scope whose caption notes that "the last divisor has two chips placed on the same vertex":

 D = 2 * [5] + [3] + (e4 at distance |e3| from 1)

so there is a single mark, mark e4 = |e3| (measured from e4's tail 1), and the divisor is markedDivisorOne rather than markedDivisorTwo. The six chip-free vertices split as

• {0, 1} -- a banana pair whose two arms both have length |e3|: the whole of e3 read from its head 0, and the near half of e4.
• {2, 4} -- a ConfigurationThree pair across e5 : 2 → 4; vertex 2's arms are e9 (to the chip 3) and e8 (to the double chip 5), vertex 4's are e6 (to 5) and the far half of e4 (to the marked chip). The chip vertex 5 is the endpoint of two arms but carries two chips, which is exactly what ConfigurationMarkedThree's chipSum-with-multiplicity phrasing was designed for.
• {6, 7} -- a lopsided banana pair: vertex 6's arm is the whole of e2 (length c, to the chip 3) and vertex 7's is the whole of e7 (length d ≤ c, to the double chip 5). The short-arm vertex 7 is reached by the ordinary equal-arm minimum; the far vertex 6 needs the second profile of ConfigurationBananaDoubleChip, and only the double chip makes it possible.

The fourth sign pattern |e4| ≤ |e3|, |e2| ≤ |e7| is the sigma image of this chamber and is discharged by GenusFiveRow08Symmetry.chamber_covers together with ClosedOrbit.closedConstruction_of_chamber; there is no chamber-4 file.

The single mark

def AtanasovRanganathan.GenusFiveRow08ChamberThree.markY (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The chip on e4, at distance |e3| from the tail 1.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.markY d = d.length 3

def AtanasovRanganathan.GenusFiveRow08ChamberThree.rowMark (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (e : Fin 12) : ℕ

The third chamber marks only slot 4, at offset markY; other slots receive offset zero.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.rowMark d e = if e = 4 then AtanasovRanganathan.GenusFiveRow08ChamberThree.markY d else 0

@[simp]

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rowMark_four (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : rowMark d 4 = markY d

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rowMark_other (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} (h4 : e ≠ 4) : rowMark d e = 0

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.marked_of_rowMark_pos (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} (h : 0 < rowMark d e) : e = 4

The core, spelled out

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.tail_four {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.tail 4 = 1

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.head_four {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.head 4 = 4

The heights

def AtanasovRanganathan.GenusFiveRow08ChamberThree.armTwo (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Vertex 2's arm minimum: e9 to the chip 3, e8 to the double chip 5.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.armTwo d = min (d.length 9) (d.length 8)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.armFour (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Vertex 4's arm minimum: e6 to the double chip 5, and the far half of the marked slot e4.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.armFour d = min (d.length 6) (d.length 4 - AtanasovRanganathan.GenusFiveRow08ChamberThree.markY d)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.pairLow (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The smaller effective arm at vertices 2 and 4, used as the shared height of their pair configuration.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.pairLow d = min (AtanasovRanganathan.GenusFiveRow08ChamberThree.armTwo d) (AtanasovRanganathan.GenusFiveRow08ChamberThree.armFour d)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.targetTwo (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Target height at vertex 2, capped by its effective arm and by the shared height plus the length of connecting slot 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.targetFour (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Target height at vertex 4, capped by its effective arm and by the shared height plus the length of connecting slot 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.bananaPar (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The shorter of the two right-banana slots.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.bananaPar d = min (d.length 10) (d.length 11)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.bananaLow (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The equal-arm reading of the right banana pair, which reaches its short-arm vertex 7.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.bananaLow d = min (d.length 2) (d.length 7)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.nearSeven (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The near vertex 7 under the double-chip profile.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.nearSeven d = AtanasovRanganathan.ConfigurationBananaDoubleChip.nearHeight (d.length 2) (d.length 7)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.farSix (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The far vertex 6 under the double-chip profile.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.heightLB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The left banana pair, both arms of length |e3|.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.heightT2 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The {2,4} pair read at the target 2.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.heightT4 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The {2,4} pair read at the target 4.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.heightRB7 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The right banana pair read at its short-arm vertex 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.heightRB6 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The right banana pair read at the far vertex 6, under the double chip.

Equations

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

Profiles

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.mkProfile {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) {h : Fin 8 → ℕ} (hin : h 1 ≤ markY d) (hout : h 4 ≤ d.length 4 - markY d) (hflat : h 1 = 0 ∨ h 4 = 0) (hconst : ∀ (e : Fin 12), d.length e = 0 → h (GenusFiveCoreAtlas.row08Core.tail e) = h (GenusFiveCoreAtlas.row08Core.head e)) : ConfigurationMarkedRow.Profile d (rowMark d) h

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.profileLB {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) : ConfigurationMarkedRow.Profile d (rowMark d) (heightLB d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.profileT2 {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) : ConfigurationMarkedRow.Profile d (rowMark d) (heightT2 d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.profileT4 {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) : ConfigurationMarkedRow.Profile d (rowMark d) (heightT4 d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.profileRB7 {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hD : d.length 7 ≤ d.length 2) : ConfigurationMarkedRow.Profile d (rowMark d) (heightRB7 d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.profileRB6 {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hD : d.length 7 ≤ d.length 2) : ConfigurationMarkedRow.Profile d (rowMark d) (heightRB6 d)

The endpoint ledger, vertex by vertex

def AtanasovRanganathan.GenusFiveRow08ChamberThree.contribForm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (h : Fin 8 → ℕ) (v : Fin 8) : ℤ

Incident-slot contribution at each row-08 core vertex in chamber three, with the marked slot 4 evaluated by its split-ramp formula.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.contrib_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) {h : Fin 8 → ℕ} (hprof : ConfigurationMarkedRow.Profile d (rowMark d) h) (hRep : ∀ (v : Fin 8), h (d.rep v) = h v) (v : Fin 8) : ConfigurationMarkedThree.positiveEndpointContribution d (ConfigurationMarkedRow.heightPotential d h) (rowMark d) (ConfigurationMarkedRow.markValue d (rowMark d) h) v = contribForm d h v

The divisor

def AtanasovRanganathan.GenusFiveRow08ChamberThree.chipWeight (v : Fin 8) : ℤ

Core-supported part of the third-chamber divisor: two chips at vertex 5 and one at vertex 3.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.chipWeight v = if v = 5 then 2 else if v = 3 then 1 else 0

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.chipWeight_nonneg (v : Fin 8) : 0 ≤ chipWeight v

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.sum_chipWeight : ∑ v : Fin 8, chipWeight v = 3

def AtanasovRanganathan.GenusFiveRow08ChamberThree.rowDivisor (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : CFDiv d.graph

AR's divisor on chamber 3: a double chip at 5, one chip at 3, and one inside the left-top leg.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.base (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8 → ℤ

Base core weight formed from the three core chips and the endpoint contribution of the marked chip on slot 4.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rowDivisor_effective (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : effective (rowDivisor d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rowDivisor_degree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : CFDiv.degree (rowDivisor d) = 4

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.base_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (v : Fin 8) : base d v = chipWeight v + if markY d = 0 then if v = 1 then 1 else 0 else if d.length 4 ≤ markY d then if v = 4 then 1 else 0 else 0

Chip allocations

Two of the five profiles move chips inside a contracted class: the {2,4} pair and the double-chip banana. Both transfers leave every class sum unchanged.

def AtanasovRanganathan.GenusFiveRow08ChamberThree.pairAlloc (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

The allocation the {2,4} pair script uses.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberThree.bananaAlloc (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

The allocation the double-chip banana script uses: the chip at 3 follows a collapsed e2 onto 6, and both chips at 5 follow a collapsed e7 onto 7.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.pairAlloc_classSum {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, pairAlloc d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.bananaAlloc_classSum {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, bananaAlloc d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

The left banana pair

def AtanasovRanganathan.GenusFiveRow08ChamberThree.lbCoeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded core coefficients after the left-banana height script, combining the base with endpoint contributions. lbCoeff_eq identifies this formula with the script computation.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.lbCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) (v : Fin 8) : base d v + contribForm d (heightLB d) v = lbCoeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.lbCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hB : d.length 3 ≤ d.length 4) (v : Fin 8) : 0 ≤ lbCoeff d v

def AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerZero (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Target representative for vertex 0, moved to vertex 3 when slot 3 is contracted.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerZero d = if d.length 3 = 0 then 3 else 0

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.lbCoeff_owner_zero {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ lbCoeff d (ownerZero d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.lbCoeff_owner_one {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ lbCoeff d 1

The {2,4} pair

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.pairLow_comm (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : pairLow d = min (armFour d) (armTwo d)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.t2Coeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded core coefficients after the vertex-2 height script, combining the pair allocation with endpoint contributions. t2Coeff_eq identifies this formula with the script computation.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.t2Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) (v : Fin 8) : pairAlloc d v + contribForm d (heightT2 d) v = t2Coeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.t2Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hB : d.length 3 ≤ d.length 4) (v : Fin 8) : 0 ≤ t2Coeff d v

def AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerTwo (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Target representative for vertex 2, moved to vertex 4 when connecting slot 5 is contracted and the effective arm at vertex 2 is longer.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.t2Coeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ t2Coeff d (ownerTwo d)

def AtanasovRanganathan.GenusFiveRow08ChamberThree.t4Coeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded core coefficients after the vertex-4 height script, combining the pair allocation with endpoint contributions. t4Coeff_eq identifies this formula with the script computation.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.t4Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) (v : Fin 8) : pairAlloc d v + contribForm d (heightT4 d) v = t4Coeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.t4Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hB : d.length 3 ≤ d.length 4) (v : Fin 8) : 0 ≤ t4Coeff d v

def AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerFour (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Target representative for vertex 4, moved to vertex 2 when connecting slot 5 is contracted and the effective arm at vertex 4 is longer.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.t4Coeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ t4Coeff d (ownerFour d)

The right banana pair, short-arm reading

def AtanasovRanganathan.GenusFiveRow08ChamberThree.rb7Coeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded core coefficients after the right-banana vertex-7 height script, combining the base with endpoint contributions. rb7Coeff_eq identifies this formula with the script computation.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rb7Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (_hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) (v : Fin 8) : base d v + contribForm d (heightRB7 d) v = rb7Coeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rb7Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (_hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) (v : Fin 8) : 0 ≤ rb7Coeff d v

def AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerSeven (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Target representative for vertex 7, moved to vertex 5 when slot 7 is contracted.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerSeven d = if d.length 7 = 0 then 5 else 7

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rb7Coeff_owner_seven {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hD : d.length 7 ≤ d.length 2) : 1 ≤ rb7Coeff d (ownerSeven d)

The right banana pair, far reading under the double chip

def AtanasovRanganathan.GenusFiveRow08ChamberThree.rb6Coeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded core coefficients after the right-banana vertex-6 height script, combining the adjusted allocation with endpoint contributions. rb6Coeff_eq identifies this formula with the script computation.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rb6Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (_hB : d.length 3 ≤ d.length 4) (_hD : d.length 7 ≤ d.length 2) (v : Fin 8) : bananaAlloc d v + contribForm d (heightRB6 d) v = rb6Coeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.near_le_far (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : nearSeven d ≤ farSix d

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.near_le_two (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : nearSeven d ≤ 2 * d.length 7

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.far_le_long (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : farSix d ≤ d.length 2

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rb6Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hD : d.length 7 ≤ d.length 2) (v : Fin 8) : 0 ≤ rb6Coeff d v

def AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerSix (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Target representative for vertex 6: keep vertex 6 when both parallel banana slots have positive length, and use vertex 7 otherwise.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberThree.ownerSix d = if 0 < AtanasovRanganathan.GenusFiveRow08ChamberThree.bananaPar d then 6 else 7

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rb6Coeff_owner_six {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hD : d.length 7 ≤ d.length 2) : 1 ≤ rb6Coeff d (ownerSix d)

Every contracted core class is reached

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.rowDivisor_reaches_coreVertex {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hD : d.length 7 ≤ d.length 2) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row08Core F x y) (hFZero : ∀ (e : Fin 12), e ∈ F ↔ d.length e = 0) (center : Fin 8) : Utilities.Certificate.StrongSeparator.Reaches d.graph (rowDivisor d) (d.coreVertex center)

theorem AtanasovRanganathan.GenusFiveRow08ChamberThree.chamberThree_pencil (length : Fin 12 → ℕ) (forest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest GenusFiveCoreAtlas.row08Core (Configurations.zeroSlots length)) (notLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy GenusFiveCoreAtlas.row08Core (Configurations.zeroSlots length)) (hP : GenusFiveRow08Symmetry.ChamberThree length) : Nonempty (Configurations.DegreeFourDharPencil (Configurations.faceSpec GenusFiveCoreAtlas.row08Core chamberThree_pencil._proof_1 length forest notLoopy).graph)

AR's seventh family, third scope. The divisor with a double chip.