theorem Noperthedron.exists_solution_tableNoperthedron.exists_solution_table : ∃ tab, True :
  ∃ tabSolution.ValidTable, TrueTrue : Prop`True` is a proposition and has only an introduction rule, `True.intro : True`.
In other words, `True` is simply true, and has a canonical proof, `True.intro`
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)

theorem Noperthedron.Solution.valid_global_imp_no_rupertNoperthedron.Solution.valid_global_imp_no_rupert (row : Solution.Row) (hrow : row.ValidGlobal) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
  (rowSolution.Row : Solution.RowNoperthedron.Solution.Row : TypeA `Solution.Row` aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file.
IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.
)
  (hrowrow.ValidGlobal : rowSolution.Row.ValidGlobalNoperthedron.Solution.Row.ValidGlobal (row : Solution.Row) : PropAssertion that a row constitutes a valid application of the rational global theorem. ) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Solution.valid_local_imp_no_rupertNoperthedron.Solution.valid_local_imp_no_rupert (row : Solution.Row) (hrow : row.ValidLocal) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
  (rowSolution.Row : Solution.RowNoperthedron.Solution.Row : TypeA `Solution.Row` aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file.
IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.
)
  (hrowrow.ValidLocal : rowSolution.Row.ValidLocalNoperthedron.Solution.Row.ValidLocal (row : Solution.Row) : PropAssertion that a row constitutes a valid application of the rational global theorem. ) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Solution.Row.valid_imp_not_rupert_ixNoperthedron.Solution.Row.valid_imp_not_rupert_ix (tab : Solution.Table) (i : ℕ) (tab_valid : tab.RowsValid)
  (row : Solution.Row) (row_valid : Solution.Row.ValidIx tab i row) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
  (tabSolution.Table : Solution.TableNoperthedron.Solution.Table : Type) (iℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
)
  (tab_validtab.RowsValid : tabSolution.Table.RowsValidNoperthedron.Solution.Table.RowsValid (tab : Solution.Table) : Prop)
  (rowSolution.Row : Solution.RowNoperthedron.Solution.Row : TypeA `Solution.Row` aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file.
IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.
)
  (row_validSolution.Row.ValidIx tab i row :
    Solution.Row.ValidIxNoperthedron.Solution.Row.ValidIx (tab : Solution.Table) (i : ℕ) (row : Solution.Row) : Prop tabSolution.Table iℕ rowSolution.Row) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Solution.valid_split_imp_no_rupertNoperthedron.Solution.valid_split_imp_no_rupert (tab : Solution.Table) (row : Solution.Row) (htab : tab.RowsValid)
  (hr : Solution.Row.ValidSplit tab row) (hlt : row.ID < Array.size tab) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
  (tabSolution.Table : Solution.TableNoperthedron.Solution.Table : Type)
  (rowSolution.Row : Solution.RowNoperthedron.Solution.Row : TypeA `Solution.Row` aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file.
IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.
)
  (htabtab.RowsValid : tabSolution.Table.RowsValidNoperthedron.Solution.Table.RowsValid (tab : Solution.Table) : Prop)
  (hrSolution.Row.ValidSplit tab row : Solution.Row.ValidSplitNoperthedron.Solution.Row.ValidSplit (tab : Solution.Table) (row : Solution.Row) : Prop tabSolution.Table rowSolution.Row)
  (hltrow.ID < Array.size tab : rowSolution.Row.IDNoperthedron.Solution.Row.ID (self : Solution.Row) : ℕ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. Array.sizeArray.size.{u} {α : Type u} (a : Array α) : ℕGets the number of elements stored in an array.

This is a cached value, so it is `O(1)` to access. The space allocated for an array, referred to as
its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
internal detail that's not observable by Lean code.
 tabSolution.Table) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Solution.valid_single_param_split_imp_no_rupertNoperthedron.Solution.valid_single_param_split_imp_no_rupert (tab : Solution.Table) (row : Solution.Row)
  (htab : tab.RowsValid) (hr : Solution.Row.ValidSingleParamSplit tab row) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
  (tabSolution.Table : Solution.TableNoperthedron.Solution.Table : Type)
  (rowSolution.Row : Solution.RowNoperthedron.Solution.Row : TypeA `Solution.Row` aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file.
IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.
)
  (htabtab.RowsValid : tabSolution.Table.RowsValidNoperthedron.Solution.Table.RowsValid (tab : Solution.Table) : Prop)
  (hrSolution.Row.ValidSingleParamSplit tab row :
    Solution.Row.ValidSingleParamSplitNoperthedron.Solution.Row.ValidSingleParamSplit (tab : Solution.Table) (row : Solution.Row) : Prop tabSolution.Table
      rowSolution.Row) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Solution.valid_full_split_imp_no_rupertNoperthedron.Solution.valid_full_split_imp_no_rupert (tab : Solution.Table) (row : Solution.Row) (htab : tab.RowsValid)
  (_hgt : row.ID < row.IDfirstChild) (_hlt : row.ID < Array.size tab)
  (hi :
    tab.HasIntervals row.IDfirstChild
      (Solution.cubeFold [Solution.Interval.lower_half, Solution.Interval.upper_half] row.interval
        [Solution.Param.θ₁, Solution.Param.φ₁, Solution.Param.θ₂, Solution.Param.φ₂, Solution.Param.α])) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
  (tabSolution.Table : Solution.TableNoperthedron.Solution.Table : Type)
  (rowSolution.Row : Solution.RowNoperthedron.Solution.Row : TypeA `Solution.Row` aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file.
IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.
)
  (htabtab.RowsValid : tabSolution.Table.RowsValidNoperthedron.Solution.Table.RowsValid (tab : Solution.Table) : Prop)
  (_hgtrow.ID < row.IDfirstChild : rowSolution.Row.IDNoperthedron.Solution.Row.ID (self : Solution.Row) : ℕ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. rowSolution.Row.IDfirstChildNoperthedron.Solution.Row.IDfirstChild (self : Solution.Row) : ℕ)
  (_hltrow.ID < Array.size tab : rowSolution.Row.IDNoperthedron.Solution.Row.ID (self : Solution.Row) : ℕ <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. Array.sizeArray.size.{u} {α : Type u} (a : Array α) : ℕGets the number of elements stored in an array.

This is a cached value, so it is `O(1)` to access. The space allocated for an array, referred to as
its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
internal detail that's not observable by Lean code.
 tabSolution.Table)
  (hitab.HasIntervals row.IDfirstChild
  (Solution.cubeFold [Solution.Interval.lower_half, Solution.Interval.upper_half] row.interval
    [Solution.Param.θ₁, Solution.Param.φ₁, Solution.Param.θ₂, Solution.Param.φ₂, Solution.Param.α]) :
    tabSolution.Table.HasIntervalsNoperthedron.Solution.Table.HasIntervals (tab : Solution.Table) (start : ℕ) (intervals : List Solution.Interval) : Prop rowSolution.Row.IDfirstChildNoperthedron.Solution.Row.IDfirstChild (self : Solution.Row) : ℕ
      (Solution.cubeFoldNoperthedron.Solution.cubeFold {α β : Type} (fs : List (α → β → β)) (b : β) : List α → List β`cubeFold fs b as`, takes a list of functions `fs` and a starting value `b` and a list of
coordinates `as` and returns a list of length `|fs|^|as|` consisting of all the ways
of folding the initial value `b` through some sequence of functions in `fs`, using values from `as`.

        [List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.Solution.Interval.lower_halfNoperthedron.Solution.Interval.lower_half (param : Solution.Param) (iv : Solution.Interval) : Solution.Interval,List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.
          Solution.Interval.upper_halfNoperthedron.Solution.Interval.upper_half (param : Solution.Param) (iv : Solution.Interval) : Solution.Interval]List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.
        rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval
        [List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.Solution.Param.θ₁Noperthedron.Solution.Param.θ₁ : Solution.Param,List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.
          Solution.Param.φ₁Noperthedron.Solution.Param.φ₁ : Solution.Param,List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.
          Solution.Param.θ₂Noperthedron.Solution.Param.θ₂ : Solution.Param,List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.
          Solution.Param.φ₂Noperthedron.Solution.Param.φ₂ : Solution.Param,List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.
          Solution.Param.αNoperthedron.Solution.Param.α : Solution.Param]List.cons.{u} {α : Type u} (head : α) (tail : List α) : List αThe list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`.

 * The recommended spelling of `[a]` in identifiers is `singleton`.)) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Solution.valid_param_split_imp_no_rupertNoperthedron.Solution.valid_param_split_imp_no_rupert (tab : Solution.Table) (row : Solution.Row) (htab : tab.RowsValid)
  (p : Solution.Param) (h : Solution.Row.ValidSplitParam tab row p) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
  (tabSolution.Table : Solution.TableNoperthedron.Solution.Table : Type)
  (rowSolution.Row : Solution.RowNoperthedron.Solution.Row : TypeA `Solution.Row` aims to closely model of exactly the data in Steininger and Yurkevich's big CSV file.
IDs start from zero. See [SY25] §7.1 for the meaning of all these fields.
)
  (htabtab.RowsValid : tabSolution.Table.RowsValidNoperthedron.Solution.Table.RowsValid (tab : Solution.Table) : Prop)
  (pSolution.Param : Solution.ParamNoperthedron.Solution.Param : Type)
  (hSolution.Row.ValidSplitParam tab row p :
    Solution.Row.ValidSplitParamNoperthedron.Solution.Row.ValidSplitParam (tab : Solution.Table) (row : Solution.Row) (param : Solution.Param) : Prop tabSolution.Table rowSolution.Row
      pSolution.Param) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ rowSolution.Row.intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)

theorem Noperthedron.Solution.Row.valid_imp_not_rupertNoperthedron.Solution.Row.valid_imp_not_rupert (tab : Solution.Table) (tab_valid : tab.RowsValid)
  (hz : 0 < Array.size tab) : ¬∃ q ∈ tab[0].interval.toReal, RupertPose q exactPolyhedron.hull
  (tabSolution.Table : Solution.TableNoperthedron.Solution.Table : Type)
  (tab_validtab.RowsValid : tabSolution.Table.RowsValidNoperthedron.Solution.Table.RowsValid (tab : Solution.Table) : Prop)
  (hz0 < Array.size tab : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` 

Conventions for notations in identifiers:

 * The recommended spelling of `<` in identifiers is `lt`. Array.sizeArray.size.{u} {α : Type u} (a : Array α) : ℕGets the number of elements stored in an array.

This is a cached value, so it is `O(1)` to access. The space allocated for an array, referred to as
its _capacity_, is at least as large as its size, but may be larger. The capacity of an array is an
internal detail that's not observable by Lean code.
 tabSolution.Table) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.∃ qPose ℝ ∈ tabSolution.Table[GetElem.getElem.{u, v, w} {coll : Type u} {idx : Type v} {elem : outParam (Type w)}
  {valid : outParam (coll → idx → Prop)} [self : GetElem coll idx elem valid] (xs : coll) (i : idx) (h : valid xs i) :
  elemThe syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic` tactic.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]` in identifiers is `getElem`.

 * The recommended spelling of `xs[i]'h` in identifiers is `getElem`.0]GetElem.getElem.{u, v, w} {coll : Type u} {idx : Type v} {elem : outParam (Type w)}
  {valid : outParam (coll → idx → Prop)} [self : GetElem coll idx elem valid] (xs : coll) (i : idx) (h : valid xs i) :
  elemThe syntax `arr[i]` gets the `i`'th element of the collection `arr`. If there
are proof side conditions to the application, they will be automatically
inferred by the `get_elem_tactic` tactic.


Conventions for notations in identifiers:

 * The recommended spelling of `xs[i]` in identifiers is `getElem`.

 * The recommended spelling of `xs[i]'h` in identifiers is `getElem`..intervalNoperthedron.Solution.Row.interval (self : Solution.Row) : Solution.Interval.toRealNoperthedron.Solution.Interval.toReal (iv : Solution.Interval) : PoseInterval ℝ,
      RupertPoseRupertPose {P : Type} [PoseLike P] (p : P) (s : Set Euc(3)) : PropA pose `p` demonstrates that a set `s` is rupert if the closure of the
`p`-inner-shadow of `s` is a subset of the interior of the
`p`-outer-shadow of `s`.
 qPose ℝ exactPolyhedronNoperthedron.exactPolyhedron : Polyhedron VertexIndex Euc(3).hullPolyhedron.hull {ι : Type} [Fintype ι] (poly : Polyhedron ι Euc(3)) : Set Euc(3)