Geometry Regge Rigorous Foundation Conformal Sq Edge Cont Diff

A smooth map of edge lengths

The declaration conformalSqEdge_contDiff is a theorem in the machine-checked library of formal theorems. It states that a specific map, called the conformal squared-edge map, is smooth. In plain terms, this map takes four numbers, one for each vertex of a tetrahedron, and produces six numbers, one for each edge, by scaling a fixed background length by the exponential of the average of the two vertex numbers. The theorem proves this map is infinitely differentiable, meaning it has no sharp corners or jumps; small changes in the vertex numbers produce small changes in the edge lengths.

This smoothness is not an assumption. It is a proved result, derived from the fact that the map is built from the exponential function, which is smooth, and from addition and multiplication by constants, which are also smooth. The theorem holds for any choice of the background length and for any order of differentiability. At the special point where all four vertex numbers are zero, the map returns the regular flat tetrahedron with all edges equal to the background length, a fact also proved in the library.

In Recognition Science, this theorem is the first rung of a larger program. The goal is to prove a component theorem in Regge calculus, a discrete approach to general relativity where spacetime is built from flat tetrahedra. The component theorem states that a certain matrix entry, the Hessian of the Regge action under the conformal edge ansatz, equals minus the area of the shared face between two tetrahedra. The smoothness theorem is a necessary ingredient because the proof will use calculus on the space of edge lengths, and calculus requires smooth functions.

The theorem does not, by itself, prove the component theorem. The path to that result requires three external classical hypotheses: the Schläfli identity, the dihedral cosine formula via Cayley-Menger cofactors, and the smoothness of the dihedral angle on the realisability cone. These are imported from the standard Regge calculus literature, not derived within the framework. The conformalSqEdge_contDiff theorem is the proven foundation on which that future work will rest.

/-- 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

/-- At ξ ≡ 0, the conformal squared-edge map gives the regular constant ℓ₀². -/
theorem conformalSqEdge_at_zero (ℓ₀ : ℝ) :
    conformalSqEdge ℓ₀ (fun _ => 0) = (fun _ => ℓ₀ ^ 2) := by
  funext e
  unfold conformalSqEdge
  simp [Real.exp_zero]

What this page does not claim

The theorem does not prove the Regge component theorem M_ij = -area(f_ij). The theorem does not derive the Schläfli identity or the dihedral cosine formula. The theorem does not establish the smoothness of the dihedral angle on the realisability cone.

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: