AR row 08, chamber 1

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

 D = [4] + [5] + (e3 at distance |e4| from 0) + (e2 at distance |e7| from 6)

so the two marks are mark e3 = |e3| - |e4| (measured from e3's tail 3) and mark e2 = |e7|. The six chip-free vertices split exactly as in AR's sixth family:

• {0, 1} -- a banana pair whose two arms both have length |e4|: the far half of e3, and the whole of e4.
• {6, 7} -- a banana pair whose two arms both have length |e7|: the near half of e2, and the whole of e7.
• {2, 3} -- a ConfigurationThree pair across the stem e9; vertex 2's arms are e5 and e8, vertex 3's are the near half of e3 and the far half of e2.

So this chamber needs no picture that row 05 did not already need, and the whole file is an instantiation of ConfigurationMarkedRow plus four coefficient tables.

The two marks

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

The chip on e3, at distance |e4| from the head 0.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.markY d = d.length 3 - d.length 4

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

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

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.markX d = d.length 7

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

The first chamber marks slot 2 at markX and slot 3 at markY; other slots receive offset zero.

Equations

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

@[simp]

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.rowMark_two (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : rowMark d 2 = markX d

@[simp]

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.rowMark_three (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : rowMark d 3 = markY d

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.rowMark_other (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} (h2 : e ≠ 2) (h3 : e ≠ 3) : rowMark d e = 0

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

The core, spelled out

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.tail_two {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.tail 2 = 6

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.head_two {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.head 2 = 3

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.tail_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.tail 3 = 3

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.head_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) : d.core.head 3 = 0

The heights

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

Vertex 2's arm minimum: e5 to the chip 4, e8 to the chip 5.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.armTwo d = min (d.length 5) (d.length 8)

def AtanasovRanganathan.GenusFiveRow08ChamberOne.armThree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Vertex 3's arm minimum: the near half of e3, the far half of e2.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.armThree d = min (AtanasovRanganathan.GenusFiveRow08ChamberOne.markY d) (d.length 2 - AtanasovRanganathan.GenusFiveRow08ChamberOne.markX d)

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

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

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.pairLow d = min (AtanasovRanganathan.GenusFiveRow08ChamberOne.armTwo d) (AtanasovRanganathan.GenusFiveRow08ChamberOne.armThree d)

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

Target height at vertex 2, bounded by its own effective arm and by the shared height plus the length of the connecting slot 9.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.targetTwo d = min (AtanasovRanganathan.GenusFiveRow08ChamberOne.armTwo d) (AtanasovRanganathan.GenusFiveRow08ChamberOne.pairLow d + d.length 9)

def AtanasovRanganathan.GenusFiveRow08ChamberOne.targetThree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

Target height at vertex 3, bounded by its own effective arm and by the shared height plus the length of the connecting slot 9.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.targetThree d = min (AtanasovRanganathan.GenusFiveRow08ChamberOne.armThree d) (AtanasovRanganathan.GenusFiveRow08ChamberOne.pairLow d + d.length 9)

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

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

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.heightLB d v = if v = 0 then d.length 4 else if v = 1 then d.length 4 else 0

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

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

Equations

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

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

The stem pair read at the target 2.

Equations

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

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

The stem pair read at the target 3.

Equations

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

Profiles

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.mkProfile {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hC : d.length 7 ≤ d.length 2) {h : Fin 8 → ℕ} (hin2 : h 6 ≤ markX d) (hout2 : h 3 ≤ d.length 2 - markX d) (hflat2 : h 6 = 0 ∨ h 3 = 0) (hin3 : h 3 ≤ markY d) (hout3 : h 0 ≤ d.length 3 - markY d) (hflat3 : h 3 = 0 ∨ h 0 = 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.GenusFiveRow08ChamberOne.profileLB {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hC : d.length 7 ≤ d.length 2) (hA : d.length 4 ≤ d.length 3) : ConfigurationMarkedRow.Profile d (rowMark d) (heightLB d)

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

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.profileT3 {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hC : d.length 7 ≤ d.length 2) (hA : d.length 4 ≤ d.length 3) : ConfigurationMarkedRow.Profile d (rowMark d) (heightT3 d)

The endpoint ledger, vertex by vertex

def AtanasovRanganathan.GenusFiveRow08ChamberOne.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 one, using split-ramp formulas at the marks on slots 2 and 3.

Equations

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

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

The two core-supported chips of chamber one, at vertices 4 and 5.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.chipWeight v = if v = 4 then 1 else if v = 5 then 1 else 0

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

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

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

AR's divisor on chamber 1.

Equations

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

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

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

Equations

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

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

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.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 = 3 then 1 else 0 else if d.length 3 ≤ markY d then if v = 0 then 1 else 0 else 0) + if markX d = 0 then if v = 6 then 1 else 0 else if d.length 2 ≤ markX d then if v = 3 then 1 else 0 else 0

Chip allocation for the stem pair

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

Core allocation for the pair configuration: transfer chips across contracted slots 5 and 8 to vertex 2, and across contracted slot 2 to vertex 3.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.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

The four coefficient tables

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

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

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

def AtanasovRanganathan.GenusFiveRow08ChamberOne.ownerOne (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Target representative for vertex 1, moved to vertex 4 when slot 4 is contracted.

Equations

• AtanasovRanganathan.GenusFiveRow08ChamberOne.ownerOne d = if d.length 4 = 0 then 4 else 1

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.lbCoeff_owner_zero {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hA : d.length 4 ≤ d.length 3) : 1 ≤ lbCoeff d (ownerZero d)

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.lbCoeff_owner_one {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ lbCoeff d (ownerOne d)

The right banana pair

def AtanasovRanganathan.GenusFiveRow08ChamberOne.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.GenusFiveRow08ChamberOne.rbCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hC : d.length 7 ≤ d.length 2) (hA : d.length 4 ≤ d.length 3) (v : Fin 8) : base d v + contribForm d (heightRB d) v = rbCoeff d v

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

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.rbCoeff_owner_six {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ rbCoeff d 6

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.rbCoeff_owner_seven {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ rbCoeff d (ownerSeven d)

The stem pair

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

def AtanasovRanganathan.GenusFiveRow08ChamberOne.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.GenusFiveRow08ChamberOne.t2Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hC : d.length 7 ≤ d.length 2) (hA : d.length 4 ≤ d.length 3) (v : Fin 8) : pairAlloc d v + contribForm d (heightT2 d) v = t2Coeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.t2Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hC : d.length 7 ≤ d.length 2) (v : Fin 8) : 0 ≤ t2Coeff d v

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

Target representative for vertex 2, moved to vertex 3 when their connecting slot 9 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.GenusFiveRow08ChamberOne.t2Coeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ t2Coeff d (ownerTwo d)

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

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

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.t3Coeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row08Core) (hC : d.length 7 ≤ d.length 2) (hA : d.length 4 ≤ d.length 3) (v : Fin 8) : pairAlloc d v + contribForm d (heightT3 d) v = t3Coeff d v

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.t3Coeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hC : d.length 7 ≤ d.length 2) (v : Fin 8) : 0 ≤ t3Coeff d v

def AtanasovRanganathan.GenusFiveRow08ChamberOne.ownerThree (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

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

Equations

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

theorem AtanasovRanganathan.GenusFiveRow08ChamberOne.t3Coeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ t3Coeff d (ownerThree d)

Every contracted core class is reached

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

AR's seventh family, first scope.