Documentation

HexRootsMathlib.Component

source
@[simp]
theorem HexRootsMathlib.DyadicSquare.doubled_center (s : Hex.DyadicSquare) :
center s.doubled = center s
source
@[simp]
theorem HexRootsMathlib.DyadicSquare.doubled_prec (s : Hex.DyadicSquare) :
s.doubled.prec = s.prec - 1
source
@[simp]
theorem HexRootsMathlib.DyadicSquare.doubled_halfWidth (s : Hex.DyadicSquare) :
halfWidth s.doubled = 2 * halfWidth s
source
theorem HexRootsMathlib.DyadicSquare.closedSquare_subset_doubled (s : Hex.DyadicSquare) :
closedSquare s ⊆ closedSquare s.doubled

A square is contained in its concentric doubled square.

source
theorem HexRootsMathlib.DyadicSquare.closedDisc_subset_doubled (s : Hex.DyadicSquare) :
closedDisc s ⊆ closedSquare s.doubled

The circumscribed closed disc is contained in the concentric doubled square; this is the geometric reason certified re-entry must double.

source
def HexRootsMathlib.Component.WellFormed (c : Hex.Component) :
Prop

The structural invariant actually required of a worklist component: there is a first square and every square has its precision. Connectivity is an algorithmic optimization and is not needed by soundness.

Equations
Instances For
    source
    def HexRootsMathlib.Component.region (c : Hex.Component) :
    Set ℂ

    The union of the closed squares retained by a component.

    Equations
    Instances For
      source
      theorem HexRootsMathlib.Component.cauchy_wellFormed (p : Hex.ZPoly) (h : 0 < Hex.DensePoly.natDegree p) :
      WellFormed (Hex.Component.cauchy p h)

      The initial Cauchy component is a nonempty singleton component.

      source
      theorem HexRootsMathlib.Component.isRoot_mem_cauchy (p : Hex.ZPoly) (h : 0 < Hex.DensePoly.natDegree p) {z : ℂ} (hz : (toPolyℂ p).IsRoot z) :
      z ∈ region (Hex.Component.cauchy p h)

      Component-level restatement of executable Cauchy coverage.

      source
      theorem HexRootsMathlib.Component.region_subset_encSquare (c : Hex.Component) :
      region c ⊆ DyadicSquare.closedSquare (Hex.encSquare c.squares)

      The executable enclosing square contains the union of all input squares, without a common-precision or connectivity hypothesis.

      source
      theorem HexRootsMathlib.Component.region_subset_doubledEnc (c : Hex.Component) :
      region c ⊆ DyadicSquare.closedSquare (Hex.encSquare c.squares).doubled

      The doubled enclosing square used by NK certification contains the whole input component region.

      source
      def HexRootsMathlib.DyadicRootIsolation.region {p : Hex.ZPoly} (iso : Hex.DyadicRootIsolation p) :
      Set ℂ

      The certified region selected by an atom certificate. Reflected certificates preserve the region kind of their source certificate.

      Equations
      Instances For
        source
        def HexRootsMathlib.Certified.region {p : Hex.ZPoly} :
        Hex.Certified p → Set ℂ

        The region whose root count is asserted by a certified result.

        Equations
        Instances For
          source
          def HexRootsMathlib.Certified.count {p : Hex.ZPoly} :
          Hex.Certified p → ℕ

          The root count carried by a certified result.

          Equations
          Instances For
            source
            theorem HexRootsMathlib.Certified.count_pos {p : Hex.ZPoly} (r : Hex.Certified p) :
            0 < count r

            Every certificate claims at least one root.

            source
            @[simp]
            theorem HexRootsMathlib.Certified.toComponent_squares {p : Hex.ZPoly} (r : Hex.Certified p) :
            r.toComponent.squares = #[r.square.doubled]
            source
            @[simp]
            theorem HexRootsMathlib.Certified.toComponent_count {p : Hex.ZPoly} (r : Hex.Certified p) :
            r.toComponent.candidateK = count r
            source
            @[simp]
            theorem HexRootsMathlib.Certified.toComponent_prec {p : Hex.ZPoly} (r : Hex.Certified p) :
            r.toComponent.prec = r.square.prec - 1
            source
            @[simp]
            theorem HexRootsMathlib.Certified.toComponent_region {p : Hex.ZPoly} (r : Hex.Certified p) :
            Component.region r.toComponent = DyadicSquare.closedSquare r.square.doubled
            source
            theorem HexRootsMathlib.Certified.toComponent_wellFormed {p : Hex.ZPoly} (r : Hex.Certified p) :
            Component.WellFormed r.toComponent

            Re-entry always constructs a nonempty common-precision component.

            source
            theorem HexRootsMathlib.Certified.toComponent_count_pos {p : Hex.ZPoly} (r : Hex.Certified p) :
            0 < r.toComponent.candidateK

            Re-entry preserves candidate-count positivity; together with toComponent_wellFormed this is the loop kernel's re-entry contract.

            source
            theorem HexRootsMathlib.Certified.region_subset_doubled {p : Hex.ZPoly} (r : Hex.Certified p) :
            region r ⊆ DyadicSquare.closedSquare r.square.doubled

            The doubled square retained on re-entry contains the certified region, for both atom certificate forms and for clusters.

            source
            theorem HexRootsMathlib.Certified.square_subset_toComponent {p : Hex.ZPoly} (r : Hex.Certified p) :
            DyadicSquare.closedSquare r.square ⊆ Component.region r.toComponent

            Re-entry contains the stored square, independently of certificate form.

            source
            theorem HexRootsMathlib.Certified.disc_subset_toComponent {p : Hex.ZPoly} (r : Hex.Certified p) :
            DyadicSquare.closedDisc r.square ⊆ Component.region r.toComponent

            Re-entry contains the stored circumscribed disc, independently of certificate form. This stronger conservative fact is useful to the loop kernel, which need not inspect the atom-witness disjunction.

            source
            theorem HexRootsMathlib.Certified.region_subset_toComponent {p : Hex.ZPoly} (r : Hex.Certified p) :
            region r ⊆ Component.region r.toComponent

            The worklist region of toComponent contains the certified region.