`DihedralAngleData`

definition

show as: view math explainer →

module: IndisputableMonolith.Geometry.DihedralAngle
domain: Geometry
line: 56 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Geometry.DihedralAngle on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  53/-! ## §1. Dihedral angle data -/
  54
  55/-- The data of a dihedral angle: a cosine value in `[-1, 1]`. -/
  56structure DihedralAngleData where
  57  cosine : ℝ
  58  cosine_lb : -1 ≤ cosine
  59  cosine_ub : cosine ≤ 1
  60
  61/-- The dihedral angle itself, via `arccos`. -/
  62def DihedralAngleData.theta (d : DihedralAngleData) : ℝ := Real.arccos d.cosine
  63
  64/-- `θ ∈ [0, π]`. -/
  65theorem theta_nonneg (d : DihedralAngleData) : 0 ≤ d.theta :=
  66  Real.arccos_nonneg d.cosine
  67
  68theorem theta_le_pi (d : DihedralAngleData) : d.theta ≤ Real.pi :=
  69  Real.arccos_le_pi d.cosine
  70
  71/-- `cos θ = cosine` by construction. -/
  72theorem cos_theta (d : DihedralAngleData) : Real.cos d.theta = d.cosine := by
  73  unfold DihedralAngleData.theta
  74  exact Real.cos_arccos d.cosine_lb d.cosine_ub
  75
  76/-! ## §2. Canonical values -/
  77
  78/-- A regular tetrahedron's dihedral angle has cosine `1/3`. -/
  79def regular_tet_dihedral : DihedralAngleData :=
  80  { cosine := 1 / 3
  81  , cosine_lb := by norm_num
  82  , cosine_ub := by norm_num
  83  }
  84
  85/-- The regular-tetrahedron dihedral angle is `arccos(1/3) ≈ 70.53°`. -/
  86theorem regular_tet_dihedral_theta :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.