8. Computational Step
We define rational approximations of the 90 noperthedron vertices by
\lfloor x \cdot 10^{16} \rfloor/10^{16}.
The rational vertex set \mathtt{nopertQ} is a \kappa-rational approximation
of the Noperthedron.
Lean code for Theorem8.2●1 definition
Associated Lean declarations
-
defdefined in Noperthedron/Checker/KappaApprox.leancomplete
def Noperthedron.KappaApprox.exact_κApprox_python : RationalApprox.κApproxPoly { v := exactVertex } { v := pythonVertex }
def Noperthedron.KappaApprox.exact_κApprox_python : RationalApprox.κApproxPoly { v := exactVertex } { v := pythonVertex }
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*}
By exhibiting the table and running the validity checking algorithm.
Formalized as \mathtt{Noperthedron.NativeCaseAnalysis.solutionTable} in the
build-on-demand \mathtt{NativeCaseAnalysis} library (checked with
\mathtt{native\_decide}) and independently in the kernel-only
\mathtt{KernelCaseAnalysis} library (checked with \mathtt{decide +kernel},
using only the standard axioms); both are kept out of the default build targets
so that CI runs stay fast.
If a global node in the solution tree is valid, then there is no Rupert solution for its interval.
Lean code for Theorem8.4●1 theorem
Associated Lean declarations
-
theoremdefined in Noperthedron/SolutionTable/Global.leancomplete
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
If a local node in the solution tree is valid, then there is no Rupert solution for its interval.
Lean code for Theorem8.5●1 theorem
Associated Lean declarations
-
theoremdefined in Noperthedron/SolutionTable/Local.leancomplete
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
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.6●2 theorems
Associated Lean declarations
-
theoremdefined in Noperthedron/SolutionTable.leancomplete
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
No row of a valid table admits a Rupert pose. Strong induction on `size - i`: a split row only refers to rows with larger IDs, and leaves are handled by the global/local theorems.
-
theoremdefined in Noperthedron/SolutionTable.leancomplete
theorem Noperthedron.Solution.valid_split_imp_no_rupert (get : ℕ → Solution.Row) (size : ℕ) (row : Solution.Row) (hr : Solution.Row.ValidSplitAt get size row) (ih : ∀ (j : ℕ), row.ID < j → j < size → ¬∃ q ∈ (get j).interval.toReal, RupertPose q exactPolyhedron.hull) : ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
theorem Noperthedron.Solution.valid_split_imp_no_rupert (get : ℕ → Solution.Row) (size : ℕ) (row : Solution.Row) (hr : Solution.Row.ValidSplitAt get size row) (ih : ∀ (j : ℕ), row.ID < j → j < size → ¬∃ q ∈ (get j).interval.toReal, RupertPose q exactPolyhedron.hull) : ¬∃ q ∈ row.interval.toReal, RupertPose q exactPolyhedron.hull
By strong 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.
For a split row, every point in its interval belongs to a child interval at a
larger index, so the induction hypothesis excludes a Rupert solution there.
At a leaf, apply Theorem or
Theorem.
If we have a valid solution table, then there is no Rupert solution of the interval of its zeroth row.
Lean code for Corollary8.7●1 theorem
Associated Lean declarations
-
theoremdefined in Noperthedron/SolutionTable.leancomplete
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
Immediate special case of Theorem 8.6.