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

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

def AtanasovRanganathan.GenusFiveRow04CoverBase.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.GenusFiveRow04CoverBase.aff data = { fixedValue := data.getD 0 0, coefficient := fun (coordinate : Fin 12) => data.getD (↑coordinate + 1) 0 }

def AtanasovRanganathan.GenusFiveRow04CoverBase.rowDivisor : Fin 8 → ℤ

The fixed degree-four row-04 divisor, with one chip at each of vertices zero, two, five, and six.

Equations

• AtanasovRanganathan.GenusFiveRow04CoverBase.rowDivisor vertex = [1, 0, 1, 0, 0, 1, 1, 0].getD (↑vertex) 0

def AtanasovRanganathan.GenusFiveRow04CoverBase.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.GenusFiveRow04CoverBase.defaultWitness = { alpha := fun (x : Fin 12) => 0, beta := fun (x : Fin 12) => 0, potential := fun (x : Fin 8) => 0 }

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

Endpoint-slope witness 0 for the row-04 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.GenusFiveRow04CoverBase.witness1 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 1 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11, and zero elsewhere. beta is -1 at slots 5; 1 at slots 0, 11, 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.GenusFiveRow04CoverBase.witness2 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

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

Equations

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

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

Endpoint-slope witness 3 for the row-04 closed cover: alpha is -1 at slots 0, 1, 2, 11, and zero elsewhere. beta is -1 at slots 5; 1 at slots 0, 2, 11, 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.GenusFiveRow04CoverBase.witness4 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Endpoint-slope witness 8 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11; 1 at slots 3, 5, and zero elsewhere. beta is -1 at slots 3, 4, 5; 1 at slots 0, 11, 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.GenusFiveRow04CoverBase.witness9 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 9 for the row-04 closed cover: alpha is -1 at slots 0, 1, 2, 11; 1 at slots 3, 5, and zero elsewhere. beta is -1 at slots 3, 4, 5; 1 at slots 0, 11, 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.GenusFiveRow04CoverBase.witness10 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 10 for the row-04 closed cover: alpha is -1 at slots 0, 1, 2, 11; 1 at slots 5, and zero elsewhere. beta is -1 at slots 3, 4, 5; 1 at slots 0, 2, 11, 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.GenusFiveRow04CoverBase.witness11 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 11 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11, and zero elsewhere. beta is -1 at slots 5; 1 at slots 1, 11, 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.GenusFiveRow04CoverBase.witness12 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 12 for the row-04 closed cover: alpha is -1 at slots 0, 1, 2, 11, and zero elsewhere. beta is -1 at slots 5; 1 at slots 1, 2, 11, 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.GenusFiveRow04CoverBase.witness13 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 13 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11; 1 at slots 3, 5, and zero elsewhere. beta is -1 at slots 2, 3, 4, 5; 1 at slots 0, 11, 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.GenusFiveRow04CoverBase.witness14 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 14 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11; 1 at slots 3, 5, and zero elsewhere. beta is -1 at slots 3, 4, 5; 1 at slots 11, 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.GenusFiveRow04CoverBase.witness15 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 15 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11; 1 at slots 2, 3, 5, and zero elsewhere. beta is -1 at slots 2, 3, 4, 5; 1 at slots 0, 11, 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.GenusFiveRow04CoverBase.witness16 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 16 for the row-04 closed cover: alpha is -1 at slots 0, 1, 2, 11; 1 at slots 3, 5, and zero elsewhere. beta is -1 at slots 3, 4, 5; 1 at slots 0, 1, 11, 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.GenusFiveRow04CoverBase.witness17 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 17 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11; 1 at slots 5, and zero elsewhere. beta is -1 at slots 3, 4, 5; 1 at slots 0, 11, 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.GenusFiveRow04CoverBase.witness18 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 18 for the row-04 closed cover: alpha is -2 at slots 2; -1 at slots 0, 1, 11; 1 at slots 3, 5, and zero elsewhere. beta is -1 at slots 3, 4, 5; 1 at slots 0, 1, 11, 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.GenusFiveRow04CoverBase.witness19 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 19 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11; 1 at slots 2, 3, 5, and zero elsewhere. beta is -1 at slots 2, 3, 4, 5; 1 at slots 11, 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.GenusFiveRow04CoverBase.witness20 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

Endpoint-slope witness 20 for the row-04 closed cover: alpha is -1 at slots 0, 1, 11; 1 at slots 3, 5, and zero elsewhere. beta is -1 at slots 2, 3, 4, 5; 1 at slots 1, 11, 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.GenusFiveRow04CoverBase.witness21 : Utilities.Certificate.ExplicitPotential.AnchorWitness 12 8 12

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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