AR row 10, chamber 1

The first scope Atanasov--Ranganathan draw for their ninth family: the apex spoke realizes the minimum, |e10| ≤ |e4| and |e10| ≤ |e3|. The displayed divisor is

 D = [0] + [2] + [7] + (e4 at distance |e10| from 4)

so the single mark is mark e4 = |e4| - |e10|, measured from e4's tail 1. The five chip-free vertices split as

• {1} -- a ConfigurationMarkedTripod centre: the slots e2 (to the chip 0), e1 (to the chip 2), and the near half of the marked e4;
• {3, 4, 5, 6} -- AR's eleventh picture (ConfigurationEleven) with A = 3, B = 5, C = 4, P = 6 and the chip Q = 7:

 alpha = |e10|   (apex arm, to the chip 0)      S = |e9|    t = |e5|
 beta  = |e3|    (B arm, to the chip 2)         u = |e11|   w = |e6|
 gamma = |e10|   (C arm: the far half of e4, to the chip at the mark)
 m₁, m₂ = |e7|, |e8|

The chamber's first inequality is exactly what makes alpha = gamma -- it places the interior chip at distance |e10| from 4 -- and its second inequality is exactly gamma ≤ beta. Both are used, and nothing else about the chamber is.

The mark

def AtanasovRanganathan.GenusFiveRow10ChamberOne.markC (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The chip on e4, at distance |e10| from the head 4.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.markC d = d.length 4 - d.length 10

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

The first chamber marks slot 4 at offset markC; all other slots receive offset zero.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.rowMark d e = if e = 4 then AtanasovRanganathan.GenusFiveRow10ChamberOne.markC d else 0

@[simp]

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

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.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.GenusFiveRow10ChamberOne.tail_four {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) : d.core.tail 4 = 1

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.armC_len {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hb : d.length 10 ≤ d.length 4) : d.length 4 - markC d = d.length 10

The far half of the marked slot -- the C arm -- has exactly the apex arm's length, which is the whole point of the chamber's first inequality.

The heights

d.length 10 is alpha = gamma, d.length 3 is beta, d.length 9 is S, d.length 5 is t, d.length 11 is u, d.length 6 is w, and d.length 7, d.length 8 are the two banana slots.

def AtanasovRanganathan.GenusFiveRow10ChamberOne.resB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

mB: B's two resources, its own arm or the apex's arm followed by S.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.resB d = min (d.length 3) (d.length 10 + d.length 9)

def AtanasovRanganathan.GenusFiveRow10ChamberOne.capG (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

G: the far route C1 ⟶ C ⟶ P, two slots because C is chip free.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.capG d = d.length 10 + d.length 6

def AtanasovRanganathan.GenusFiveRow10ChamberOne.parq (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The shorter banana slot.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.parq d = min (d.length 7) (d.length 8)

def AtanasovRanganathan.GenusFiveRow10ChamberOne.htB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The height of B under the target-B profile.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.htB d = min (AtanasovRanganathan.GenusFiveRow10ChamberOne.resB d) (d.length 10 + d.length 11)

def AtanasovRanganathan.GenusFiveRow10ChamberOne.htE (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The height of P under the target-P profile.

Equations

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

def AtanasovRanganathan.GenusFiveRow10ChamberOne.htD (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The height of the chip Q under the target-P profile.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.htD d = min (AtanasovRanganathan.GenusFiveRow10ChamberOne.htE d) (AtanasovRanganathan.GenusFiveRow10ChamberOne.resB d + d.length 11)

def AtanasovRanganathan.GenusFiveRow10ChamberOne.htC (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The height of B under the target-P profile.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.htC d = min (AtanasovRanganathan.GenusFiveRow10ChamberOne.htD d) (AtanasovRanganathan.GenusFiveRow10ChamberOne.resB d)

def AtanasovRanganathan.GenusFiveRow10ChamberOne.tripod (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

The tripod at 1: e2, then e1, then the near half of the marked e4.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.tripod d = min (d.length 2) (min (d.length 1) (AtanasovRanganathan.GenusFiveRow10ChamberOne.markC d))

def AtanasovRanganathan.GenusFiveRow10ChamberOne.shift (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℤ

The transfer of B's surplus into Q's class when the B-Q slot collapses.

Equations

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

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

The flat profile, which reaches the apex 3 and the vertex 4 at once.

Equations

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

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

The target-B profile: B alone rises above the flat level.

Equations

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

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

The target-P profile: the chip Q rides up with P.

Equations

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

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

The tripod profile.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.heightT d v = if v = 1 then AtanasovRanganathan.GenusFiveRow10ChamberOne.tripod d else 0

Profiles

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.mkProfile {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) {h : Fin 8 → ℕ} (hin4 : h 1 ≤ markC d) (hout4 : h 4 ≤ d.length 4 - markC d) (hflat4 : h 1 = 0 ∨ h 4 = 0) (hconst : ∀ (e : Fin 12), d.length e = 0 → h (GenusFiveCoreAtlas.row10Core.tail e) = h (GenusFiveCoreAtlas.row10Core.head e)) : ConfigurationMarkedRow.Profile d (rowMark d) h

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.profileFlat {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) : ConfigurationMarkedRow.Profile d (rowMark d) (heightFlat d)

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.profileB {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) : ConfigurationMarkedRow.Profile d (rowMark d) (heightB d)

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.profileP {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) : ConfigurationMarkedRow.Profile d (rowMark d) (heightP d)

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.profileT {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (_hc : d.length 10 ≤ d.length 3) : ConfigurationMarkedRow.Profile d (rowMark d) (heightT d)

The endpoint ledger, vertex by vertex

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

Incident-slot contribution for the first row-10 chamber, using the split-ramp formula on marked slot 4.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.contrib_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) {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.GenusFiveRow10ChamberOne.chipWeight (v : Fin 8) : ℤ

Core-supported part of the first-chamber divisor: one chip each at vertices 0, 2, and 7.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.chipWeight v = if v = 0 then 1 else if v = 2 then 1 else if v = 7 then 1 else 0

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

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

def AtanasovRanganathan.GenusFiveRow10ChamberOne.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.GenusFiveRow10ChamberOne.base (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8 → ℤ

Base core weight combining the three core chips with 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.GenusFiveRow10ChamberOne.rowDivisor_effective (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : effective (rowDivisor d)

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

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

Chip allocations

Four conditional transfers, each inside one contracted class. Three of them hand a collapsed arm's chip to the picture vertex it has merged with; the fourth, shift, is ConfigurationBananaTail's, moving B's surplus to the chip Q when the B-Q slot collapses.

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

Allocation for the flat script, transferring chips from 0 to 3 and from 1 to 4 when slots 10 and 4 respectively contract.

Equations

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

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

Allocation for the vertex-5 height adjustment, additionally transferring the chip at vertex 2 across contracted slot 3.

Equations

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

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

Allocation for the banana profile, additionally transferring across contracted slot 9 and across contracted slot 11 when its height comparison requires it.

Equations

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

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

Allocation for the tripod at vertex 1, collecting the chips from vertices 0 and 2 across contracted slots 2 and 1.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_ten {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 10 = 0) : d.rep 0 = d.rep 3

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_four {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 4 = 0) : d.rep 1 = d.rep 4

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 3 = 0) : d.rep 2 = d.rep 5

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_nine {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 9 = 0) : d.rep 3 = d.rep 5

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_eleven {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 11 = 0) : d.rep 5 = d.rep 7

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_two {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 2 = 0) : d.rep 0 = d.rep 1

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_one {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 1 = 0) : d.rep 2 = d.rep 1

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_six {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 6 = 0) : d.rep 4 = d.rep 6

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rep_zero_banana {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : parq d = 0) : d.rep 7 = d.rep 6

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.allocFlat_classSum {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, allocFlat d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.allocB_classSum {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, allocB d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.allocP_classSum {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, allocP d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.allocT_classSum {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (r : Fin 8) : ∑ v : Fin 8 with d.rep v = d.rep r, allocT d v = ∑ v : Fin 8 with d.rep v = d.rep r, base d v

The flat profile: the apex 3 and the vertex 4

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

Expanded core coefficients of the flat-height script applied to allocFlat.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.fCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (_hc : d.length 10 ≤ d.length 3) (v : Fin 8) : allocFlat d v + contribForm d (heightFlat d) v = fCoeff d v

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.fCoeff_owner_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ fCoeff d 3

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.fCoeff_owner_four {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ fCoeff d 4

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.fCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) (v : Fin 8) : 0 ≤ fCoeff d v

The target-B profile

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

Expanded core coefficients after the height adjustment at vertex 5, applied to allocB.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.bCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (_hc : d.length 10 ≤ d.length 3) (v : Fin 8) : allocB d v + contribForm d (heightB d) v = bCoeff d v

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.htB_le_three {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : htB d ≤ d.length 3

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.ten_le_htB {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hc : d.length 10 ≤ d.length 3) : d.length 10 ≤ htB d

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.bCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) (v : Fin 8) : 0 ≤ bCoeff d v

def AtanasovRanganathan.GenusFiveRow10ChamberOne.ownerB (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Which vertex of B's class owns the chip delivered to 5. When the A-B slot collapses the apex is in the class and already carries it; when the B-Q slot collapses the chip at Q is.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberOne.ownerB d = if d.length 9 = 0 then 3 else if d.length 11 = 0 then 7 else 5

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.bCoeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hc : d.length 10 ≤ d.length 3) : 1 ≤ bCoeff d (ownerB d)

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.ownerB_rep {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) : d.rep (ownerB d) = d.rep 5

The target-P profile

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

Expanded core coefficients of the banana height profile applied to allocP, including the transfer across contracted slot 11.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.pCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (_hc : d.length 10 ≤ d.length 3) (v : Fin 8) : allocP d v + contribForm d (heightP d) v = pCoeff d v

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.pChain (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : resB d = min (d.length 3) (d.length 10 + d.length 9) ∧ parq d = min (d.length 7) (d.length 8) ∧ capG d = d.length 10 + d.length 6 ∧ htE d = min (capG d) (resB d + d.length 11 + parq d) ∧ htD d = min (htE d) (resB d + d.length 11) ∧ htC d = min (htD d) (resB d)

The nested minima of the target-P profile, in the shape ConfigurationEleven consumes.

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.pCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) (v : Fin 8) : 0 ≤ pCoeff d v

def AtanasovRanganathan.GenusFiveRow10ChamberOne.ownerP (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : Fin 8

Which vertex of P's class owns the chip delivered to 6. When the C-P slot collapses C is in the class and already carries it; when a banana slot collapses the chip at Q is.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.pCoeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (_hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) : 1 ≤ pCoeff d (ownerP d)

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.ownerP_rep {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) : d.rep (ownerP d) = d.rep 6

The tripod at 1

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

Expanded core coefficients after the tripod script at vertex 1, applied to allocT.

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.tCoeff_eq {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (_hc : d.length 10 ≤ d.length 3) (v : Fin 8) : allocT d v + contribForm d (heightT d) v = tCoeff d v

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.tCoeff_owner {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} : 1 ≤ tCoeff d 1

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.tCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hb : d.length 10 ≤ d.length 4) (v : Fin 8) : 0 ≤ tCoeff d v

Every contracted core class is reached

theorem AtanasovRanganathan.GenusFiveRow10ChamberOne.rowDivisor_reaches_coreVertex {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 10 ≤ d.length 4) (hc : d.length 10 ≤ d.length 3) (F : Finset (Fin 12)) (hRepReach : ∀ (x y : Fin 8), d.rep x = d.rep y ↔ Utilities.Certificate.ContractionForestCensusGeneral.ReachIn GenusFiveCoreAtlas.row10Core 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.GenusFiveRow10ChamberOne.chamberOne_pencil (length : Fin 12 → ℕ) (forest : Utilities.Certificate.ContractionForestCensusGeneral.IsForest GenusFiveCoreAtlas.row10Core (Configurations.zeroSlots length)) (notLoopy : ¬Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy GenusFiveCoreAtlas.row10Core (Configurations.zeroSlots length)) (hP : GenusFiveRow10Symmetry.ChamberOne length) : Nonempty (Configurations.DegreeFourDharPencil (Configurations.faceSpec GenusFiveCoreAtlas.row10Core chamberOne_pencil._proof_1 length forest notLoopy).graph)

AR's ninth family, first scope.