Encyclopedia Gravity Gravity Seven Gaps Wick Four One All Hinges Boundary Four One Spacelike Pair
ARTICLE 4 claims 4 theorems
Gravity Seven Gaps Wick Four One All Hinges Boundary Four One Spacelike Pair
In a quantum gravity calculation, a machine-checked proof shows that a specific class of geometric building blocks, the spacelike hinges of a causal 4-simplex, have a well-defined, continuous boundary value in the complex plane.
The spacelike hinge boundary
A 4-simplex is the four-dimensional analogue of a triangle: it has five vertices, ten edges, and ten triangular faces, which the framework calls hinges. In the causal version used here, one vertex is the apex and four edges touch it, giving the simplex a built-in time direction. The declaration boundary_fourOne_spacelike_pair concerns the four hinges that do not touch the apex. Each such hinge has a pair of opposite vertices, one of which is the apex itself.
The proof establishes a boundary value for these spacelike hinges. As a parameter moves along a closed interval from the Lorentzian to the Euclidean regime, the cosine of the dihedral angle at each spacelike hinge follows a continuous path. At the Euclidean endpoint, this path reaches the value -(1/4), the same value for a regular 4-simplex. At the Lorentzian endpoint, the value is purely imaginary: (sqrt 2 / 8) * I. This imaginary number is the Lorentzian dihedral datum at a spacelike hinge, a quantity that appears in the Regge action for gravity.
In Recognition Science, the framework models this as a Wick rotation, a standard technique that turns a problem in Lorentzian signature into one in Euclidean signature. The declaration proves that for every one of the four spacelike hinges, the split-form cosine path is continuous on the closed interval and ends at the Euclidean value. It also proves the closed-form area-squared for these hinges is a constant 3/16, including at the endpoints, which keeps the square-root branch away from its cut.
The declaration does not claim the full action-level continuation. The continued Regge action itself, built from deficit angles over the whole simplicial complex, remains an open target. The proof covers one traced hinge at a time, and the extension to all ten hinges is a separate result. The framework also does not claim any physical interpretation for the imaginary Lorentzian dihedral angle; it is a mathematical datum within the model.
THEOREM wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- THEOREM (B1 headline, boundary continuation): every split-form cosine
path of the fourOne type is continuous on the CLOSED interval `[0, 1]` and
ends at the Euclidean regular-4-simplex value `-(1/4)` (`+C_pq` numerator
convention of the landed module; textbook `-C` interior cosine `+1/4`). -/
theorem wick_boundary_continuation_fourOne_allHinges :
∀ p q : Fin 5, p ≠ q →
ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by
intro p q hpq
fin_cases p <;> fin_cases q
· exact absurd rfl hpq
· exact ⟨boundary_pair01.1, boundary_pair01.2.2⟩
· exact ⟨boundary_pair02.1, boundary_pair02.2.2⟩
· exact ⟨boundary_pair03.1, boundary_pair03.2.2⟩
· exact ⟨boundary_pair04.1, boundary_pair04.2.2⟩
· exact boundary_symm ⟨boundary_pair01.1, boundary_pair01.2.2⟩
· exact absurd rfl hpq
· exact ⟨boundary_pair12.1, boundary_pair12.2.2⟩
· exact ⟨boundary_pair13.1, boundary_pair13.2.2⟩
· exact ⟨boundary_pair14.1, boundary_pair14.2.2⟩
· exact boundary_symm ⟨boundary_pair02.1, boundary_pair02.2.2⟩
· exact boundary_symm ⟨boundary_pair12.1, boundary_pair12.2.2⟩
· exact absurd rfl hpq
· exact ⟨boundary_pair23.1, boundary_pair23.2.2⟩
· exact ⟨boundary_pair24.1, boundary_pair24.2.2⟩
· exact boundary_symm ⟨boundary_pair03.1, boundary_pair03.2.2⟩
· exact boundary_symm ⟨boundary_pair13.1, boundary_pair13.2.2⟩
· exact boundary_symm ⟨boundary_pair23.1, boundary_pair23.2.2⟩
· exact absurd rfl hpq
· exact ⟨boundary_pair34.1, boundary_pair34.2.2⟩
· exact boundary_symm ⟨boundary_pair04.1, boundary_pair04.2.2⟩
· exact boundary_symm ⟨boundary_pair14.1, boundary_pair14.2.2⟩
· exact boundary_symm ⟨boundary_pair24.1, boundary_pair24.2.2⟩
· exact boundary_symm ⟨boundary_pair34.1, boundary_pair34.2.2⟩
· exact absurd rfl hpq
THEOREM wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- THEOREM (B1 headline, boundary continuation): every split-form cosine
path of the fourOne type is continuous on the CLOSED interval `[0, 1]` and
ends at the Euclidean regular-4-simplex value `-(1/4)` (`+C_pq` numerator
convention of the landed module; textbook `-C` interior cosine `+1/4`). -/
theorem wick_boundary_continuation_fourOne_allHinges :
∀ p q : Fin 5, p ≠ q →
ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by
intro p q hpq
fin_cases p <;> fin_cases q
· exact absurd rfl hpq
· exact ⟨boundary_pair01.1, boundary_pair01.2.2⟩
· exact ⟨boundary_pair02.1, boundary_pair02.2.2⟩
· exact ⟨boundary_pair03.1, boundary_pair03.2.2⟩
· exact ⟨boundary_pair04.1, boundary_pair04.2.2⟩
· exact boundary_symm ⟨boundary_pair01.1, boundary_pair01.2.2⟩
· exact absurd rfl hpq
· exact ⟨boundary_pair12.1, boundary_pair12.2.2⟩
· exact ⟨boundary_pair13.1, boundary_pair13.2.2⟩
· exact ⟨boundary_pair14.1, boundary_pair14.2.2⟩
· exact boundary_symm ⟨boundary_pair02.1, boundary_pair02.2.2⟩
· exact boundary_symm ⟨boundary_pair12.1, boundary_pair12.2.2⟩
· exact absurd rfl hpq
· exact ⟨boundary_pair23.1, boundary_pair23.2.2⟩
· exact ⟨boundary_pair24.1, boundary_pair24.2.2⟩
· exact boundary_symm ⟨boundary_pair03.1, boundary_pair03.2.2⟩
· exact boundary_symm ⟨boundary_pair13.1, boundary_pair13.2.2⟩
· exact boundary_symm ⟨boundary_pair23.1, boundary_pair23.2.2⟩
· exact absurd rfl hpq
· exact ⟨boundary_pair34.1, boundary_pair34.2.2⟩
· exact boundary_symm ⟨boundary_pair04.1, boundary_pair04.2.2⟩
· exact boundary_symm ⟨boundary_pair14.1, boundary_pair14.2.2⟩
· exact boundary_symm ⟨boundary_pair24.1, boundary_pair24.2.2⟩
· exact boundary_symm ⟨boundary_pair34.1, boundary_pair34.2.2⟩
· exact absurd rfl hpq
THEOREM fourOneCosPath · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- The split-form cosine path of the opposite pair `(p, q)` along the
physical fourOne arc (MODEL; generalizes the landed `hingeCosPath`, which
is the case `p = 2`, `q = 3`). -/
noncomputable def fourOneCosPath (p q : Fin 5) (t : ℝ) : ℂ :=
dihedralCosSplitC (continuationEdgesC CausalPentType.fourOne 1 1 t) p q
THEOREM fourOne_areaSq_interior_off_cut · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- THEOREM: the constant spacelike-class area-squared `3/16` avoids the
sqrt cut EVERYWHERE (both endpoints included), and the timelike-class
area-squared `z/4 - 1/16` avoids it on the full open interior (its
Lorentzian endpoint value `-5/16` sits ON the cut boundary, the ALLOWED
endpoint contact documented in the landed module). -/
theorem fourOne_areaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) :
((3 / 16 : ℂ) ∈ Complex.slitPlane)
∧ (zArc t / 4 - 1 / 16 ∈ Complex.slitPlane) := by
constructor
· exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num))
· apply Complex.mem_slitPlane_iff.mpr
right
have hy : 0 < (zArc t).im := zArc_im_pos ht
have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by
simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im]
ring
rw [him]
exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'
What this page does not claim
The declaration does not claim the action-level continuation or the continued Regge action itself. It does not claim a physical interpretation for the imaginary Lorentzian dihedral angle. It does not claim the boundary value for the six timelike hinges, which have a different value of -(3/8).
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/WickFourOneAllHinges.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:
- What is the physical interpretation of the imaginary Lorentzian dihedral angle at a spacelike hinge?
- How does the boundary continuation for a single hinge extend to the full action-level continuation over the simplicial complex?
- What is the relationship between the spacelike hinge boundary value and the timelike hinge boundary value of -(3/8)?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- THEOREM (B1 headline, boundary continuation): every split-form cosine path of the fourOne type is continuous on the CLOSED interval `[0, 1]` and ends at the Euclidean regular-4-simplex value `-(1/4)` (`+C_pq` numerator convention of the landed module; textbook `-C` interior cosine `+1/4`). -/ theorem wick_boundary_continuation_fourOne_allHinges : ∀ p q : Fin 5, p ≠ q → ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1) ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by intro p q hpq fin_cases p <;> fin_cases q · exact absurd rfl hpq · exact ⟨boundary_pair01.1, boundary_pair01.2.2⟩ · exact ⟨boundary_pair02.1, boundary_pair02.2.2⟩ · exact ⟨boundary_pair03.1, boundary_pair03.2.2⟩ · exact ⟨boundary_pair04.1, boundary_pair04.2.2⟩ · exact boundary_symm ⟨boundary_pair01.1, boundary_pair01.2.2⟩ · exact absurd rfl hpq · exact ⟨boundary_pair12.1, boundary_pair12.2.2⟩ · exact ⟨boundary_pair13.1, boundary_pair13.2.2⟩ · exact ⟨boundary_pair14.1, boundary_pair14.2.2⟩ · exact boundary_symm ⟨boundary_pair02.1, boundary_pair02.2.2⟩ · exact boundary_symm ⟨boundary_pair12.1, boundary_pair12.2.2⟩ · exact absurd rfl hpq · exact ⟨boundary_pair23.1, boundary_pair23.2.2⟩ · exact ⟨boundary_pair24.1, boundary_pair24.2.2⟩ · exact boundary_symm ⟨boundary_pair03.1, boundary_pair03.2.2⟩ · exact boundary_symm ⟨boundary_pair13.1, boundary_pair13.2.2⟩ · exact boundary_symm ⟨boundary_pair23.1, boundary_pair23.2.2⟩ · exact absurd rfl hpq · exact ⟨boundary_pair34.1, boundary_pair34.2.2⟩ · exact boundary_symm ⟨boundary_pair04.1, boundary_pair04.2.2⟩ · exact boundary_symm ⟨boundary_pair14.1, boundary_pair14.2.2⟩ · exact boundary_symm ⟨boundary_pair24.1, boundary_pair24.2.2⟩ · exact boundary_symm ⟨boundary_pair34.1, boundary_pair34.2.2⟩ · exact absurd rfl hpqThe proof establishes a boundary value for these spacelike hinges. wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.leanTHEOREM wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- THEOREM (B1 headline, boundary continuation): every split-form cosine path of the fourOne type is continuous on the CLOSED interval `[0, 1]` and ends at the Euclidean regular-4-simplex value `-(1/4)` (`+C_pq` numerator convention of the landed module; textbook `-C` interior cosine `+1/4`). -/ theorem wick_boundary_continuation_fourOne_allHinges : ∀ p q : Fin 5, p ≠ q → ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1) ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ) := by intro p q hpq fin_cases p <;> fin_cases q · exact absurd rfl hpq · exact ⟨boundary_pair01.1, boundary_pair01.2.2⟩ · exact ⟨boundary_pair02.1, boundary_pair02.2.2⟩ · exact ⟨boundary_pair03.1, boundary_pair03.2.2⟩ · exact ⟨boundary_pair04.1, boundary_pair04.2.2⟩ · exact boundary_symm ⟨boundary_pair01.1, boundary_pair01.2.2⟩ · exact absurd rfl hpq · exact ⟨boundary_pair12.1, boundary_pair12.2.2⟩ · exact ⟨boundary_pair13.1, boundary_pair13.2.2⟩ · exact ⟨boundary_pair14.1, boundary_pair14.2.2⟩ · exact boundary_symm ⟨boundary_pair02.1, boundary_pair02.2.2⟩ · exact boundary_symm ⟨boundary_pair12.1, boundary_pair12.2.2⟩ · exact absurd rfl hpq · exact ⟨boundary_pair23.1, boundary_pair23.2.2⟩ · exact ⟨boundary_pair24.1, boundary_pair24.2.2⟩ · exact boundary_symm ⟨boundary_pair03.1, boundary_pair03.2.2⟩ · exact boundary_symm ⟨boundary_pair13.1, boundary_pair13.2.2⟩ · exact boundary_symm ⟨boundary_pair23.1, boundary_pair23.2.2⟩ · exact absurd rfl hpq · exact ⟨boundary_pair34.1, boundary_pair34.2.2⟩ · exact boundary_symm ⟨boundary_pair04.1, boundary_pair04.2.2⟩ · exact boundary_symm ⟨boundary_pair14.1, boundary_pair14.2.2⟩ · exact boundary_symm ⟨boundary_pair24.1, boundary_pair24.2.2⟩ · exact boundary_symm ⟨boundary_pair34.1, boundary_pair34.2.2⟩ · exact absurd rfl hpqAt the Euclidean endpoint, this path reaches the value -(1/4), the same value for a regular 4-simplex. wick_boundary_continuation_fourOne_allHinges · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.leanTHEOREM fourOneCosPath · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- The split-form cosine path of the opposite pair `(p, q)` along the physical fourOne arc (MODEL; generalizes the landed `hingeCosPath`, which is the case `p = 2`, `q = 3`). -/ noncomputable def fourOneCosPath (p q : Fin 5) (t : ℝ) : ℂ := dihedralCosSplitC (continuationEdgesC CausalPentType.fourOne 1 1 t) p qAt the Lorentzian endpoint, the value is purely imaginary: (sqrt 2 / 8) * I. fourOneCosPath · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.leanTHEOREM fourOne_areaSq_interior_off_cut · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean
/-- THEOREM: the constant spacelike-class area-squared `3/16` avoids the sqrt cut EVERYWHERE (both endpoints included), and the timelike-class area-squared `z/4 - 1/16` avoids it on the full open interior (its Lorentzian endpoint value `-5/16` sits ON the cut boundary, the ALLOWED endpoint contact documented in the landed module). -/ theorem fourOne_areaSq_interior_off_cut {t : ℝ} (ht : t ∈ Set.Ioo (0 : ℝ) 1) : ((3 / 16 : ℂ) ∈ Complex.slitPlane) ∧ (zArc t / 4 - 1 / 16 ∈ Complex.slitPlane) := by constructor · exact Complex.mem_slitPlane_iff.mpr (Or.inl (by norm_num)) · apply Complex.mem_slitPlane_iff.mpr right have hy : 0 < (zArc t).im := zArc_im_pos ht have him : (zArc t / 4 - 1 / 16).im = (zArc t).im / 4 := by simp only [Complex.sub_im, Complex.div_ofNat_im, Complex.one_im] ring rw [him] exact (div_pos hy (by norm_num : (0 : ℝ) < 4)).ne'It also proves the closed-form area-squared for these hinges is a constant 3/16, including at the endpoints. fourOne_areaSq_interior_off_cut · IndisputableMonolith/Gravity/SevenGaps/WickFourOneAllHinges.lean