Independent generated check. This module provides an additional generated proof of row 06 and is not imported by the main LowGenus root.

Generated shared data for the chamber-restricted AR row-06 cover: the fixed divisor and the pooled anchor witnesses. Imported by every cell chunk and by the assembling module.

def AtanasovRanganathan.GenusFiveRow06CoverBase.aff (data : List ℤ) : Utilities.Certificate.ExplicitPotential.AffineForm 12

Decode an integer coefficient list as a twelve-variable affine form: the first entry is the constant and missing entries are zero.

Equations

• AtanasovRanganathan.GenusFiveRow06CoverBase.aff data = { fixedValue := data.getD 0 0, coefficient := fun (coordinate : Fin 12) => data.getD (↑coordinate + 1) 0 }

def AtanasovRanganathan.GenusFiveRow06CoverBase.rowDivisor : Fin 8 → ℤ

The fixed degree-four row-06 divisor, with two chips at each of the hub vertices two and three.

Equations

• AtanasovRanganathan.GenusFiveRow06CoverBase.rowDivisor vertex = [0, 0, 2, 2, 0, 0, 0, 0].getD (↑vertex) 0

def AtanasovRanganathan.GenusFiveRow06CoverBase.defaultWitness : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

The zero endpoint slopes and zero core potential used for an out-of-range witness-table lookup.

Equations

