Gravity Analysis Regge4 Dschlaefli Pathwise Freudenthal4 Simplex Flat Schlaefli

A flat four-dimensional check

In four-dimensional geometry, a simplex is the generalization of a triangle to four dimensions: the simplest shape with five vertices, ten edges, and ten triangular faces. A classical identity by Ludwig Schläfli relates how the volume of such a shape changes when its edges are stretched to how its dihedral angles change. The Recognition Science framework's machine-checked library of formal theorems contains a declaration, freudenthal4SimplexFlatSchlaefliPresent_true, which records a verified result about this identity for one special case: a flat simplex, one that lies entirely in a lower-dimensional plane.

The declaration establishes that for this flat four-dimensional simplex, the Schläfli identity holds in a specific, restricted sense. It proves that if you move the simplex's edges along any straight-line path starting from the flat shape, the sum of the hinge areas times the directional derivatives of the dihedral angles equals zero. This is a check of the identity's structure at a single point, not a proof for all shapes. The library also confirms that the ten triangular hinge areas are all strictly positive, so the result is not vacuous, and that the seed hinge's dihedral angle has a well-defined derivative along every such path.

What the declaration does not claim is broader. It does not prove the full pathwise Schläfli identity for all non-flat four-dimensional simplices; that remains an open target in the framework. It also does not claim to have derived the Einstein-Hilbert action of general relativity in four dimensions, nor to have shown any physical consequence about gravity. The declaration is a formal, combinatorial checkpoint: a verification that a particular geometric identity holds at a flat seed configuration, not a statement about the physical world.

theorem freudenthal4SimplexFlatSchlaefliPresent_true :
    freudenthal4SimplexFlatSchlaefliPresent = true :=
  rfl

/-- **THEOREM (Gate A2-style at flat).** For every squared-edge velocity
through the flat seed, the area-weighted directional angle sum vanishes:

`Σ_h A_h · (Σ_e v_e · ∂θ_h/∂ℓ²_e) = 0`.

This is the flat directional contraction of `freudenthal4SimplexFlatSchlaefli`
and is the 4D analog of the flat evaluation of the 3D pathwise Schläfli kill
along every edge direction. -/
theorem freudenthal4SimplexFlatDirectionalSchlaefli (v : Fin 10 → ℝ) :
    (∑ h : Fin 10, hingeAreaFlat h * flatDirectionalAngleDeriv v h) = 0 := by
  unfold flatDirectionalAngleDeriv flatAngleJacobian
  calc
    (∑ h : Fin 10, hingeAreaFlat h *
        (∑ e : Fin 10, v e * (flatSchlaefliSummand h e / hingeAreaFlat h)))
        = ∑ h : Fin 10, ∑ e : Fin 10,
            v e * flatSchlaefliSummand h e := by
          refine Finset.sum_congr rfl fun h _ => ?_
          rw [Finset.mul_sum]
          refine Finset.sum_congr rfl fun e _ => ?_
          calc
            hingeAreaFlat h * (v e * (flatSchlaefliSummand h e / hingeAreaFlat h))
                = v e * (hingeAreaFlat h * (flatSchlaefliSummand h e / hingeAreaFlat h)) := by
                  ring
            _ = v e * flatSchlaefliSummand h e := by rw [mul_div_cancel_area]
    _ = ∑ e : Fin 10, v e * (∑ h : Fin 10, flatSchlaefliSummand h e) := by
          rw [Finset.sum_comm]
          refine Finset.sum_congr rfl fun e _ => ?_
          rw [Finset.mul_sum]
    _ = ∑ e : Fin 10, v e * 0 := by
          refine Finset.sum_congr rfl fun e _ => ?_
          rw [freudenthal4SimplexFlatSchlaefli e]
    _ = 0 := by simp

What this page does not claim

The full pathwise Schläfli identity holds for all non-flat four-dimensional simplices. The Einstein-Hilbert action of general relativity has been derived in four dimensions. The declaration has any direct physical consequence for gravity in the observable universe.

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/Gravity/Analysis/Regge4DSchlaefliPathwise.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: