AR row 08, chamber 2

The second scope AR draw for their seventh family: |e3| ≤ |e4| and |e2| ≤ |e7|, i.e. b ≤ a and c ≤ d. The displayed divisor is

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

so the two marks are mark e4 = |e3| (from e4's tail 1) and mark e7 = |e7| - |e2| (from e7's tail 5). The six chip-free vertices are

• {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.
• {6, 7} -- a banana pair whose two arms both have length |e2|: the whole of e2 read from its tail 6, and the far half of e7.
• {4, 5} -- not a pair. Both would have an arm into the same chip vertex 2, which carries only one chip, so ConfigurationThree's chipSum fails and the profile drives 2 to -1. AR's own solid subgraph here is the chipped triangle 2 - 4 - 5, one chip on 2 and one arm from each triangle vertex; that is ConfigurationChippedTriangle, read once at u = 4 and once at u = 5. Its docstring records the two repairs that do not work.

The triangle data at the target 4 is al = |e4| - |e3| (the far half of the marked e4), be = |e7| - |e2| (the near half of the marked e7), ga = |e9|, and the triangle slots p = |e5|, q = |e6|, r = |e8|; at the target 5 the same picture is read with al ↔ be and p ↔ r.

The two marks

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

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

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.markX (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The chip on e7, at distance |e7| - |e2| from the tail 5.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberTwo.markX d = d.length 7 - d.length 2

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.armAl (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The far half of the marked e4: the target 4's own arm.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberTwo.armAl d = d.length 4 - AtanasovRanganathan.GenusFiveRow08ChamberTwo.markY d

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

The second chamber marks slot 4 at markY and slot 7 at markX; other slots receive offset zero.

Equations

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

@[simp]

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

@[simp]

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.rowMark_seven (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : rowMark d 7 = markX d

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

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

The core, spelled out

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

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.tail_seven {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.tail 7 = 5

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.head_seven {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.head 7 = 7

The heights

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.hcT4 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The chipped-triangle profile read at the target 4.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.h0T4 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Auxiliary side height for the configuration targeting vertex 4, using its effective arm, the right mark, and slots 9 and 8.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.htT4 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Height at the target vertex 4 supplied by the marked configuration, with slots 5 and 6 bounding the target and slot 8 bounding its partner.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.hvT4 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Height at the partner vertex 5 in the marked configuration targeting vertex 4.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.hcT5 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The same picture read at the target 5: al ↔ be, p ↔ r.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.h0T5 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Auxiliary side height for the configuration targeting vertex 5, obtained by exchanging the two arms and using slots 9 and 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.htT5 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Height at the target vertex 5 supplied by the marked configuration after exchanging the two arms and the roles of slots 5 and 8.

Equations

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

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.hvT5 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Height at the partner vertex 4 in the marked configuration targeting vertex 5.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.boundsT4 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : (hcT4 d ≤ d.length 9 ∧ hcT4 d ≤ armAl d ∧ hcT4 d ≤ markX d) ∧ (hcT4 d = d.length 9 ∨ hcT4 d = armAl d ∨ hcT4 d = markX d) ∧ (h0T4 d ≤ markX d ∧ h0T4 d ≤ hcT4 d + d.length 8 ∧ hcT4 d ≤ h0T4 d) ∧ (h0T4 d = markX d ∨ h0T4 d = hcT4 d + d.length 8) ∧ (htT4 d ≤ armAl d ∧ htT4 d ≤ hcT4 d + d.length 5 ∧ htT4 d ≤ h0T4 d + d.length 6 ∧ hcT4 d ≤ htT4 d) ∧ (htT4 d = armAl d ∨ htT4 d = hcT4 d + d.length 5 ∨ htT4 d = h0T4 d + d.length 6) ∧ (hvT4 d ≤ h0T4 d ∧ hvT4 d ≤ htT4 d ∧ hcT4 d ≤ hvT4 d ∧ htT4 d ≤ hvT4 d + d.length 6 ∧ hvT4 d ≤ hcT4 d + d.length 8 ∧ hvT4 d ≤ markX d) ∧ (hvT4 d = h0T4 d ∨ hvT4 d = htT4 d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.boundsT5 (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : (hcT5 d ≤ d.length 9 ∧ hcT5 d ≤ markX d ∧ hcT5 d ≤ armAl d) ∧ (hcT5 d = d.length 9 ∨ hcT5 d = markX d ∨ hcT5 d = armAl d) ∧ (h0T5 d ≤ armAl d ∧ h0T5 d ≤ hcT5 d + d.length 5 ∧ hcT5 d ≤ h0T5 d) ∧ (h0T5 d = armAl d ∨ h0T5 d = hcT5 d + d.length 5) ∧ (htT5 d ≤ markX d ∧ htT5 d ≤ hcT5 d + d.length 8 ∧ htT5 d ≤ h0T5 d + d.length 6 ∧ hcT5 d ≤ htT5 d) ∧ (htT5 d = markX d ∨ htT5 d = hcT5 d + d.length 8 ∨ htT5 d = h0T5 d + d.length 6) ∧ (hvT5 d ≤ h0T5 d ∧ hvT5 d ≤ htT5 d ∧ hcT5 d ≤ hvT5 d ∧ htT5 d ≤ hvT5 d + d.length 6 ∧ hvT5 d ≤ hcT5 d + d.length 5 ∧ hvT5 d ≤ armAl d) ∧ (hvT5 d = h0T5 d ∨ hvT5 d = htT5 d)

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.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.GenusFiveRow08ChamberTwo.heightRB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℕ

The right banana pair, both arms of length |e2|.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberTwo.heightRB d v = if v = 6 then d.length 2 else if v = 7 then d.length 2 else 0

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

The chipped triangle read at the target 4.

Equations

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

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

The chipped triangle read at the target 5.

Equations

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

Profiles

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.mkProfile {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hC : d.length 2 ≤ d.length 7) {h : Fin 8 → ℕ} (hin4 : h 1 ≤ markY d) (hout4 : h 4 ≤ d.length 4 - markY d) (hflat4 : h 1 = 0 ∨ h 4 = 0) (hin7 : h 5 ≤ markX d) (hout7 : h 7 ≤ d.length 7 - markX d) (hflat7 : h 5 = 0 ∨ h 7 = 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.GenusFiveRow08ChamberTwo.profileLB {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hC : d.length 2 ≤ d.length 7) : ConfigurationMarkedRow.Profile d (rowMark d) (heightLB d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.profileRB {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hC : d.length 2 ≤ d.length 7) : ConfigurationMarkedRow.Profile d (rowMark d) (heightRB d)

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.profileT5 {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hC : d.length 2 ≤ d.length 7) : ConfigurationMarkedRow.Profile d (rowMark d) (heightT5 d)

The endpoint ledger, vertex by vertex

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.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 two, using split-ramp formulas on marked slots 4 and 7.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.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.GenusFiveRow08ChamberTwo.chipWeight (v : Fin 8) : ℤ

The two core-supported chips of chamber two, at vertices 2 and 3.

Equations

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

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.sum_chipWeight : ∑ v : Fin 8, chipWeight v = 2

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

AR's divisor on chamber 2.

Equations

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

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

Base core weight formed from the chips at vertices 2 and 3 and the endpoint contributions of the marked chips on slots 4 and 7.

Equations

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

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

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.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) + if markX d = 0 then if v = 5 then 1 else 0 else if d.length 7 ≤ markX d then if v = 7 then 1 else 0 else 0

Chip allocations for the two triangle scripts

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

Allocation for the vertex-4 script: transfer across contracted slots 9 and 4, and lend a chip from vertex 2 to vertex 5 across slot 8 when the height comparison requires it.

Equations

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

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

Allocation for the vertex-5 script: transfer across contracted slots 9 and 4, and lend a chip from vertex 2 to vertex 4 across slot 5 when the height comparison requires it.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.allocT4_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, allocT4 d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.allocT5_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, allocT5 d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

The left banana pair

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.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.GenusFiveRow08ChamberTwo.lbCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hC : d.length 2 ≤ d.length 7) (v : Fin 8) : base d v + contribForm d (heightLB d) v = lbCoeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.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.GenusFiveRow08ChamberTwo.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.GenusFiveRow08ChamberTwo.ownerZero d = if d.length 3 = 0 then 3 else 0

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

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

The right banana pair

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

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

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.rbCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (_hB : d.length 3 ≤ d.length 4) (hC : d.length 2 ≤ d.length 7) (v : Fin 8) : base d v + contribForm d (heightRB d) v = rbCoeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.rbCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hC : d.length 2 ≤ d.length 7) (v : Fin 8) : 0 ≤ rbCoeff d v

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

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

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberTwo.ownerSix d = if d.length 2 = 0 then 3 else 6

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.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.GenusFiveRow08ChamberTwo.ownerSeven d = if d.length 7 = 0 then 5 else 7

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.rbCoeff_owner_six {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ rbCoeff d (ownerSix d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.rbCoeff_owner_seven {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hC : d.length 2 ≤ d.length 7) : 1 ≤ rbCoeff d (ownerSeven d)

The chipped triangle at the target 4

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

Expanded core coefficients after the vertex-4 height script, combining the target 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.GenusFiveRow08ChamberTwo.t4Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hC : d.length 2 ≤ d.length 7) (v : Fin 8) : allocT4 d v + contribForm d (heightT4 d) v = t4Coeff d v

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

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

Representative receiving the vertex-4 target chip: use vertex 4 when the configuration delivers there, otherwise vertex 2 across contracted slot 5 without lending, and vertex 5 in the remaining case.

Equations

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

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

The chipped triangle at the target 5

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

Expanded core coefficients after the vertex-5 height script, combining the target allocation with endpoint contributions. t5Coeff_eq identifies this formula with the script computation.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.t5Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (_hC : d.length 2 ≤ d.length 7) (v : Fin 8) : allocT5 d v + contribForm d (heightT5 d) v = t5Coeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.t5Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hB : d.length 3 ≤ d.length 4) (hC : d.length 2 ≤ d.length 7) (v : Fin 8) : 0 ≤ t5Coeff d v

def AtanasovRanganathan.GenusFiveRow08ChamberTwo.ownerFive (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Representative receiving the vertex-5 target chip: use vertex 5 when the configuration delivers there, otherwise vertex 2 across contracted slot 8 without lending, and vertex 4 in the remaining case.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.t5Coeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ t5Coeff d (ownerFive d)

Every contracted core class is reached

theorem AtanasovRanganathan.GenusFiveRow08ChamberTwo.rowDivisor_reaches_coreVertex {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hB : d.length 3 ≤ d.length 4) (hC : d.length 2 ≤ d.length 7) (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.GenusFiveRow08ChamberTwo.chamberTwo_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.ChamberTwo length) : Nonempty (Configurations.DegreeFourDharPencil (Configurations.faceSpec GenusFiveCoreAtlas.row08Core chamberTwo_pencil._proof_1 length forest notLoopy).graph)

AR's seventh family, second scope. The chipped triangle.