• AtanasovRanganathan.GenusFiveRow06CoverBase.defaultWitness = { alpha := fun (x : Fin 12) => 0, beta := fun (x : Fin 12) => 0, potential := fun (x : Fin 8) => 0 }

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness0 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 0 for the row-06 closed cover: alpha is -1 at slots 2, and zero elsewhere. beta is -1 at slots 3; 1 at slots 2, and zero elsewhere. The nonzero affine potentials occur at vertices 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness1 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 1 for the row-06 closed cover: alpha is -1 at slots 2; 1 at slots 3, and zero elsewhere. beta is -1 at slots 3, and zero elsewhere. The nonzero affine potentials occur at vertices 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness2 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 2 for the row-06 closed cover: alpha is zero. beta is zero. The affine potential is zero.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness3 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 3 for the row-06 closed cover: alpha is -1 at slots 8, 9, and zero elsewhere. beta is 1 at slots 9, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness4 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 4 for the row-06 closed cover: alpha is -1 at slots 8, 9, and zero elsewhere. beta is 1 at slots 8, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness5 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 5 for the row-06 closed cover: alpha is -1 at slots 4; 1 at slots 7, and zero elsewhere. beta is -1 at slots 7, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness6 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 6 for the row-06 closed cover: alpha is -1 at slots 4, and zero elsewhere. beta is -1 at slots 7; 1 at slots 4, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness7 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 7 for the row-06 closed cover: alpha is -2 at slots 2; 2 at slots 3, and zero elsewhere. beta is -2 at slots 3, and zero elsewhere. The nonzero affine potentials occur at vertices 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness8 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 8 for the row-06 closed cover: alpha is -2 at slots 2; 1 at slots 3, and zero elsewhere. beta is -1 at slots 3, and zero elsewhere. The nonzero affine potentials occur at vertices 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness9 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 9 for the row-06 closed cover: alpha is -2 at slots 2; -1 at slots 0, 1, and zero elsewhere. beta is -1 at slots 3; 1 at slots 0; 2 at slots 2, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness10 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 10 for the row-06 closed cover: alpha is -2 at slots 2; -1 at slots 0, 1, and zero elsewhere. beta is -2 at slots 3; 1 at slots 0; 2 at slots 2, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness11 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 11 for the row-06 closed cover: alpha is -2 at slots 2; -1 at slots 0, 1; 2 at slots 3, and zero elsewhere. beta is -2 at slots 3; 2 at slots 2, and zero elsewhere. The nonzero affine potentials occur at vertices 1, 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness12 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 12 for the row-06 closed cover: alpha is -1 at slots 4, and zero elsewhere. beta is -2 at slots 7; 1 at slots 4, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness13 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 13 for the row-06 closed cover: alpha is -1 at slots 4; 1 at slots 5; 2 at slots 7, and zero elsewhere. beta is -2 at slots 7; -1 at slots 5, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness14 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 14 for the row-06 closed cover: alpha is -2 at slots 4; 1 at slots 5; 2 at slots 7, and zero elsewhere. beta is -2 at slots 7; -1 at slots 5, 6, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness15 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 15 for the row-06 closed cover: alpha is -1 at slots 2, 4; 1 at slots 3, and zero elsewhere. beta is -1 at slots 3, 7; 1 at slots 2, 4, and zero elsewhere. The nonzero affine potentials occur at vertices 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness16 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 16 for the row-06 closed cover: alpha is -1 at slots 4; 2 at slots 7, and zero elsewhere. beta is -2 at slots 7; -1 at slots 5, 6; 1 at slots 4, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness17 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 17 for the row-06 closed cover: alpha is -2 at slots 9; -1 at slots 8, and zero elsewhere. beta is 1 at slots 8, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness18 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 18 for the row-06 closed cover: alpha is -2 at slots 9; -1 at slots 8, 10, 11, and zero elsewhere. beta is 1 at slots 10; 2 at slots 9, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness19 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 19 for the row-06 closed cover: alpha is -2 at slots 8, 9; -1 at slots 10, 11, and zero elsewhere. beta is 1 at slots 10; 2 at slots 9, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness20 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 20 for the row-06 closed cover: alpha is -1 at slots 2, 8, 9; 1 at slots 3, and zero elsewhere. beta is -1 at slots 3; 1 at slots 2, 8, and zero elsewhere. The nonzero affine potentials occur at vertices 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness21 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 21 for the row-06 closed cover: alpha is -2 at slots 9; -1 at slots 8, 10, 11, and zero elsewhere. beta is 1 at slots 8; 2 at slots 9, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness22 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 22 for the row-06 closed cover: alpha is -2 at slots 8; -1 at slots 9, and zero elsewhere. beta is 1 at slots 9, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness23 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 23 for the row-06 closed cover: alpha is -2 at slots 8; -1 at slots 9; 1 at slots 10, and zero elsewhere. beta is -1 at slots 10, 11; 2 at slots 8, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness24 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 24 for the row-06 closed cover: alpha is -2 at slots 8, 9; 1 at slots 10, and zero elsewhere. beta is -1 at slots 10, 11; 2 at slots 8, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness25 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 25 for the row-06 closed cover: alpha is -1 at slots 2, 8, 9; 1 at slots 3, and zero elsewhere. beta is -1 at slots 3; 1 at slots 2, 9, and zero elsewhere. The nonzero affine potentials occur at vertices 2, 3, 4, 5, 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness26 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 26 for the row-06 closed cover: alpha is -2 at slots 8; -1 at slots 9, and zero elsewhere. beta is -1 at slots 10, 11; 1 at slots 9; 2 at slots 8, and zero elsewhere. The nonzero affine potentials occur at vertices 4, 5.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness27 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 27 for the row-06 closed cover: alpha is -2 at slots 4; 1 at slots 7, and zero elsewhere. beta is -1 at slots 7, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness28 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 28 for the row-06 closed cover: alpha is -2 at slots 4; -1 at slots 5, 6, and zero elsewhere. beta is -1 at slots 7; 1 at slots 5; 2 at slots 4, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness29 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 29 for the row-06 closed cover: alpha is -2 at slots 4; -1 at slots 5, 6, and zero elsewhere. beta is -2 at slots 7; 1 at slots 5; 2 at slots 4, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witness30 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 30 for the row-06 closed cover: alpha is -2 at slots 4; -1 at slots 5, 6; 1 at slots 7, and zero elsewhere. beta is -1 at slots 7; 2 at slots 4, and zero elsewhere. The nonzero affine potentials occur at vertices 6, 7.

Equations

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

def AtanasovRanganathan.GenusFiveRow06CoverBase.witnesses : List (Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12)

The thirty-one endpoint-slope and affine-potential witnesses shared by the row-06 closed-cover cells.

Equations

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