Geometry Regge Rigorous Foundation Dihedral Structure

Dihedral angles as structured data

A dihedral angle is the angle between two faces of a tetrahedron, measured along their shared edge. In classical geometry, these angles are not arbitrary: they are determined by the six edge lengths, and they vary smoothly as the tetrahedron is deformed without collapsing. The Recognition Science declaration DihedralStructure packages exactly this classical fact as a formal object: a function that assigns to every non-degenerate tetrahedron and every one of its six edges a real number between 0 and π, together with a named hypothesis that this assignment is smooth in the squared edge lengths.

The structure is deliberately minimal. It does not define the dihedral angle from the edge lengths; it only records the properties such a definition must have. The angle is bounded between 0 and π, which matches the geometric meaning of an angle between two planes. The smoothness hypothesis is marked as external: classically it follows from the Cayley-Menger cofactor formula, but the formal library does not yet prove that connection. The declaration also includes two concrete examples, the regular and right-angle unit tetrahedra, each verified to be non-degenerate, so the structure is not empty.

This object is a stepping stone, not a destination. The full goal is a Regge component theorem stating that a certain Hessian matrix entry equals minus the area of a shared face. That theorem requires three classical ingredients: Schläfli's identity, the dihedral cosine formula, and smoothness of the dihedral angle. DihedralStructure supplies the third as a hypothesis, while the first two are recorded as separate named assumptions. The machine-checked library proves the smoothness of the Cayley-Menger volume polynomial and of the conformal edge map, but it does not yet bridge from those to the dihedral angle itself.

What the declaration establishes, then, is a precise vocabulary for talking about dihedral angles in a formal setting. It tells a reader what properties any acceptable definition must satisfy, and it names the gap between the classical theory and the formal one. It does not claim to have closed that gap. The work of deriving the dihedral angle from the Cayley-Menger minors, and of proving Schläfli's identity from first principles, remains open and is explicitly listed as future work.

/-- A dihedral-angle datum: a smooth assignment of dihedral angles to
non-degenerate tetrahedra.  In a future expansion this will be replaced
by the explicit Cayley-Menger cosine formula. -/
structure DihedralStructure where
  /-- The dihedral angle at edge `e` of tetrahedron `T`. -/
  theta : NonDegenerateTet → Fin 6 → ℝ
  /-- Dihedral angles lie in `[0, π]`. -/
  theta_in_range : ∀ T e, 0 ≤ theta T e ∧ theta T e ≤ Real.pi
  /-- Smoothness in the squared edge data (named hypothesis; classically
  follows from the Cayley-Menger cofactor formula). -/
  theta_smooth : Prop  -- placeholder for the smoothness statement

/-- The unit regular tetrahedron is non-degenerate. -/
def regularUnitTet : NonDegenerateTet where
  sqEdge := regularUnitSqEdges
  sqEdge_pos := by
    intro i
    unfold regularUnitSqEdges
    norm_num
  cm_pos := by
    rw [cm3_regular_unit]
    norm_num

/-- The right-angle unit tetrahedron is non-degenerate. -/
def rightAngleUnitTet : NonDegenerateTet where
  sqEdge := rightAngleUnitSqEdges
  sqEdge_pos := by
    intro i
    unfold rightAngleUnitSqEdges
    fin_cases i <;> norm_num
  cm_pos := by
    rw [cm3_rightAngle_unit]
    norm_num

theorem cm3_conformal_contDiff (ℓ₀ : ℝ) (n : ℕ∞) :
    ContDiff ℝ n (fun ξ : Fin 4 → ℝ => cm3 (conformalSqEdge ℓ₀ ξ)) := by
  exact (cm3_contDiff n).comp (conformalSqEdge_contDiff ℓ₀ n)

/-- The conformal edge map is smooth in ξ (each component is `exp` of a
linear combination, which is smooth, times a positive constant). -/
theorem conformalSqEdge_contDiff (ℓ₀ : ℝ) (n : ℕ∞) :
    ContDiff ℝ n (conformalSqEdge ℓ₀) := by
  -- conformalSqEdge ℓ₀ ξ e = ℓ₀² * exp(ξ v1 + ξ v2)
  -- This is smooth in ξ via composition of smooth functions.
  -- The output is in (Fin 6 → ℝ); use contDiff_pi.
  rw [contDiff_pi]
  intro e
  -- Now we need ContDiff ℝ n (fun ξ => conformalSqEdge ℓ₀ ξ e).
  unfold conformalSqEdge
  -- Goal: ContDiff ℝ n (fun ξ => ℓ₀ ^ 2 * Real.exp (ξ (edgeVertices e).1 + ξ (edgeVertices e).2))
  have h_v1 : ContDiff ℝ n (fun ξ : Fin 4 → ℝ => ξ (edgeVertices e).1) :=
    (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin 4 => ℝ)
      (edgeVertices e).1).contDiff
  have h_v2 : ContDiff ℝ n (fun ξ : Fin 4 → ℝ => ξ (edgeVertices e).2) :=
    (ContinuousLinearMap.proj (R := ℝ) (φ := fun _ : Fin 4 => ℝ)
      (edgeVertices e).2).contDiff
  have h_sum : ContDiff ℝ n
      (fun ξ : Fin 4 → ℝ => ξ (edgeVertices e).1 + ξ (edgeVertices e).2) :=
    h_v1.add h_v2
  have h_exp_smooth : ContDiff ℝ n (Real.exp : ℝ → ℝ) := Real.contDiff_exp
  have h_exp : ContDiff ℝ n
      (fun ξ : Fin 4 → ℝ => Real.exp (ξ (edgeVertices e).1 + ξ (edgeVertices e).2)) := by
    have := ContDiff.comp (g := Real.exp) (f := fun ξ : Fin 4 → ℝ =>
              ξ (edgeVertices e).1 + ξ (edgeVertices e).2) h_exp_smooth h_sum
    simpa using this
  -- ℓ₀^2 * exp(...) is smooth via product with a constant function.
  have h_const : ContDiff ℝ n (fun _ : Fin 4 → ℝ => ℓ₀ ^ 2) := contDiff_const
  exact ContDiff.mul h_const h_exp

What this page does not claim

DihedralStructure does not define the dihedral angle from edge lengths; it only records properties such a definition must have. The smoothness of the dihedral angle is a named hypothesis, not a proved theorem. The Regge component theorem M_ij = -area(f_ij) is not proved in this module; it requires additional classical hypotheses.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/ReggeRigorousFoundation.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: