Encyclopedia Gravity Gravity Seven Gaps Wick Hinge Data Complete Wick Hinge Area Sq Closed Forms Comp
ARTICLE 4 claims 3 theorems 1 open
Gravity Seven Gaps Wick Hinge Data Complete Wick Hinge Area Sq Closed Forms Comp
For a single causal 4-simplex, the squared areas of all twenty triangular hinges follow exactly two closed forms under the complex Wick continuation.
The hinge areas
In the framework's study of causal 4-simplices, the building blocks of spacetime, a triangular hinge is a face shared by tetrahedra. The declaration wick_hinge_areaSq_closed_forms_complete proves, in the machine-checked library of formal theorems, that for every one of the twenty hinges on either of the two causal simplex types, the squared area takes exactly one of two simple expressions in the complex parameter z. For hinges whose edges are all spacelike, the squared area is constantly 3/16. For every hinge that includes at least one timelike edge, it is z/4 − 1/16.
This is a statement about a single simplex, not about a full spacetime. The declaration certifies the continuation of these areas along the upper half-plane arc at the physical point a = 1, alpha = 1. It does not continue the Regge action itself, which would require summing deficit angles over a complex of three or more simplices sharing an interior hinge. That action-level continuation remains open, and the declaration explicitly leaves the relevant status flag untouched.
The result is a theorem in the framework's library, kernel-checked with no axioms beyond the standard three. It also memorializes two exact product-form failures: the diagonal-cofactor product lands on the branch cut with values −40 and −48 at specific interior parameters, which the split-sqrt convention repairs. The endpoint values are exact because each split cosine is continuous on the closed interval, though the Lorentzian endpoint carries a documented sign factor and no unrestricted equality with the real formula is claimed.
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_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_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⟩
What this page does not claim
The declaration does not continue the Regge action itself. It does not change any FullTheoryLedger flag. It does not claim an unrestricted equality with the real Lorentzian formula at the endpoint.
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 is needed to certify the action-level continuation?
- How do the two closed forms behave at the Lorentzian endpoint with the sign factor applied?
- What is the geometric significance of the constant 3/16 for all-spacelike hinges?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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⟩For every one of the twenty hinges on either of the two causal simplex types, the squared area takes exactly one of two simple expressions in the complex parameter z. wick_hinge_areaSq_closed_forms_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⟩For hinges whose edges are all spacelike, the squared area is constantly 3/16. wick_hinge_areaSq_closed_forms_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⟩For every hinge that includes at least one timelike edge, it is z/4 − 1/16. wick_hinge_areaSq_closed_forms_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean- OPENThe action-level continuation remains open.