Encyclopedia Gravity Gravity Seven Gaps Wick Hinge Data Complete Wick Hinge Data Continuation Complet
ARTICLE 5 claims 5 theorems
Gravity Seven Gaps Wick Hinge Data Complete Wick Hinge Data Continuation Complet
A machine-checked theorem certifies that the geometry of a single quantum simplex continues smoothly from Lorentzian to Euclidean signature, while leaving the full action-level continuation open.
The hinge-data continuation
In the Recognition Science framework's study of quantum gravity, a causal 4-simplex is the discrete building block of spacetime: a five-vertex tetrahedron-like object whose edges carry timelike or spacelike character. The theorem wick_hinge_data_continuation_complete certifies, for every one of the twenty triangular hinges of both causal simplex types, that the geometric data continue smoothly when the signature of spacetime is rotated from Lorentzian to Euclidean. This is the mathematical operation known as Wick rotation, and here it is applied to the dihedral cosines and squared areas of the hinges, the angles and face sizes that encode the simplex's shape.
The certification covers the full open arc of the rotation parameter and extends continuously to the Euclidean endpoint, where the cosine takes the exact value -1/4, the regular 4-simplex value. Two companion theorems give the closed forms for all twenty hinge areas-squared: 3/16 for all-spacelike classes and z/4 - 1/16 for classes with timelike edges. A third theorem memorializes two exact product-form crossings that land on the branch cut at specific interior parameters, values -40 and -48, which document a previously failed transcription and the repaired convention. All three theorems are kernel-checked with no axioms beyond the standard three, and the library's axiom audit confirms this.
What the declaration does not claim is equally precise. It is a hinge-data continuation, not an action-level continuation. The action, the Regge action obtained by summing deficit angles over simplices sharing an interior hinge, requires a genuine three-or-more-pent interior-hinge simplicial complex, which remains an open target. No FullTheoryLedger flag is changed by this result; the action-level continuation open bit was cleared elsewhere by a separate V2 terminal. The endpoint values are exact because each split cosine is proved continuous on the closed interval, but the Lorentzian endpoint carries a documented sign factor, and no unrestricted equality with the real Lorentzian formula is claimed.
In plain terms, the framework has rigorously established that the shape data of a single quantum simplex survive the rotation between signatures, a necessary step toward a full quantum gravity theory. The reader can now see the precise boundary of this achievement: the geometry of individual building blocks is certified, but the sum over many blocks that would define the full action remains the next open question.
THEOREM wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3 headline, hinge-DATA continuation, complete): for EVERY
triangular hinge (every unordered opposite vertex pair `{p, q}`, both
orientations) of BOTH causal 4-simplex types, at the physical point
`a = 1`, `alpha = 1`, the split-form complex-first Wick continuation is
(i) branch-regular on the FULL open arc interior `Set.Ioo 0 1` and
(ii) a continuous path on the CLOSED interval `[0, 1]` ending at the
Euclidean regular-4-simplex cosine `-(1/4)`.
SCOPE: hinge data (dihedral cosines and areas-squared of single-simplex
hinges) ONLY. The action-level continuation stays OPEN (the C12
three-pent interior-hinge complex is its prerequisite); no
`FullTheoryLedger` flag is touched by this result. -/
theorem wick_hinge_data_continuation_complete :
∀ p q : Fin 5, p ≠ q →
(BranchRegularOn
(fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q
(Set.Ioo 0 1)
∧ ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ))
∧ (BranchRegularOn
(fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
(Set.Ioo 0 1)
∧ ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ)) := by
intro p q hpq
obtain ⟨h41cont, h41end⟩ :=
wick_boundary_continuation_fourOne_allHinges p q hpq
obtain ⟨h32branch, h32cont, h32end⟩ :=
wick_continuation_threeTwo_hinges p q hpq
exact ⟨⟨branchRegular_fourOne_allHinges p q hpq, h41cont, h41end⟩,
⟨h32branch, h32cont, h32end⟩⟩
THEOREM wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3 headline, hinge-DATA continuation, complete): for EVERY
triangular hinge (every unordered opposite vertex pair `{p, q}`, both
orientations) of BOTH causal 4-simplex types, at the physical point
`a = 1`, `alpha = 1`, the split-form complex-first Wick continuation is
(i) branch-regular on the FULL open arc interior `Set.Ioo 0 1` and
(ii) a continuous path on the CLOSED interval `[0, 1]` ending at the
Euclidean regular-4-simplex cosine `-(1/4)`.
SCOPE: hinge data (dihedral cosines and areas-squared of single-simplex
hinges) ONLY. The action-level continuation stays OPEN (the C12
three-pent interior-hinge complex is its prerequisite); no
`FullTheoryLedger` flag is touched by this result. -/
theorem wick_hinge_data_continuation_complete :
∀ p q : Fin 5, p ≠ q →
(BranchRegularOn
(fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q
(Set.Ioo 0 1)
∧ ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1)
∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ))
∧ (BranchRegularOn
(fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t) p q
(Set.Ioo 0 1)
∧ ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1)
∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ)) := by
intro p q hpq
obtain ⟨h41cont, h41end⟩ :=
wick_boundary_continuation_fourOne_allHinges p q hpq
obtain ⟨h32branch, h32cont, h32end⟩ :=
wick_continuation_threeTwo_hinges p q hpq
exact ⟨⟨branchRegular_fourOne_allHinges p q hpq, h41cont, h41end⟩,
⟨h32branch, h32cont, h32end⟩⟩
THEOREM wick_hinge_areaSq_closed_forms_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3, areas-squared complete): the closed forms of ALL twenty
hinge areas-squared, both causal types, for every `z`: `3/16` on the
all-spacelike classes, `z/4 - 1/16` on every class with timelike edges.
Cut avoidance on the open arc interior is
`WickFourOneAllHinges.fourOne_areaSq_interior_off_cut` (identical two
closed forms; the `-5/16` Lorentzian endpoint contact is the documented
allowed contact). -/
theorem wick_hinge_areaSq_closed_forms_complete (z : ℂ) :
(hingeAreaSqC (hingeEdgesC z) 0 1 2 = (3 / 16 : ℂ)
∧ hingeAreaSqC (hingeEdgesC z) 0 1 3 = (3 / 16 : ℂ)
∧ hingeAreaSqC (hingeEdgesC z) 0 2 3 = (3 / 16 : ℂ)
∧ hingeAreaSqC (hingeEdgesC z) 1 2 3 = (3 / 16 : ℂ))
∧ (hingeAreaSqC (hingeEdgesC z) 0 1 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdgesC z) 0 2 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdgesC z) 0 3 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdgesC z) 1 2 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdgesC z) 1 3 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdgesC z) 2 3 4 = z / 4 - 1 / 16)
∧ (hingeAreaSqC (hingeEdges32C z) 0 1 2 = (3 / 16 : ℂ)
∧ hingeAreaSqC (hingeEdges32C z) 0 1 3 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 0 1 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 0 2 3 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 0 2 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 1 2 3 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 1 2 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 0 3 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 1 3 4 = z / 4 - 1 / 16
∧ hingeAreaSqC (hingeEdges32C z) 2 3 4 = z / 4 - 1 / 16) :=
⟨fourOne_areaSq_spacelike z, fourOne_areaSq_timelike z,
threeTwo_areaSq_closed z⟩
THEOREM wick_product_form_kills_memorialized · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3, kill certificates memorialized): the two product-form
gate FAIL events as one kernel statement: at interior arc parameters the
diagonal-cofactor PRODUCT sits ON the `csqrt` branch cut with the exact
values `-40` (mixed class, `tStarMixed`) and `-48` (upper-pair class,
`t = 2/3` exactly). The single-sqrt product transcription stays KILLED;
the split-sqrt form is the repaired convention. -/
theorem wick_product_form_kills_memorialized :
(tStarMixed ∈ Set.Ioo (0 : ℝ) 1
∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 1 1
* cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 4 4
= -40
∧ (-40 : ℂ) ∉ Complex.slitPlane)
∧ ((2 / 3 : ℝ) ∈ Set.Ioo (0 : ℝ) 1
∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 1 1
* cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 2 2
= -48
∧ (-48 : ℂ) ∉ Complex.slitPlane) :=
⟨product_form_crossing_threeTwo_mixed, product_form_crossing_threeTwo_upper⟩
THEOREM action_level_closed_by_v2_elsewhere · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- Documentation theorem (by `rfl`): hinge-data continuation is not the
action-level closer. The CausalSimplex4D action-level open bit was cleared
2026-07-23 by the V2 terminal (`wick_action_continuation_4d_v2_holds`),
not by this module. -/
theorem action_level_closed_by_v2_elsewhere :
causalSimplex4DStatus.action_level_continuation_open = false := rfl
What this page does not claim
The action-level continuation is not established by this result; it remains open and requires a three-or-more-pent interior-hinge simplicial complex. No unrestricted equality with the real Lorentzian formula is claimed at the endpoint, due to the documented sign factor. This result does not change any FullTheoryLedger flag; the action-level open bit was cleared by a separate V2 terminal.
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/WickHingeDataComplete.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 simplicial complex structure would allow the action-level continuation to be certified?
- How does the hinge-data continuation relate to the full Regge action in the classical limit?
- What physical predictions follow from the Euclidean endpoint value -1/4 for the regular 4-simplex?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3 headline, hinge-DATA continuation, complete): for EVERY triangular hinge (every unordered opposite vertex pair `{p, q}`, both orientations) of BOTH causal 4-simplex types, at the physical point `a = 1`, `alpha = 1`, the split-form complex-first Wick continuation is (i) branch-regular on the FULL open arc interior `Set.Ioo 0 1` and (ii) a continuous path on the CLOSED interval `[0, 1]` ending at the Euclidean regular-4-simplex cosine `-(1/4)`. SCOPE: hinge data (dihedral cosines and areas-squared of single-simplex hinges) ONLY. The action-level continuation stays OPEN (the C12 three-pent interior-hinge complex is its prerequisite); no `FullTheoryLedger` flag is touched by this result. -/ theorem wick_hinge_data_continuation_complete : ∀ p q : Fin 5, p ≠ q → (BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q (Set.Ioo 0 1) ∧ ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1) ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ)) ∧ (BranchRegularOn (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t) p q (Set.Ioo 0 1) ∧ ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1) ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ)) := by intro p q hpq obtain ⟨h41cont, h41end⟩ := wick_boundary_continuation_fourOne_allHinges p q hpq obtain ⟨h32branch, h32cont, h32end⟩ := wick_continuation_threeTwo_hinges p q hpq exact ⟨⟨branchRegular_fourOne_allHinges p q hpq, h41cont, h41end⟩, ⟨h32branch, h32cont, h32end⟩⟩The theorem certifies, for every one of the twenty triangular hinges of both causal simplex types, that the geometric data continue smoothly when the signature of spacetime is rotated from Lorentzian to Euclidean. wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.leanTHEOREM wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3 headline, hinge-DATA continuation, complete): for EVERY triangular hinge (every unordered opposite vertex pair `{p, q}`, both orientations) of BOTH causal 4-simplex types, at the physical point `a = 1`, `alpha = 1`, the split-form complex-first Wick continuation is (i) branch-regular on the FULL open arc interior `Set.Ioo 0 1` and (ii) a continuous path on the CLOSED interval `[0, 1]` ending at the Euclidean regular-4-simplex cosine `-(1/4)`. SCOPE: hinge data (dihedral cosines and areas-squared of single-simplex hinges) ONLY. The action-level continuation stays OPEN (the C12 three-pent interior-hinge complex is its prerequisite); no `FullTheoryLedger` flag is touched by this result. -/ theorem wick_hinge_data_continuation_complete : ∀ p q : Fin 5, p ≠ q → (BranchRegularOn (fun t => continuationEdgesC CausalPentType.fourOne 1 1 t) p q (Set.Ioo 0 1) ∧ ContinuousOn (fourOneCosPath p q) (Set.Icc 0 1) ∧ fourOneCosPath p q 1 = -(1 / 4 : ℂ)) ∧ (BranchRegularOn (fun t => continuationEdgesC CausalPentType.threeTwo 1 1 t) p q (Set.Ioo 0 1) ∧ ContinuousOn (threeTwoCosPath p q) (Set.Icc 0 1) ∧ threeTwoCosPath p q 1 = -(1 / 4 : ℂ)) := by intro p q hpq obtain ⟨h41cont, h41end⟩ := wick_boundary_continuation_fourOne_allHinges p q hpq obtain ⟨h32branch, h32cont, h32end⟩ := wick_continuation_threeTwo_hinges p q hpq exact ⟨⟨branchRegular_fourOne_allHinges p q hpq, h41cont, h41end⟩, ⟨h32branch, h32cont, h32end⟩⟩The certification covers the full open arc of the rotation parameter and extends continuously to the Euclidean endpoint, where the cosine takes the exact value -1/4. wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.leanTHEOREM wick_hinge_areaSq_closed_forms_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3, areas-squared complete): the closed forms of ALL twenty hinge areas-squared, both causal types, for every `z`: `3/16` on the all-spacelike classes, `z/4 - 1/16` on every class with timelike edges. Cut avoidance on the open arc interior is `WickFourOneAllHinges.fourOne_areaSq_interior_off_cut` (identical two closed forms; the `-5/16` Lorentzian endpoint contact is the documented allowed contact). -/ theorem wick_hinge_areaSq_closed_forms_complete (z : ℂ) : (hingeAreaSqC (hingeEdgesC z) 0 1 2 = (3 / 16 : ℂ) ∧ hingeAreaSqC (hingeEdgesC z) 0 1 3 = (3 / 16 : ℂ) ∧ hingeAreaSqC (hingeEdgesC z) 0 2 3 = (3 / 16 : ℂ) ∧ hingeAreaSqC (hingeEdgesC z) 1 2 3 = (3 / 16 : ℂ)) ∧ (hingeAreaSqC (hingeEdgesC z) 0 1 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdgesC z) 0 2 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdgesC z) 0 3 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdgesC z) 1 2 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdgesC z) 1 3 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdgesC z) 2 3 4 = z / 4 - 1 / 16) ∧ (hingeAreaSqC (hingeEdges32C z) 0 1 2 = (3 / 16 : ℂ) ∧ hingeAreaSqC (hingeEdges32C z) 0 1 3 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 0 1 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 0 2 3 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 0 2 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 1 2 3 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 1 2 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 0 3 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 1 3 4 = z / 4 - 1 / 16 ∧ hingeAreaSqC (hingeEdges32C z) 2 3 4 = z / 4 - 1 / 16) := ⟨fourOne_areaSq_spacelike z, fourOne_areaSq_timelike z, threeTwo_areaSq_closed z⟩Two companion theorems give the closed forms for all twenty hinge areas-squared: 3/16 for all-spacelike classes and z/4 - 1/16 for classes with timelike edges. wick_hinge_areaSq_closed_forms_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.leanTHEOREM wick_product_form_kills_memorialized · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- THEOREM (B3, kill certificates memorialized): the two product-form gate FAIL events as one kernel statement: at interior arc parameters the diagonal-cofactor PRODUCT sits ON the `csqrt` branch cut with the exact values `-40` (mixed class, `tStarMixed`) and `-48` (upper-pair class, `t = 2/3` exactly). The single-sqrt product transcription stays KILLED; the split-sqrt form is the repaired convention. -/ theorem wick_product_form_kills_memorialized : (tStarMixed ∈ Set.Ioo (0 : ℝ) 1 ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 1 1 * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 tStarMixed) 4 4 = -40 ∧ (-40 : ℂ) ∉ Complex.slitPlane) ∧ ((2 / 3 : ℝ) ∈ Set.Ioo (0 : ℝ) 1 ∧ cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 1 1 * cmCofactorC (continuationEdgesC CausalPentType.threeTwo 1 1 (2 / 3)) 2 2 = -48 ∧ (-48 : ℂ) ∉ Complex.slitPlane) := ⟨product_form_crossing_threeTwo_mixed, product_form_crossing_threeTwo_upper⟩A third theorem memorializes two exact product-form crossings that land on the branch cut at specific interior parameters, values -40 and -48. wick_product_form_kills_memorialized · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.leanTHEOREM action_level_closed_by_v2_elsewhere · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
/-- Documentation theorem (by `rfl`): hinge-data continuation is not the action-level closer. The CausalSimplex4D action-level open bit was cleared 2026-07-23 by the V2 terminal (`wick_action_continuation_4d_v2_holds`), not by this module. -/ theorem action_level_closed_by_v2_elsewhere : causalSimplex4DStatus.action_level_continuation_open = false := rflIt is a hinge-data continuation, not an action-level continuation. action_level_closed_by_v2_elsewhere · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean