Rupert Counterexample

8. Computational Step🔗

Theorem8.1
uses 0used by 1XL∃∀N

There exists a valid solution table whose zeroth row covers

\begin{align*} \theta_1,\theta_2&\in[0,2\pi/15] \subset [0,0.42], \\ \varphi_1&\in [0,\pi] \subset [0,3.15],\\ \varphi_2&\in [0,\pi/2] \subset [0,1.58],\\ \alpha &\in [-\pi/2,\pi/2] \subset [-1.58,1.58]. \end{align*}

Proof for Theorem 8.1
uses 0

By exhibiting the table and running the validity checking algorithm.

Theorem8.2
Group: Soundness of table rows and propagated non-Rupert certificates. (3)
Group member previews
Preview
Theorem 8.3
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

If a global node in the solution tree is valid, then there is no Rupert solution for its interval.

Lean code for Theorem8.2●1 theorem
  • theoremdefined in Noperthedron/SolutionTable/Global.lean
    complete
    theorem Noperthedron.Solution.valid_global_imp_no_rupert (row : Solution.Row)
  (hrow : row.ValidGlobal) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.valid_global_imp_no_rupert
  (row : Solution.Row)
  (hrow : row.ValidGlobal) :
  ¬∃ q ∈ row.interval.toReal,
      RupertPose q exactPolyhedron.hull
Proof for Theorem 8.2
uses 1
Theorem8.3
Group: Soundness of table rows and propagated non-Rupert certificates. (3)
Group member previews
Preview
Theorem 8.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

If a local node in the solution tree is valid, then there is no Rupert solution for its interval.

Lean code for Theorem8.3●1 theorem
  • theoremdefined in Noperthedron/SolutionTable/Local.lean
    complete
    theorem Noperthedron.Solution.valid_local_imp_no_rupert (row : Solution.Row)
  (hrow : row.ValidLocal) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.valid_local_imp_no_rupert
  (row : Solution.Row)
  (hrow : row.ValidLocal) :
  ¬∃ q ∈ row.interval.toReal,
      RupertPose q exactPolyhedron.hull
Proof for Theorem 8.3
Proof uses 3
Proof dependency previews
Preview
Lemma 2.1.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.
Theorem8.4
Group: Soundness of table rows and propagated non-Rupert certificates. (3)
Group member previews
Preview
Theorem 8.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

If we have a valid solution table, and in particular its ith row is valid, then there is no Rupert solution of the interval of its ith row.

Lean code for Theorem8.4●5 theorems
  • theoremdefined in Noperthedron/SolutionTable.lean
    complete
    theorem Noperthedron.Solution.Row.valid_imp_not_rupert_ix
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid : Solution.RowsValidAt get size) (i : ℕ) (hi : i < size) :
  ¬∃ q ∈ (get i).interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.Row.valid_imp_not_rupert_ix
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid :
    Solution.RowsValidAt get size)
  (i : ℕ) (hi : i < size) :
  ¬∃ q ∈ (get i).interval.toReal,
      RupertPose q exactPolyhedron.hull
  • theoremdefined in Noperthedron/SolutionTable.lean
    complete
    theorem Noperthedron.Solution.valid_split_imp_no_rupert (get : ℕ → Solution.Row)
  (size : ℕ) (rowsValid : Solution.RowsValidAt get size)
  (row : Solution.Row) (hr : Solution.Row.ValidSplitAt get size row)
  (hlt : row.ID < size) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.valid_split_imp_no_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid :
    Solution.RowsValidAt get size)
  (row : Solution.Row)
  (hr :
    Solution.Row.ValidSplitAt get size
      row)
  (hlt : row.ID < size) :
  ¬∃ q ∈ row.interval.toReal,
      RupertPose q exactPolyhedron.hull
  • theoremdefined in Noperthedron/SolutionTable.lean
    complete
    theorem Noperthedron.Solution.valid_single_param_split_imp_no_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid : Solution.RowsValidAt get size) (row : Solution.Row)
  (hr : Solution.Row.ValidSingleParamSplitAt get size row) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.valid_single_param_split_imp_no_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid :
    Solution.RowsValidAt get size)
  (row : Solution.Row)
  (hr :
    Solution.Row.ValidSingleParamSplitAt
      get size row) :
  ¬∃ q ∈ row.interval.toReal,
      RupertPose q exactPolyhedron.hull
  • theoremdefined in Noperthedron/SolutionTable.lean
    complete
    theorem Noperthedron.Solution.valid_full_split_imp_no_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid : Solution.RowsValidAt get size) (row : Solution.Row)
  (_hgt : row.ID < row.IDfirstChild) (_hlt : row.ID < size)
  (hi :
    Solution.HasIntervalsAt get size row.IDfirstChild
      (Solution.cubeFold
        [Solution.Interval.lower_half, Solution.Interval.upper_half]
        row.interval Solution.Param.splitOrder)) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.valid_full_split_imp_no_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid :
    Solution.RowsValidAt get size)
  (row : Solution.Row)
  (_hgt : row.ID < row.IDfirstChild)
  (_hlt : row.ID < size)
  (hi :
    Solution.HasIntervalsAt get size
      row.IDfirstChild
      (Solution.cubeFold
        [Solution.Interval.lower_half,
          Solution.Interval.upper_half]
        row.interval
        Solution.Param.splitOrder)) :
  ¬∃ q ∈ row.interval.toReal,
      RupertPose q exactPolyhedron.hull
  • theoremdefined in Noperthedron/SolutionTable.lean
    complete
    theorem Noperthedron.Solution.valid_param_split_imp_no_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid : Solution.RowsValidAt get size) (row : Solution.Row)
  (p : Solution.Param)
  (h : Solution.Row.ValidSplitParamAt get size row p) :
  ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.valid_param_split_imp_no_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid :
    Solution.RowsValidAt get size)
  (row : Solution.Row)
  (p : Solution.Param)
  (h :
    Solution.Row.ValidSplitParamAt get
      size row p) :
  ¬∃ q ∈ row.interval.toReal,
      RupertPose q exactPolyhedron.hull
Proof for Theorem 8.4
Proof uses 2
Proof dependency previews
Preview
Theorem 8.2
Loading preview
Proof dependency preview content is loaded from the rendered-fragment cache.

By a mutual induction on the number of rows left in the table following the ith. This is because validity constrains each row to only refer to later entries. Appeal inductively to this same theorem if the row splits into other nodes in the tree, or appeal to Theorem or Theorem at the leaves.

Corollary8.5
Group: Soundness of table rows and propagated non-Rupert certificates. (3)
Group member previews
Preview
Theorem 8.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

If we have a valid solution table, then there is no Rupert solution of the interval of its zeroth row.

Lean code for Corollary8.5●1 theorem
  • theoremdefined in Noperthedron/SolutionTable.lean
    complete
    theorem Noperthedron.Solution.Row.valid_imp_not_rupert (get : ℕ → Solution.Row)
  (size : ℕ) (rowsValid : Solution.RowsValidAt get size)
  (hz : 0 < size) :
  ¬∃ q ∈ (get 0).interval.toReal, RupertPose q exactPolyhedron.hull
    theorem Noperthedron.Solution.Row.valid_imp_not_rupert
  (get : ℕ → Solution.Row) (size : ℕ)
  (rowsValid :
    Solution.RowsValidAt get size)
  (hz : 0 < size) :
  ¬∃ q ∈ (get 0).interval.toReal,
      RupertPose q exactPolyhedron.hull
Proof for Corollary 8.5
uses 1

Immediate special case of Theorem 8.4.