Gravity Analysis Regge4 Dschlaefli Pathwise

A four-dimensional test of a geometric law

The Schläfli identity is a classical geometric relation. For a deforming polyhedron in any dimension, it states that the change in volume is proportional to the sum of each hinge's dihedral angle times the change in its area. In four dimensions, the hinges are triangles, and the identity becomes a sum over ten triangle hinges. The module gravity analysis here tests this identity on a specific four-dimensional simplex, the Freudenthal 4-simplex, using a discrete Regge calculus approach where spacetime is built from flat simplices.

The classical identity holds for smooth deformations. The framework's library, a machine-checked collection of formal theorems, proves the identity at a special "flat" configuration of the simplex, where all squared edge lengths are set to a specific seed value. The proof establishes that the column sums of the Schläfli summand table vanish, meaning the identity holds at this point. It also proves a stronger directional version: for any affine velocity through this flat seed, the sum of hinge areas times the derivative of the dihedral angles is zero. This is a non-vacuous result, with strictly positive hinge areas.

The module also defines a target for the full pathwise identity away from the flat seed, but this remains open. The current proof does not yet cover the entire space of non-degenerate simplices, nor does it establish the derivative for every hinge row. The library explicitly marks this as an open target, not a failure. The module does not flip the gap_action_recovery flag, meaning it does not yet bridge to a broader action recovery principle.

What this establishes in plain language is a rigorous check at a single point in a four-dimensional geometric space. It confirms the Schläfli identity holds at the flat seed and its immediate directional neighborhood, providing a concrete, machine-verified foundation for further work. The next step is to extend this proof from the flat seed to the full space of non-degenerate simplices, which would complete the pathwise identity and potentially link discrete geometry to the Einstein-Hilbert action in four dimensions.

theorem freudenthal4SimplexFlatSchlaefliPresent_true :
    freudenthal4SimplexFlatSchlaefliPresent = true :=
  rfl

def flatHingeData (h : Fin 10) : HingeDataN where
  measure := hingeAreaFlat h
  measure_nonneg := le_of_lt (hingeAreaFlat_pos h)

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

/-- Flat arccos chain factor `d(arccos)/d(cos) = -1/sin = -√2`. -/
theorem arccos_chain_factor_flat :
    -(1 / Real.sqrt (1 - cosDihedral seedFlatSqEdges ^ 2)) = -(Real.sqrt 2) := by
  rw [sinDihedral_flat]
  field_simp

What this page does not claim

The module does not prove the full pathwise Schläfli identity for all non-degenerate 4-simplices. The module does not establish a connection to the Einstein-Hilbert action or to physical gravity. The module does not flip the gap_action_recovery flag.

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: