Gravity Analysis Regge4 Dflat Second Variation Freudenthal4 Simplex Pathwise Sch

The missing pathwise formula

In the study of gravity, one common approach is to discretize spacetime into a mesh of flat, four-dimensional simplexes, the higher-dimensional analogue of triangles. The Regge action, named after Tullio Regge's 1961 proposal, is a way to write down gravity's equations on such a mesh using only the edge lengths of the simplexes. A central question is how this discrete action behaves when the mesh is slightly deformed, and whether it converges to the smooth Einstein-Hilbert action of general relativity in the limit of a fine mesh.

The declaration Freudenthal4SimplexPathwiseSchlaefli_absent is a formal statement in the framework's machine-checked library of formal theorems. It records, as a proved theorem, that a particular formula, the pathwise Schläfli identity for a Freudenthal 4-simplex, is not present in the library. The Schläfli identity is a classical geometric relation describing how the volume of a simplex changes when its dihedral angles change. The "pathwise" qualifier means the formula would hold along a continuous path of simplex shapes, not just at the flat, regular starting point.

What the declaration establishes is a precise status report. The library has proved the flat, non-pathwise version of the identity, where all edges have equal length, and the flat directional version, which holds for infinitesimal motions away from that flat shape. It has also proved that the candidate expression for the second variation of the Regge action has a specific value, -1/16, on a certain test direction, which differs from the Einstein-Hilbert value of -1/4. But the full pathwise formula, which would cover arbitrary deformations, is absent. The theorem simply states this absence as a fact, with a boolean flag set to false.

In Recognition Science, this absence is not a failure but a precisely mapped open target. The framework's own status structure lists schlaefliElevationOpen as true, meaning the elevation of the nonlinear action to the candidate form remains an open problem. The declaration does not claim that the pathwise formula is false, nor that it cannot be proved. It does not claim that the discrete Regge action fails to converge to general relativity. It only asserts that this specific piece of the derivation has not yet been completed in the library.

The practical consequence is that the framework's program to derive gravity from its foundational principles has a known, named gap. The next step is clear: find and verify the missing pathwise Schläfli formula. Until then, the candidate second variation, while identified and partially tested, cannot be fully elevated to a theorem about the true nonlinear action. This is how the framework operates: every claim, even a negative one about what is not yet known, is recorded with the same rigor as a positive result.

/-- **Named missing identity** (not a Lean theorem in this library).

Pathwise Schläfli on every Freudenthal / Kuhn 4-simplex, squared-edge
coordinates:

```
  ∀ σ 4-simplex, ∀ e ∈ edges(σ), at every nondegenerate path point,
    Σ_{h ⊂ σ} A_h(σ) · (∂θ_{σ,h} / ∂ℓ²_e) = 0
```

(`nH = nE = 10` instance of `SchlaefliN.SchlaefliIdentityN` with
measures = hinge areas and `dTheta_dL` = squared-edge partials of the
4-simplex dihedrals).

3D analog (THEOREM):
`Geometry.SchlaefliTetrahedronProof.tetraSchlaefliSixEdgeClosedForm`.

Flat-seed algebraic closed form and flat directional kill are THEOREM in
`Regge4DSchlaefliPathwise` (non-vacuous positive-area witness; seed-angle
`HasDerivAt`).  Full off-flat pathwise closed form along a general
nondegenerate path remains absent
(`freudenthal4SimplexPathwiseSchlaefliPresent` stays `false`).  Do not
inhabit a vacuous `Prop` shell. -/
theorem Freudenthal4SimplexPathwiseSchlaefli_absent :
    freudenthal4SimplexPathwiseSchlaefliPresent = false :=
  freudenthal4SimplexPathwiseSchlaefliPresent_false

theorem flat_freudenthal_schlaefli_present :
    freudenthal4SimplexFlatSchlaefliPresent = true :=
  freudenthal4SimplexFlatSchlaefliPresent_true

theorem flat_freudenthal_directional_schlaefli_present :
    freudenthal4SimplexFlatDirectionalSchlaefliPresent = true :=
  freudenthal4SimplexFlatDirectionalSchlaefliPresent_true

/-- Continuum-facing coefficient after Frobenius pin and `/|symbolDir|²`:
`-1/16`. -/
theorem candidate_continuumFace_normalizedTT_symbolDir :
    distinctHingeMomentForm ((Real.sqrt 2)⁻¹ • axisTTPlus) symbolDir /
        (∑ i : Fin 4, symbolDir i * symbolDir i) =
      (-1 / 16 : ℝ) :=
  continuumFace_normalizedPlus_symbolDir

/-- Frozen EH target. -/
theorem eh_target_neg_quarter :
    einsteinHilbertTTCoefficient4D = -(1 / 4 : ℝ) :=
  einsteinHilbertTTCoefficient4D_eq

theorem regge4DFlatSecondVariationStatus_flags :
    regge4DFlatSecondVariationStatus.candidateIdentified = true ∧
      regge4DFlatSecondVariationStatus.candidateBlochFaceEvaluated = true ∧
        regge4DFlatSecondVariationStatus.freudenthal4FlatSchlaefliPresent =
          true ∧
          regge4DFlatSecondVariationStatus.freudenthal4FlatDirectionalPresent =
            true ∧
            regge4DFlatSecondVariationStatus.freudenthal4PathwiseSchlaefliPresent =
              false ∧
              regge4DFlatSecondVariationStatus.schlafliElevationOpen = true ∧
                regge4DFlatSecondVariationStatus.gapActionRecovery = false := by
  decide

What this page does not claim

The pathwise Schläfli formula is false or impossible to prove. The discrete Regge action fails to converge to general relativity. The declaration itself proves any property of the true nonlinear action's second variation.

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/Regge4DFlatSecondVariation.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: