Encyclopedia Gravity Gravity Seven Gaps Three Pent Causal Consistency Physical Point Regular

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Three Pent Causal Consistency Physical Point Regular

At one special choice of scale and shape, a small complex of triangles becomes a perfectly regular four-dimensional building block.

Verify this page

The regular point

The declaration physical_point_regular is a check that a particular geometric construction has a well-behaved, non-degenerate example. The construction is a minimal complex of three five-vertex simplices, called pents, glued around a shared interior hinge. Each pent is a four-dimensional analogue of a triangle, and the complex is a candidate building block for a discrete model of spacetime.

The declaration proves that when the two free parameters, a scale factor and a shape parameter, are both set to 1, every one of the three pents becomes the regular unit 4-simplex. A regular 4-simplex is the four-dimensional analogue of an equilateral triangle: all ten of its edges have the same length. The proof also computes a specific geometric invariant, the Cayley-Menger determinant, which for this regular case equals 5. A positive value of this invariant is the criterion that the pent can be embedded as a genuine, non-degenerate simplex in four-dimensional Euclidean space.

This result matters because it shows the complex is not an empty formal object. It provides a concrete, physical point in the parameter space where the construction is fully realized and regular. This anchors the entire family of assignments, which for a broader range of parameters presents each pent as a standard causal simplex from the framework's library of four-dimensional building blocks.

What the declaration does not claim is just as important. It does not establish that the complex is the unique or even the preferred building block for spacetime. It does not address the values of the dihedral angles around the hinge, which would be needed to compute the total curvature or action. It also does not claim that the classical equivalence between a positive Cayley-Menger determinant and embeddability in four-dimensional space has been formally proved within the framework's library. The declaration is a single, sharp existence check, not a theory of gravity.

THEOREM physical_point_regular · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
physical_point_regular · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:285 
/-- THEOREM (non-vacuity anchor): at the physical point `a = 1`,
`alpha = 1`, every pent of the complex Wick-rotates to the regular unit
4-simplex, `cm4 = 5`. -/
theorem physical_point_regular :
    wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)
        = (fun _ => (1 : ℝ))
      ∧ cm4 (wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)) = 5
      ∧ wick CausalPentType.threeTwo (inducedSqEdges pentBVert 1 1)
          = (fun _ => (1 : ℝ))
      ∧ wick CausalPentType.threeTwo (inducedSqEdges pentCVert 1 1)
          = (fun _ => (1 : ℝ)) := by
  have hA : wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)
      = (fun _ => (1 : ℝ)) := by
    rw [induced_pentA_eq, wick_lorentzian,
      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
  have hB : wick CausalPentType.threeTwo (inducedSqEdges pentBVert 1 1)
      = (fun _ => (1 : ℝ)) := by
    rw [induced_pentB_eq, wick_lorentzian,
      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
  have hC : wick CausalPentType.threeTwo (inducedSqEdges pentCVert 1 1)
      = (fun _ => (1 : ℝ)) := by
    rw [induced_pentC_eq, wick_lorentzian,
      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
  exact ⟨hA, by rw [hA]; exact cm4_regular_unit, hB, hC⟩
THEOREM physical_point_regular · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
physical_point_regular · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:285 
/-- THEOREM (non-vacuity anchor): at the physical point `a = 1`,
`alpha = 1`, every pent of the complex Wick-rotates to the regular unit
4-simplex, `cm4 = 5`. -/
theorem physical_point_regular :
    wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)
        = (fun _ => (1 : ℝ))
      ∧ cm4 (wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)) = 5
      ∧ wick CausalPentType.threeTwo (inducedSqEdges pentBVert 1 1)
          = (fun _ => (1 : ℝ))
      ∧ wick CausalPentType.threeTwo (inducedSqEdges pentCVert 1 1)
          = (fun _ => (1 : ℝ)) := by
  have hA : wick CausalPentType.threeTwo (inducedSqEdges pentAVert 1 1)
      = (fun _ => (1 : ℝ)) := by
    rw [induced_pentA_eq, wick_lorentzian,
      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
  have hB : wick CausalPentType.threeTwo (inducedSqEdges pentBVert 1 1)
      = (fun _ => (1 : ℝ)) := by
    rw [induced_pentB_eq, wick_lorentzian,
      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
  have hC : wick CausalPentType.threeTwo (inducedSqEdges pentCVert 1 1)
      = (fun _ => (1 : ℝ)) := by
    rw [induced_pentC_eq, wick_lorentzian,
      euclideanSqEdges_alpha_one CausalPentType.threeTwo]
  exact ⟨hA, by rw [hA]; exact cm4_regular_unit, hB, hC⟩
THEOREM threePent_causal_assignment · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean
threePent_causal_assignment · IndisputableMonolith/Gravity/SevenGaps/ThreePentCausalConsistency.lean:310 
/-- **GAP6-A HEADLINE (THEOREM): an explicit admissible causal
edge-length assignment on the minimal three-pent interior-hinge complex
EXISTS.**  On the exact 4d CDT range (`0 < a`, `alpha > 7/12`), the ONE
global assignment `causalSqLength` presents all three pents
simultaneously as standard Lorentzian (3,2) simplices (consistency
core), members of the Lorentzian causal class, with strict Lorentzian
CM negativity and Euclidean CM admissibility after Wick, per pent.
EXISTENCE-ONLY SCOPE: this realizes the symmetric standard CDT slab
assignment; it does not classify asymmetric assignments or hinge-cycle
monodromy.  The certified-non-existence branch of the W3-2 lane does
not fire; gap6-b may proceed against this concrete object. -/
theorem threePent_causal_assignment (a alpha : ℝ) (ha : 0 < a)
    (halpha : 7 / 12 < alpha) :
    (inducedSqEdges pentAVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha
        ∧ inducedSqEdges pentBVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha
        ∧ inducedSqEdges pentCVert a alpha
          = lorentzianSqEdges CausalPentType.threeTwo a alpha)
      ∧ (inducedSqEdges pentAVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo
        ∧ inducedSqEdges pentBVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo
        ∧ inducedSqEdges pentCVert a alpha
            ∈ LorentzianClass CausalPentType.threeTwo)
      ∧ (cm4 (inducedSqEdges pentAVert a alpha) < 0
        ∧ cm4 (inducedSqEdges pentBVert a alpha) < 0
        ∧ cm4 (inducedSqEdges pentCVert a alpha) < 0)
      ∧ (0 < cm4 (wick CausalPentType.threeTwo
            (inducedSqEdges pentAVert a alpha))
        ∧ 0 < cm4 (wick CausalPentType.threeTwo
            (inducedSqEdges pentBVert a alpha))
        ∧ 0 < cm4 (wick CausalPentType.threeTwo
            (inducedSqEdges pentCVert a alpha))) := by
  have halpha0 : 0 < alpha := lt_trans (by norm_num) halpha
  exact ⟨⟨induced_pentA_eq a alpha, induced_pentB_eq a alpha,
      induced_pentC_eq a alpha⟩,
    threePent_lorentzian_class a alpha ha halpha0,
    threePent_lorentzian_cm4_neg a alpha ha halpha0.le,
    threePent_euclidean_admissible a alpha ha halpha⟩

What this page does not claim

The declaration does not claim the complex is unique or physically preferred. It does not compute the dihedral angles around the hinge. It does not formally prove the classical equivalence between a positive Cayley-Menger determinant and embeddability in four-dimensional space.

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/SevenGaps/ThreePentCausalConsistency.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