Files needed for a verification of the proof of Propositions 1 and 2 in the paper "Limits of order-types" by Goaoc, Hubard, Joannis de Verclos, Sereni, Volec

This web-page contains the coefficients, the squared inequalities and the scripts that can be used to verify the correctness of the proofs of Propositions 1 and 2 presented in the paper "Limits of order-types" authored by Xavier Goaoc, Alfredo Hubard, Rémi de Joannis de Verclos, Jean-Sébastien Sereni, and Jan Volec.

• verification script and data (zip; the compressed size of the archive is around 17M)

  Description of the files in the archive:

  • prop1.sage – the verification Sage script for Proposition 1
  • prop2.sage – the verification Sage script for Proposition 2
  • CS0, CS1, …, CS23 – the pairing densities for types σ₀, …, σ₂₃
  • c5lb – data for computing the lower bound on c₅
    The file contains the objective function and 289 square inequalities.
  • c6lb – data for computing the lower bound on c₆
    The file contains the objective function and 311 square inequalities.
  • 6points_densities – coefficients for expressing density of each pointset of size 6 as a linear combination of densities of pointsets of size 8
  • inbal-118 – data for proving that for each limit of order-types there is a pointset of size 6 with density > 1/18
    The file contains 391 square inequalities.
  • inbal-132 – data for proving that for each limit of order-types there is a pointset of size 6 with density < 1/32
    The file contains 391 square inequalities.

  USAGE: run sage verify_bounds.sage

  • Note that the computation requires around 5GB of memory and a 64bit version of Sage 6.x (tested with Sage 6.1.1).
  • Also note that it takes around 60 minutes to run the computations (tested on a laptop with Intel Core i5-2520M and 16GB RAM).

Additional related files (not needed for the verification itself):

• list of the pointsets and flags rooted on σ₀, …, σ₂₃