Encyclopedia Gravity Gravity Seven Gaps Wick Hinge Data Complete

ARTICLE 4 claims 3 theorems 1 open

Gravity Seven Gaps Wick Hinge Data Complete

A machine-checked proof certifies that the geometric data of every triangular hinge in a causal 4-simplex continues smoothly from Euclidean to Lorentzian signature, a complete but deliberately narrow result.

Verify this page

The hinge-data certificate

In the Recognition Science framework's study of quantum gravity, a causal 4-simplex is the discrete spacetime building block: a five-vertex tetrahedron-like object whose edges carry timelike or spacelike character. The framework's library of formal theorems has now certified, for both possible causal types of this simplex, that the geometric data attached to every one of its twenty triangular hinges can be continued from the Euclidean regime into the Lorentzian one. A hinge is the triangular face where two tetrahedra meet, and its data are the dihedral cosine and the squared area of that triangle.

The central theorem, wick_hinge_data_continuation_complete, proves for every unordered pair of vertices (equivalently, every triangular hinge) and for both causal types that the continuation is branch-regular on the full open arc interior, continuous on the closed interval [0,1], and ends at the Euclidean regular-4-simplex cosine value -(1/4). A second theorem, wick_hinge_areaSq_closed_forms_complete, gives the closed form for all twenty areas-squared: 3/16 on all-spacelike classes, and z/4 - 1/16 on every class with timelike edges. A third theorem, wick_product_form_kills_memorialized, records two exact product-form crossings that land on the branch cut at interior parameters, values -40 and -48, memorializing a gate failure that the split-sqrt form repairs.

The scope is deliberately narrow. This is a hinge-data continuation, not an action-level continuation. The action-level result, summing deficit angles over simplices sharing an interior hinge to continue the Regge action itself, remains OPEN and requires a genuine three-or-more-pent interior-hinge simplicial complex, which is a separate lane's prerequisite question. No FullTheoryLedger flag is changed by this result; the action-level continuation open bit remains true, though a documentation theorem notes it was cleared elsewhere by a V2 terminal on 2026-07-23. Endpoint honesty is inherited: branch certificates are interior-only because several hinge data sit exactly on a cut at the Lorentzian endpoint, though the endpoint values are exact because each split cosine is proved continuous on [0,1].

What this establishes in plain language is a complete and machine-checked certificate for the geometric data of a single causal 4-simplex's hinges, not for the full action. The three theorems are kernel-checked conjunctions of earlier results, sorry-free, and audit to the standard three axioms [propext, Classical.choice, Quot.sound]. The framework models this as a step in its Seven-Gaps campaign, lane B of the finishing charter, the third deliverable: the conjunction of per-type certificates into a single completeness statement over both causal types and all twenty hinges. The reader can now see exactly which geometric data are certified and which are not, and the framework's library stands with a precise, bounded claim rather than an overreaching one.

THEOREM wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean
wick_hinge_data_continuation_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean:86 
/-- 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
wick_hinge_areaSq_closed_forms_complete · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean:118 
/-- 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
wick_product_form_kills_memorialized · IndisputableMonolith/Gravity/SevenGaps/WickHingeDataComplete.lean:149 
/-- 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⟩

What this page does not claim

This result does not prove the action-level Wick continuation of the Regge action itself. This result does not change any FullTheoryLedger flag; the action-level continuation open bit remains true here. This result does not claim unrestricted equality with the real Lorentzian formula at the endpoint, due to the documented split-form sign factor.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND