Documentation

LeanPool.Besicovitch.SixPoint.RationalChord

The rational chord of the retargeted six-point argument #

The six-point analysis computes the sharp constant sStar, but a Lean proof of sigmaOne ≤ sStar needs that endpoint to be attained exactly, and the resulting tightness is what makes the finite certificates expensive. The argument is carried out instead at the rational threshold barS = 6934 / 10000, which still improves on the published 0.7 and leaves the weighted score a margin of about 3 * 10 ^ -3 rather than 10 ^ -8.

The routing and exclusion modules use a chord only through the two facts below: that it lies between one and two, and that it lies in an explicit rational box. Both are immediate here.

source
noncomputable def LeanPool.Besicovitch.barC :
ℝ

Twice the rational threshold: the chord length of the retargeted argument.

Equations
Instances For
    source
    noncomputable def LeanPool.Besicovitch.barS :
    ℝ

    The rational density threshold certified by the retargeted argument.

    Equations
    Instances For
      source
      theorem LeanPool.Besicovitch.barS_eq :
      barS = 6934 / 10000

      The rational threshold is 0.6934.

      source
      theorem LeanPool.Besicovitch.barC_mem_isolation_box :
      13867999999999999 / 10 ^ 16 < barC ∧ barC < 13868000000000001 / 10 ^ 16

      The rational chord lies in an explicit isolation box.

      source
      theorem LeanPool.Besicovitch.one_lt_barC_and_barC_lt_two :
      1 < barC ∧ barC < 2

      The rational chord is a genuine chord of the unit disk.

      source
      theorem LeanPool.Besicovitch.barC_pos :
      0 < barC

      The rational chord is positive.

      source
      theorem LeanPool.Besicovitch.barS_mem_isolation_box :
      6933999999999999 / 10 ^ 16 ≤ barS ∧ barS < 6934000000000001 / 10 ^ 16

      The rational threshold lies in an explicit isolation box.

      source
      theorem LeanPool.Besicovitch.half_lt_barS_and_barS_lt_one :
      1 / 2 < barS ∧ barS < 1

      The rational threshold lies strictly between one half and one.

      source
      theorem LeanPool.Besicovitch.half_lt_barS :
      1 / 2 < barS

      The rational threshold exceeds one half.

      source
      theorem LeanPool.Besicovitch.barS_lt_one :
      barS < 1

      The rational threshold is below one.

      source
      theorem LeanPool.Besicovitch.barS_pos :
      0 < barS

      The rational threshold is positive.

      source
      theorem LeanPool.Besicovitch.barS_lt_seven_tenths :
      barS < 7 / 10

      The rational threshold is below the previous record.