theorem RationalApprox.sinℚ_approx (x : ℝ) :
  |Real.sin x - RationalApprox.sinℚ x| ≤
    |x| ^ 27 / ↑(Nat.factorial 27)

theorem RationalApprox.cosℚ_approx (x : ℝ) :
  |Real.cos x - RationalApprox.cosℚ x| ≤
    |x| ^ 26 / ↑(Nat.factorial 26)

theorem RationalApprox.sinℚ_approx' (x : ℝ)
  (hx : x ∈ Set.Icc (-4) 4) :
  |Real.sin x - RationalApprox.sinℚ x| ≤
    RationalApprox.κ / 7

theorem RationalApprox.cosℚ_approx' (x : ℝ)
  (hx : x ∈ Set.Icc (-4) 4) :
  |Real.cos x - RationalApprox.cosℚ x| ≤
    RationalApprox.κ / 7

theorem RationalApprox.norm_le_delta_sqrt_dims
  {m n : ℕ} {δ : ℝ}
  (A : Matrix (Fin m) (Fin n) ℝ)
  (hδ : 0 < δ)
  (hle :
    ∀ (i : Fin m) (j : Fin n),
      |A i j| ≤ δ) :
  ‖LinearMap.toContinuousLinearMap
        (Matrix.toEuclideanLin A)‖ ≤
    δ * √(↑m * ↑n)

theorem RationalApprox.norm_matrix_actual_approx_le_kappa
  {m n : ↥(Finset.Icc 1 3)}
  (A :
    Matrix (Fin ↑m) (Fin ↑n)
      RationalApprox.DistLeKappaEntry)
  (x y : ↑(Set.Icc (-4) 4)) :
  ‖RationalApprox.clinActual A ↑x ↑y -
        RationalApprox.clinApprox A ↑x
          ↑y‖ ≤
    RationalApprox.κ

