Encyclopedia Gravity Gravity Analysis Regge4 Dschlaefli Pathwise Pathwise Flat Remainder Directional

ARTICLE 3 claims 2 theorems 1 open

Gravity Analysis Regge4 Dschlaefli Pathwise Pathwise Flat Remainder Directional

A machine-checked theorem shows that a certain weighted sum of angle changes vanishes at a special flat starting point in a four-dimensional simplex.

Verify this page

The flat directional identity

The declaration pathwiseFlatRemainder_directional_zero is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns the Freudenthal 4-simplex, the simplest five-vertex geometric object in four-dimensional space. The theorem states that at a particular flat seed configuration, a weighted sum of dihedral angle derivatives along any linear path through that configuration equals zero.

To see what this means concretely, consider a four-dimensional simplex as a collection of ten edges and ten triangular hinges. The Schläfli identity is a classical relation: for a deforming simplex, the sum over hinges of the hinge area times the rate of change of the dihedral angle vanishes. This identity is central to Regge calculus, a discrete approach to general relativity. The framework's theorem establishes that this identity holds at the flat seed, for every possible affine velocity direction through that seed. The proof uses a table of flat summands and a Jacobian that converts edge-length changes into angle changes.

The theorem is one milestone in a larger program. The framework's library also proves that the flat Schläfli summand table has vanishing column sums, that the seed-hinge row matches a known angle kernel, and that a non-vacuous witness with strictly positive areas exists. These results together confirm that the flat directional identity is not trivially empty: there is a genuine geometric configuration where the weighted sum vanishes.

What the theorem does not claim is just as important. It does not establish the full pathwise Schläfli identity away from the flat seed, on the general nondegenerate 4-simplex. The library explicitly marks that as an open target. It also does not provide a remapped derivative statement for every hinge row, and it does not prove the convergence of the framework's discrete action to the Einstein-Hilbert action in four dimensions. The theorem is a precise, local statement about one flat configuration, not a global derivation of gravity.

THEOREM freudenthal4SimplexFlatDirectionalSchlaefli · IndisputableMonolith/Gravity/Analysis/Regge4DSchlaefliPathwise.lean
freudenthal4SimplexFlatDirectionalSchlaefli · IndisputableMonolith/Gravity/Analysis/Regge4DSchlaefliPathwise.lean:414 
/-- **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
THEOREM flatSchlaefliSummand_seed_eq_area_angleKernel · freudenthal4SimplexFlatSchlaefliPresent_true · IndisputableMonolith/Gravity/Analysis/Regge4DSchlaefliPathwise.lean
flatSchlaefliSummand_seed_eq_area_angleKernel · IndisputableMonolith/Gravity/Analysis/Regge4DSchlaefliPathwise.lean:241 
theorem flatSchlaefliSummand_seed_eq_area_angleKernel (e : Fin 10) :
    flatSchlaefliSummand 0 e = hingeAreaFlat 0 * angleKernel e := by
  rw [hingeAreaFlat_0]
  refine seed_summand_mul_angle e ?_
  fin_cases e
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]; norm_num
  · -- e = ⟨8,_⟩: OfNat `8` ≠ raw Fin constructor, so unfold
    simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]
    have hs : Real.sqrt 2 * Real.sqrt 2 = (2 : ℝ) :=
      Real.mul_self_sqrt (by norm_num)
    rw [neg_mul, mul_div_assoc', hs]
    norm_num
  · simp only [flatSchlaefliSummand, flatSchlaefliSummandQ, angleKernel,
      cosDihedralKernel]
    have hs : Real.sqrt 2 * Real.sqrt 2 = (2 : ℝ) :=
      Real.mul_self_sqrt (by norm_num)
    -- -√2 * (-√2 / 4) = (√2 * √2) / 4
    rw [show -Real.sqrt 2 * (-Real.sqrt 2 / 4) = Real.sqrt 2 * Real.sqrt 2 / 4 from by
      ring]
    rw [hs]
    norm_num
freudenthal4SimplexFlatSchlaefliPresent_true · IndisputableMonolith/Gravity/Analysis/Regge4DSchlaefliPathwise.lean:312 
theorem freudenthal4SimplexFlatSchlaefliPresent_true :
    freudenthal4SimplexFlatSchlaefliPresent = true :=
  rfl

What this page does not claim

The theorem does not prove the Schläfli identity away from the flat seed. The theorem does not derive the Einstein-Hilbert action from the discrete action. The theorem does not provide a remapped derivative statement for every hinge row.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND