Gravity Seven Gaps Wick Hinge Data Complete Action Level Closed By V2 Elsewhere

The action-level flag

In the Recognition Science framework's machine-checked library of formal theorems, a declaration named action_level_closed_by_v2_elsewhere does one narrow bookkeeping job: it records that a status flag, action_level_continuation_open, has been set to false. The flag belongs to a data structure describing a causal 4-simplex, the four-dimensional building block of spacetime in this approach. The declaration itself is a proof by definitional equality, meaning the fact is true because of how the flag was defined, not because this library proved the underlying physics.

The context matters. A separate part of the same library, WickHingeDataComplete, proves three substantial theorems about continuing hinge data: the dihedral cosines and areas-squared of the triangular faces of a single causal 4-simplex, for both causal types, along a complex arc from Lorentzian to Euclidean signature. Those theorems are real and kernel-checked. But they cover only hinge data, not the full action. The action-level continuation, which would sum deficit angles over simplices sharing an interior hinge and thus continue the Regge action itself, requires a simplicial complex with three or more simplices meeting at an interior hinge. That prerequisite is the C12 lane's question and is not touched in this part of the library.

The declaration action_level_closed_by_v2_elsewhere exists precisely to prevent a reader from misattributing the closure. Its docstring states that the action-level open bit was cleared on 2026-07-23 by the V2 terminal, with a separate theorem wick_action_continuation_4d_v2_holds, not by this library. The name says it plainly: the action-level question was closed by V2, elsewhere. This library merely records that fact in the status structure, so that downstream code and readers know the flag is no longer open.

What the declaration does not claim is equally important. It does not claim that the hinge-data theorems in this library constitute an action-level continuation. It does not claim that the action-level continuation is proved here. It does not even claim that the action-level continuation is proved at all in this file; it points elsewhere. The honest scope note in the library's documentation is explicit: the action-level continuation remains OPEN as far as this library is concerned, and no FullTheoryLedger flag is changed by the hinge-data results. The declaration is a pointer, not a proof.

/-- 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

/-- 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

/-- 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⟩⟩

/-- 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

This library proves the action-level continuation of the Regge action. The hinge-data theorems in this file constitute an action-level continuation. The declaration action_level_closed_by_v2_elsewhere itself contains the proof of the action-level continuation.

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: