Across 087500 092500

Shared exact checkpoint data; all transitions are verified by kernel proofs.

def ConwaySoifer.Simplified.Certificates.Across087500092500.point0 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point0 = ([-1387500000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point1 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point1 = ([0], [787500000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point2 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point2 = ([7031250000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point3 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point3 = ([7950000000000], [675000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point4 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point4 = ([9000000000000], [3375000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point5 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point5 = ([-476437500000, -5445000000000], [238218750000, 2722500000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point6 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point6 = ([-238218750000, -2722500000000], [-238218750000, -2722500000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point7 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point7 = ([238218750000, 2722500000000], [-476437500000, -5445000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point8 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point8 = ([476437500000, 5445000000000], [-238218750000, -2722500000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point9 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point9 = ([238218750000, 2722500000000], [238218750000, 2722500000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point10 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point10 = ([-238218750000, -2722500000000], [476437500000, 5445000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point11 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point11 = ([8212500000000, -9000000000000], [787500000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point12 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point12 = ([9000000000000], [-787500000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point13 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point13 = ([9000000000000], [0])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point14 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point14 = ([-787500000000, -9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point15 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point15 = ([787500000000, 9000000000000], [8212500000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point16 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point16 = ([9000000000000], [4500000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point17 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point17 = ([0], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point18 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point18 = ([-9000000000000], [8212500000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point19 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point19 = ([-8212500000000, 9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point20 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point20 = ([-9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point21 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point21 = ([-9000000000000], [0])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point22 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point22 = ([-8212500000000, 9000000000000], [-787500000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point23 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point23 = ([-9000000000000], [787500000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point24 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point24 = ([-787500000000, -9000000000000], [-8212500000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point25 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point25 = ([0], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point26 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point26 = ([787500000000, 9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point27 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point27 = ([8212500000000, -9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point28 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point28 = ([9000000000000], [-9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point29 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point29 = ([9000000000000], [-8212500000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point30 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point30 = ([9000000000000], [8212500000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point31 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point31 = ([9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point32 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point32 = ([8212500000000, -9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point33 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point33 = ([-18000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point34 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point34 = ([-17212500000000, 9000000000000], [8212500000000, -9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point35 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point35 = ([-17212500000000, 9000000000000], [9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point36 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point36 = ([8212500000000, -9000000000000], [-17212500000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point37 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point37 = ([9000000000000], [-18000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.point38 : Certificates.IPoint

Shared exact polynomial coordinates, scaled by the certificate denominator.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.point38 = ([9000000000000], [-17212500000000, 9000000000000])

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet0 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet1 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet2 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet3 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet4 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet5 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet6 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet7 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet8 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet9 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet10 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet11 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet12 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet13 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.pointSet14 : List Certificates.IPoint

Shared mandatory-point list for one proposed owner state.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.capsConstraints : Fin 10 → List Certificates.Cap

Contact constraints shared by every state in this certificate trace.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.ownerFlags : Fin 10 → Option (Fin 6)

Side-owner restrictions shared by every state in this certificate trace.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.model0 : Certificates.Model

Proposed owner constraints after 0 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.step0 : Certificates.Step

The forced-point assignment at trace index 0.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.step0 = { owner := 3, q := ConwaySoifer.Simplified.Certificates.Across087500092500.point0 }

def ConwaySoifer.Simplified.Certificates.Across087500092500.model1 : Certificates.Model

Proposed owner constraints after 1 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.step1 : Certificates.Step

The forced-point assignment at trace index 1.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.step1 = { owner := 0, q := ConwaySoifer.Simplified.Certificates.Across087500092500.point1 }

def ConwaySoifer.Simplified.Certificates.Across087500092500.model2 : Certificates.Model

Proposed owner constraints after 2 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.step2 : Certificates.Step

The forced-point assignment at trace index 2.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.step2 = { owner := 7, q := ConwaySoifer.Simplified.Certificates.Across087500092500.point2 }

def ConwaySoifer.Simplified.Certificates.Across087500092500.model3 : Certificates.Model

Proposed owner constraints after 3 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.step3 : Certificates.Step

The forced-point assignment at trace index 3.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.step3 = { owner := 1, q := ConwaySoifer.Simplified.Certificates.Across087500092500.point3 }

def ConwaySoifer.Simplified.Certificates.Across087500092500.model4 : Certificates.Model

Proposed owner constraints after 4 forced-point assignments.

Equations

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

def ConwaySoifer.Simplified.Certificates.Across087500092500.step4 : Certificates.Step

The forced-point assignment at trace index 4.

Equations

• ConwaySoifer.Simplified.Certificates.Across087500092500.step4 = { owner := 1, q := ConwaySoifer.Simplified.Certificates.Across087500092500.point4 }

def ConwaySoifer.Simplified.Certificates.Across087500092500.model5 : Certificates.Model

Proposed owner constraints after 5 forced-point assignments.

Equations

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

theorem ConwaySoifer.Simplified.Certificates.Across087500092500.trace_steps : [step0, step1, step2, step3, step4] = Data.Across087500092500.steps

The shared step constants reproduce the original certificate trace exactly.