AR row 10, chamber 2

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

 D = [1] + [2] + [7] + (e10 at distance |e4| from 3)

so the single mark is mark e10 = |e10| - |e4|, measured from e10's tail 0. The decomposition is the one of chamber 1 with the mark moved from e4 to e10: the tripod slides from 1 to 0, and the half-slot arm slides from C to the apex A.

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

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

Again the chamber's first inequality is exactly alpha = gamma and its second is exactly gamma ≤ beta. The third case, c = min, is the sigma image of this chamber and is carried for free by GenusFiveRow10Symmetry.chamber_covers.

The mark

def AtanasovRanganathan.GenusFiveRow10ChamberTwo.markA (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

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

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberTwo.markA d = d.length 10 - d.length 4

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

The second chamber marks slot 10 at offset markA; all other slots receive offset zero.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberTwo.rowMark d e = if e = 10 then AtanasovRanganathan.GenusFiveRow10ChamberTwo.markA d else 0

@[simp]

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.rowMark_ten (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : rowMark d 10 = markA d

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.rowMark_other (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) {e : Fin 12} (h10 : e ≠ 10) : rowMark d e = 0

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

The core, spelled out

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.tail_ten {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) : d.core.tail 10 = 0

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.head_ten {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) : d.core.head 10 = 3

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.armA_len {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hb : d.length 4 ≤ d.length 10) : d.length 10 - markA d = d.length 4

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

The heights

d.length 4 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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.resB d = min (d.length 3) (d.length 4 + d.length 9)

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

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

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberTwo.capG d = d.length 4 + d.length 6

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

The shorter banana slot.

Equations

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

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

The height of B under the target-B profile.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberTwo.htB d = min (AtanasovRanganathan.GenusFiveRow10ChamberTwo.resB d) (d.length 4 + d.length 11)

def AtanasovRanganathan.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.htD (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : ℕ

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

Equations

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

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

The height of B under the target-P profile.

Equations

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

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

The tripod at 0: e0, then e2, then the near half of the marked e10.

Equations

• AtanasovRanganathan.GenusFiveRow10ChamberTwo.tripod d = min (d.length 0) (min (d.length 2) (AtanasovRanganathan.GenusFiveRow10ChamberTwo.markA d))

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

The tripod profile.

Equations

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

Profiles

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.mkProfile {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 4 ≤ d.length 10) {h : Fin 8 → ℕ} (hin10 : h 0 ≤ markA d) (hout10 : h 3 ≤ d.length 10 - markA d) (hflat10 : h 0 = 0 ∨ h 3 = 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.GenusFiveRow10ChamberTwo.profileFlat {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 4 ≤ d.length 10) (hc : d.length 4 ≤ d.length 3) : ConfigurationMarkedRow.Profile d (rowMark d) (heightFlat d)

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

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

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

The endpoint ledger, vertex by vertex

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

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

Equations

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

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

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

Equations

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

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

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

def AtanasovRanganathan.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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 10.

Equations

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

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

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

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

Chip allocations

def AtanasovRanganathan.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.allocT (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

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

Equations

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.rep_zero_zero {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hz : d.length 0 = 0) : d.rep 2 = d.rep 0

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.fCoeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

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

Equations

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

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

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

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

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

The target-B profile

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

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

Equations

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

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

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.four_le_htB {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hc : d.length 4 ≤ d.length 3) : d.length 4 ≤ htB d

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

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

Which vertex of B's class owns the chip delivered to 5.

Equations

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

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.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.GenusFiveRow10ChamberTwo.pCoeff (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) (v : Fin 8) : ℤ

Expanded core coefficients of the banana height profile applied to the second-chamber allocP.

Equations

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

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

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.pChain (d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12) : resB d = min (d.length 3) (d.length 4 + d.length 9) ∧ parq d = min (d.length 7) (d.length 8) ∧ capG d = d.length 4 + 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.GenusFiveRow10ChamberTwo.pCoeff_nonneg {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hb : d.length 4 ≤ d.length 10) (hc : d.length 4 ≤ d.length 3) (v : Fin 8) : 0 ≤ pCoeff d v

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

Which vertex of P's class owns the chip delivered to 6.

Equations

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

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

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

The tripod at 0

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

Expanded core coefficients after the tripod script at vertex 0, applied to the second-chamber allocT.

Equations

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

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

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

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

Every contracted core class is reached

theorem AtanasovRanganathan.GenusFiveRow10ChamberTwo.rowDivisor_reaches_coreVertex {d : Utilities.Certificate.DegenerateSpec.DegSpec 8 12} (hCore : d.core = GenusFiveCoreAtlas.row10Core) (hb : d.length 4 ≤ d.length 10) (hc : 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.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.GenusFiveRow10ChamberTwo.chamberTwo_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.ChamberTwo length) : Nonempty (Configurations.DegreeFourDharPencil (Configurations.faceSpec GenusFiveCoreAtlas.row10Core chamberTwo_pencil._proof_1 length forest notLoopy).graph)

AR's ninth family, second scope.