Documentation

LeanPool.Besicovitch.Certificates.EndpointBridge

The certified six-point endpoint #

This file transfers the exact polynomial certificate to the natural radical endpoint and identifies the constants defined from that endpoint.

source
noncomputable def LeanPool.Besicovitch.certifiedEndpointPair :
ℝ × ℝ

The unique endpoint pair isolated by the exact polynomial certificate.

Equations
Instances For
    source
    theorem LeanPool.Besicovitch.certifiedEndpointPair_isEndpointPolynomialPair :
    IsEndpointPolynomialPair certifiedEndpointPair.1 certifiedEndpointPair.2

    The certified pair satisfies the signed polynomial endpoint system.

    source
    theorem LeanPool.Besicovitch.certifiedEndpointPair_isEndpointPair :
    IsEndpointPair certifiedEndpointPair.1 certifiedEndpointPair.2

    The certified polynomial pair is a solution of the natural radical system.

    source
    theorem LeanPool.Besicovitch.IsEndpointPolynomialPair.eq_certifiedEndpointPair {c B : ℝ} (h : IsEndpointPolynomialPair c B) :
    (c, B) = certifiedEndpointPair

    Every signed polynomial endpoint pair is the certified pair.

    source
    theorem LeanPool.Besicovitch.IsEndpointPair.eq_certifiedEndpointPair {c B : ℝ} (h : IsEndpointPair c B) :
    (c, B) = certifiedEndpointPair

    Every natural radical endpoint pair is the certified pair.

    source
    theorem LeanPool.Besicovitch.exists_isEndpointPair :
    ∃ (c : ℝ) (B : ℝ), IsEndpointPair c B

    A natural radical endpoint pair exists.

    source
    theorem LeanPool.Besicovitch.cStar_eq_certifiedEndpointPair_fst :
    cStar = certifiedEndpointPair.1

    The first coordinate of the certified pair is exactly cStar.

    source
    theorem LeanPool.Besicovitch.certifiedEndpointPair_radicands_pos :
    0 < (certifiedEndpointPair.2 ^ 2 - 1) / 2 ∧ 0 < (certifiedEndpointPair.2 ^ 2 + (4 * certifiedEndpointPair.1 ^ 2 - 2 * certifiedEndpointPair.1 - certifiedEndpointPair.2) ^ 2) / 2 - certifiedEndpointPair.1 ^ 2

    The certified endpoint radicands are strictly positive.

    source
    theorem LeanPool.Besicovitch.certifiedEndpointPair_second_mem_isolation_box :
    2873744161801659 / 10 ^ 15 < certifiedEndpointPair.2 ∧ certifiedEndpointPair.2 < 2873744161801662 / 10 ^ 15

    The certified second coordinate lies in its strict rational isolation interval.

    source
    theorem LeanPool.Besicovitch.cStar_mem_isolation_box :
    13866128436518096 / 10 ^ 16 < cStar ∧ cStar < 13866128436518100 / 10 ^ 16

    cStar lies strictly inside the certified rational isolation interval.

    source
    theorem LeanPool.Besicovitch.sStar_mem_isolation_box :
    6933064218259048 / 10 ^ 16 < sStar ∧ sStar < 6933064218259050 / 10 ^ 16

    sStar lies strictly inside the half-coordinate isolation interval.

    source
    theorem LeanPool.Besicovitch.sStar_le_6934_div_10000_certified :
    sStar ≤ 6934 / 10000

    The exact isolation interval puts sStar below 0.6934.

    source
    theorem LeanPool.Besicovitch.half_lt_sStar_and_sStar_lt_one_certified :
    1 / 2 < sStar ∧ sStar < 1

    The certified endpoint lies in the elementary range needed by the six-point argument.

    source
    theorem LeanPool.Besicovitch.half_lt_sStar :
    1 / 2 < sStar

    The six-point endpoint is larger than one half.

    source
    theorem LeanPool.Besicovitch.sStar_lt_one :
    sStar < 1

    The six-point endpoint is smaller than one.

    source
    theorem LeanPool.Besicovitch.one_lt_cStar_and_cStar_lt_two :
    1 < cStar ∧ cStar < 2

    Twice the endpoint lies strictly between one and two.

    source
    theorem LeanPool.Besicovitch.sStar_pos :
    0 < sStar

    The six-point endpoint is positive.

    source
    theorem LeanPool.Besicovitch.cStar_pos :
    0 < cStar

    Twice the six-point endpoint is positive.