theorem RationalApprox.R_difference_norm_bounded
  (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR α - RationalApprox.rotRℚℝ α‖ ≤
    RationalApprox.κ

theorem RationalApprox.R'_difference_norm_bounded
  (α : ℝ) (hα : α ∈ Set.Icc (-4) 4) :
  ‖rotR' α - RationalApprox.rotR'ℚℝ α‖ ≤
    RationalApprox.κ

theorem RationalApprox.M_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotM θ φ - RationalApprox.rotMℚℝ θ φ‖ ≤
    RationalApprox.κ

theorem RationalApprox.Mθ_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMθ θ φ -
        RationalApprox.rotMθℚℝ θ φ‖ ≤
    RationalApprox.κ

theorem RationalApprox.Mφ_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖rotMφ θ φ -
        RationalApprox.rotMφℚℝ θ φ‖ ≤
    RationalApprox.κ

theorem RationalApprox.X_difference_norm_bounded
  (θ φ : ℝ) (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖vecXL θ φ -
        RationalApprox.vecXLℚℝ θ φ‖ ≤
    RationalApprox.κ

theorem RationalApprox.Rℚ_norm_bounded (α : ℝ)
  (hα : α ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotRℚℝ α‖ ≤
    1 + RationalApprox.κ

theorem RationalApprox.Mℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theorem RationalApprox.R'ℚ_norm_bounded (α : ℝ)
  (hα : α ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotR'ℚℝ α‖ ≤
    1 + RationalApprox.κ

theorem RationalApprox.Mθℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMθℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theorem RationalApprox.Mφℚ_norm_bounded {θ φ : ℝ}
  (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4) :
  ‖RationalApprox.rotMφℚℝ θ φ‖ ≤
    1 + RationalApprox.κ

theorem RationalApprox.norm_sub_le_prod {n m : ℕ}
  (mv : RationalApprox.MatVec n m) (κ : ℝ)
  (κ_pos : κ > 0)
  (hκ : mv.DiffBoundedBy κ) :
  ‖mv.compA - mv.compB‖ ≤
    ↑mv.size * κ * mv.maxNormList.prod

theorem RationalApprox.bounds_kappa_M {P : Euc(3)}
  {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotM ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ

theorem RationalApprox.bounds_kappa_Mθ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMθ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMθℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ

theorem RationalApprox.bounds_kappa_Mφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotMφ ↑↑θ ↑↑φ) P) (toR2 w) -
        ↑((RationalApprox.rotMφℚ ↑θ ↑φ)
              P_ ⬝ᵥ
            w)‖ ≤
    3 * RationalApprox.κ

theorem RationalApprox.bounds_kappa_RM
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ ((rotR ↑↑α) ((rotM ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    4 * RationalApprox.κ

theorem RationalApprox.bounds_kappa_R'M
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR' ↑↑α) ((rotM ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotR'ℚ ↑α)
              ((RationalApprox.rotMℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    4 * RationalApprox.κ

theorem RationalApprox.bounds_kappa_RMθ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR ↑↑α) ((rotMθ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMθℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    4 * RationalApprox.κ

theorem RationalApprox.bounds_kappa_RMφ
  {P : Euc(3)} {P_ : Fin 3 → ℚ}
  {α θ φ : ↑(Set.Icc (-4) 4)}
  {w : Fin 2 → ℚ} (hP : ‖P‖ ≤ 1)
  (approx :
    ‖P - toR3 P_‖ ≤ RationalApprox.κ)
  (hw : ‖toR2 w‖ = 1) :
  ‖inner ℝ
          ((rotR ↑↑α) ((rotMφ ↑↑θ ↑↑φ) P))
          (toR2 w) -
        ↑((RationalApprox.rotRℚ ↑α)
              ((RationalApprox.rotMφℚ ↑θ
                  ↑φ)
                P_) ⬝ᵥ
            w)‖ ≤
    4 * RationalApprox.κ

theorem RationalApprox.GlobalTheorem.rational_global
  {ι : Type} [Fintype ι] [Nonempty ι]
  (p : Pose ℚ) (ε : ℚ) (hε : 0 ≤ ε)
  (poly : GoodPoly ι)
  (poly_ : Polyhedron ι (Fin 3 → ℚ))
  (happrox :
    RationalApprox.κApproxPoly
      poly.vertices poly_)
  (pc :
    RationalApprox.GlobalTheorem.RationalGlobalTheoremPrecondition
      poly poly_ happrox p ε) :
  ¬∃ q ∈ Metric.closedBall p.toReal ↑ε,
      RupertPose q poly.hull

theorem RationalApprox.ek_spanning_imp_e_spanning
  (P P' : Local.Triangle)
  (hk : RationalApprox.κApproxTri P P')
  (hP : ∀ (i : Fin 3), ‖P i‖ ≤ 1)
  {θ φ ε : ℝ} (hθ : θ ∈ Set.Icc (-4) 4)
  (hφ : φ ∈ Set.Icc (-4) 4)
  (hspan : P'.κSpanning θ φ ε) :
  P.Spanning θ φ ε

theorem RationalApprox.bounds_kappa3_X
  {P P_ : Euc(3)}
  {θ φ : ↑(Set.Icc (-4) 4)} (hP : ‖P‖ ≤ 1)
  (Papprox :
    ‖P - P_‖ ≤ RationalApprox.κ) :
  ‖inner ℝ (vecX ↑θ ↑φ) P -
        inner ℝ
          (RationalApprox.vecXℚℝ ↑θ ↑φ)
          P_‖ ≤
    3 * RationalApprox.κ

theorem RationalApprox.bounds_kappa3_M
  {P Q Q_ P_ : Euc(3)}
  {θ φ : ↑(Set.Icc (-4) 4)} (hP : ‖P‖ ≤ 1)
  (hQ : ‖Q‖ ≤ 1)
  (Papprox : ‖P - P_‖ ≤ RationalApprox.κ)
  (Qapprox :
    ‖Q - Q_‖ ≤ RationalApprox.κ) :
  ‖inner ℝ ((rotM ↑θ ↑φ) P)
          ((rotM ↑θ ↑φ) Q) -
        inner ℝ
          ((RationalApprox.rotMℚℝ ↑θ ↑φ)
            P_)
          ((RationalApprox.rotMℚℝ ↑θ ↑φ)
            Q_)‖ ≤
    5 * RationalApprox.κ